Lambda expressions in calchylus module

All three concepts and four rules are implemented in the calchylus module so that for example the very basic Lambda calculus identity application λx.x y becomes (L x , x y) in calchylus notation. Infact, the function indicator and the separator character can be freely defined in calchylus by with- initialization macros.

In the most of the examples we will use L and , because it will be easier to type L from the keyboard. Using the comma rather than the dot comes from the Hy programming language environment restrictions, where the dot is a reserved letter for cons in list processing.

Let us strip down the former expression and show how all rules are taking place in it.

In (L x , x y), L is the Lambda function indicator and parentheses () indicate the whole application that should be evaluated. x before the separator , is the function argument. x after the separator, but :underline:`before the next space` is the function body. Finally y is the value for the function, thus we have a full application here, rather than just an abstraction. Abstraction would, on the other hand be: (L x , x).

Note

In mathematics, identity function can be denoted either by $$f(x) = x$$ or by

$$x → f(x)$$.

Because these rules are notable in any functional and Lisp like language, there is a great temptation to implement Lambda calculus evaluator as a native anonymous function calls. The problem with this approach is very subtle and will bring practicer to the deep foundations of the programming languages. That is, to decide in which order to evaluate arguments and functions and how to deal with argument name collisions.

Let us first see the easy native implementation of the Lambda calculus to learn what all this means.