Lambda Calculus

<Exp> ::= <ident> |  
( <Exp> ) |  
<Exp> <Exp> |  --application
λ<ident>.<Exp>    --abstraction
-- Syntax of the λ-calculus --

The syntax of the λ-calculus is very simple, comprising just four kinds of expression but surprisingly it is sufficient to define any computable function. Constants including integers, booleans, conditiional, declarations and so on can all be defined using just the syntax above, as can be demonstrated by examples. Because of this it is often convenient to extend the syntax with options for constants (0, 1, 2, ..., +, -, *, /, =, ≠, ≤, <, ≥, >, true, false, ∧, ∨, ¬, nil, cons, null, hd, tl, if...then...else..., let {rec}...in... etc.) but, if that is done, it is only a convenience and does not increase the power of the language. Note that an abstraction defines an anonymous function.




The pure λ-calculus appears to lack recursion, or equivalently iteration, but recursive functions can in fact be defined by using the fixed-point operator Y, e.g.,
let Y = lambda G. (lambda g. G(g g)) (lambda g. G(g g))
in let F = lambda f. lambda n. if n<=0 then 1 else n*f(n-1)
in Y F 10
or even
(lambda G. (lambda g. G(g g)) (lambda g. G(g g)))
(lambda f. lambda n. if n<=0 then 1 else n*f(n-1)) 10

References

[All92] Lloyd Allison, 'Applications of Recursively Defined Data Structures', Australian Computer Journal, 25(1), pp.14-20, arxiv:2206.12795, 1993.
[All92] Lloyd Allison, 'Lazy Dynamic-Programming can be Eager', Information Processing Letters, 43(4), pp.207-212, doi:10.1016/0020-0190(92)90202-7, September 1992.
[All89] Lloyd Allison, 'Circular Programs and Self-Referential Structures', Software Practice & Experience, 19(2), pp.99-109, doi:10.1002/spe.4380190202, February 1989.
[All88] Lloyd Allison, 'Some Applications of Continuations', The Computer Journal, 31(1), pp.9-16, doi:10.1093/comjnl/31.1.9, January 1988.
And other publications.