3.2 Comparison to lambda calculus

Prev Up Next Page 20 of 800 Search internet

At the lowest level, the Logiweb programming language is lambda calculus (lambda abstraction \ x . A, functional application x ' y, and variables) extended with three more constructs. The three additional constructs are a constant true, a selection construct If x then y else z, and quoting quote t end quote.

The constant true is similar to NIL in Lisp and null in C.

The If x then y else z construct equals y if x equals true and equals z if x differs from true (except if computation of x loops indefinitely, of course). A term x is considered to differ from true iff x can be reduced to a term of form \ x . A.

The value of quote t end quote represents the term t. The quote t end quote construct corresponds to (quote x) in Lisp. In principle, quote t end quote could be defined as a macro which expanded into a monster formula containing only lambda abstraction, true, and If-then-else.

The Logiweb reduction system is as follows:

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 reduction engine uses leftmost reduction. Quotes are reduced as if they were macro expanded into monster formulas containing only lambda abstraction, true, and If-then-else.

Lambda calculus and mathematical equality

A Logiweb term is in 'root normal form' if it has form true or \ x . A.

Two Logiweb terms are 'root equivalent' if they both reduce to T, both reduce to lambda terms, or neither reduce to root normal form

Logiweb does not support parallel 'or', and there is no way to define parallel 'or' inside Logiweb. But if it did, then parallel 'or' x||y would reduce to T if x or y reduced to T and would reduce to a lambda abstraction if both x and y reduced to lambda abstractions. If parallel 'or' was added to Logiweb, then two closed terms x and y would be considered to be 'mathematically equal' if f ' x was root equivalent to f ' y for all closed terms f.

Mathematical equality defines a class division on the set of terms. We shall refer to the classes of that class division as 'maps'.

Maps satisfy a long list of axioms which make them convenient to reason about mathematically. Furthermore, one can generalize maps by adding Hilberts epsilon operator to the language. Doing so results in map theory. Map theory can be used both for reasoning about Logiweb programs and for general mathematics. As an example, the notions of sets and set membership are definable in map theory and all axioms of ZFC set theory are provable in map theory.

Prev Up Next Page 20 of 800 Search logiweb.eu

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