Page 20 of 800
| Page 20 of 800 | Search internet |
At the lowest level, the Logiweb programming language is lambda calculus (lambda abstraction 
, functional application 
, and variables) extended with three more constructs. The three additional constructs are a constant 
, a selection construct 
, and quoting 
.
The constant is similar to NIL in Lisp and null in C.
The construct equals y if x equals and equals z if x differs from (except if computation of x loops indefinitely, of course). A term x is considered to differ from iff x can be reduced to a term of form .
The value of represents the term t. The construct corresponds to (quote x) in Lisp. In principle, could be defined as a macro which expanded into a monster formula containing only lambda abstraction, , and If-then-else.
The Logiweb reduction system is as follows:
The reduction engine uses leftmost reduction. Quotes are reduced as if they were macro expanded into monster formulas containing only lambda abstraction, , and If-then-else.
A Logiweb term is in 'root normal form' if it has form or .
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 
was root equivalent to 
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.
| Page 20 of 800 | Search logiweb.eu |