Page 241 of 800
| Page 241 of 800 | Search internet |
The value of
equals the value of
except for two things:
, 
is a free variable. is taken from the term 
.As an example, the value of
equals 
except for debugging information. In contrast, the value of
equals 
because 'unquoting' (the underlining) does not work inside quotes.
As an example of use, consider again the function
The expand-all function implements that e.g. 
macro expands to 
. The expand-all function unpacks the argument x and macro expands the subterms u and v of the term t. After expanding u and v, expand-all passes t, u, and v on to expand-all1 which finishes the work. The expand-all1 function mainly uses the macro expanded subterms u and v but debugging information is taken from the unexpanded term t.
The term does not really macro expand to . Rather, it expands to
That is so because it was chosen on the Peano page to let universal quantification piggyback lambda abstraction. That allows to re-use functions for variable substitution and computation of the 'free' and 'freefor' side conditions.
The definition of expand-all1 reads:
The expand-all1 function traverses u as long as the principal operator of u is a comma operator and then uses 
to construct a universal quantifier with debugging information taken from t. The debugging information is only inserted in the root of the tree, not in the subtrees u and v which retain their own debugging information.
| Page 241 of 800 | Search logiweb.eu |