7.7.2 Reduction system

Page 198 of 800

Search internet

All maps supported by Logiweb can be written using the following syntax:

$M ::= V | \ V . M | M ' M | true | If M then M else M$

Above, V denotes the syntax class of all variables and M denotes the syntax class of all maps.

When given a map, the Logiweb abstract machine (lgwam) is able to reduce the map. Lgwam reduces the map according to the following reduction system:

$array ( left,left,left ) ( \ x . y ) ' z & %% reduce to %% & < y | x := z > \\ true ' z & %% reduce to %% & true \\ If true then u else v & %% reduce to %% & u \\ If \ x . y then u else v & %% reduce to %% & v end array$

The right hand side of the first reduction rule denotes the result of replacing x by z in y with suitable renaming of bound variables.

The reduction order used is normal order reduction.

A term is said to be on true normal form if it has form true . It is said to be on function normal form if it has form $\ v . m$ for some variable v of syntax class V and some term m of syntax class M. A map is said to be on root normal form if it is on true or function normal form.

When given a term, lgwam reduces it using the reduction rules above and normal order reduction until the term is on root normal form (if ever).

Page 198 of 800

Search logiweb.eu