Page 83 of 800
| Page 83 of 800 | Search internet |
Put this in macro.lgs and compile.
""P macro
""R base
""D 32
lambda " dot "
""B
page ( ""N , ""C )
title "A macro definition"
bib "@MISC{dummy}"
main text "
\begin{statements}
\item "[[ macro define lambda x dot y as \ x . y end define ]]"
\item "[[ etst ( lambda x dot x + 2 ) ' 3 ; 5 end test ]]"
\end{statements}
\nocite{dummy}\color{white}\bibliography{./page}
"
appendix "
\begin{statements}
\item "[[ tex show define lambda x dot y as "
\hat{",x,"
}",y end define ]]"
\end{statements}
"
end page
The lambda x dot y construct is rendered 
like Alonso Church and people before him wrote it. But when Church handed in a manuscript, one typographer could not put a hat above a character and put the hat in front instead. Another typographer saw it, considered it a mistake, and guessed that the hat was the lower part of a lambda, so he replaced the hat by a lambda, and lambda calculus was born.
The source above defines the new lambda by letting it macro expand to the lambda from the base page. An alternative would be that you define your own lambda. Only problem is that lambda abstraction is one of the nine predefined concepts of Logiweb and thus you cannot define it. Instead you can proclaim it. Thus, instead of the macro definition above you would write:
\item "[[ proclaim lambda x dot y as "lambda" end proclaim ]]"
That renders as 
and proclaims to denote lambda abstraction. Strings are hardwired into the language so they can be used even before proclaiming anything. For more on the nine predefined constructs see the section on bootstrapping.
In many situations, a macro definition is better than proclaiming your own lambda. Suppose you work in a theory which includes beta-reduction among its axioms. Furthermore, suppose the axiom of beta-reduction explicitly refers to \ x . y. In that case you should prefer using a macro since macro expansion occurs before proof checking. On the other hand, good theories recognize everything proclaimed as a lambda as a lambda, so you could also proclaim your own lambda and complain fiercely to the one who formulated the beta-rule.
| Page 83 of 800 | Search logiweb.eu |