Logiweb(TM)

7.7.2 Reduction system

Prev Up Next 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).

Prev Up Next Page 198 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05