History

Please fill in your query. A complete syntax description you will find on the General Help page.
A nominal axiomatization of the lambda calculus. (English)
J. Log. Comput. 20, No. 2, 501-531 (2010).
The lambda calculus is, as the authors say, fundamental in computer science, however an algebraic form of it would be easier to use. Combinatory logic is a very simple algebraic form of the lambda calculus, but the authors claim that there is no sound translation of $λ$-terms to combinators. This I would dispute [see {\it M. W. Bunder, J. R. Hindley} and {\it J. P. Seldin}, “On adding ($ξ$) to weak equality in combinatory logic”, J. Symb. Log. 54, No.~2, 590‒607 (1989; Zbl 0702.03007)]. They also say that the combinatory postulates are not natural or ergonomic, which is probably true. The authors develop the “nominal” algebras ULAM (which they show to be sound and complete with respect to the $λβ$ calculus) and ULAME (sound and complete with respect to the $λβη$-calculus). In addition to application and “distinct unknowns” (Curry’s indeterminates), which is all that combinatory logic needs, these have $λ$-abstraction, permutations, used to define the substitutions needed in the rules ($α$) and ($β$), as well as “$x\#t$” to stand for “$x$ is not free in $t$”. While the $λ$-postulates of these new systems are quite natural, some of the additional postulates needed for the new concepts (for example (fr) and (ax)) read rather strangely. One $λ$-postulate, $β$id, seems to be derivable from the others.
Reviewer: Martin W. Bunder (Wollongong)