Created: 2026-07-01 10:58 by Thom
In mathematical logic, lambda calculus is a formal way to define computation. Alonzo Church came up with it in 1936. It is designed like a Turing machine, which is also from 1936, and with the Church-Turing Thesis it is stated that these two are equivalent. How is it defined? Lambda calculus is defined by terms from this grammar: `E -> xtext( )|text( )lambda x . Etext( )|text( )Etext( )E` This is also an inductive type, variable x is a valid term, an abstraction is a valid term with a valid term in it, and application is also from valid terms. Within lambda terms if there is a variable not in `lambda` then it is considered 'free'. Any free occurrence of `x` in a term `M` (`lambda x . M`) any other variable in `M` is free in `lambda x . M`. How can you actually use it? There are many strategies for reducing these terms, and in spirit with the greek letters, reductions are called `alpha`, `beta`, and `eta`. This article will focus on `beta-reduction`. `beta-reduction` is defined as the following: an application form `(lambda x . t) s` reduces to `t[x:=s]`. For example for every s, `(lambda x . x) s -> x[x:=s]`. You can see that `lambda x . x` is the identity function. `(lambda x . y) s -> y[x:=s] = y` makes `lambda x . y` a constant function. Applications Lambda calculus is Turing complete so every term can be used to simulate a Turing machine. It has applications in mathematics, linguistics, computer science. It played an important role in the theory of programming languages especially functional programming languages like Haskell, ML, and more. Versions of lambda calculus are untyped and simply typed. In typed lambda calculus, functions can be applied only if they accept the given input's "type" of data. Examples of computation The basic lambda calculus may be used to model arithmetic, Booleans, data structures, and recursion. Arithmetic Church numerals are the most common way to define the natural numbers (`NN`). These are defined as: `0 := lambda f . lambda x . x` `1 := lambda f . lambda x . ftext( )x` `2 := lambda f . lambda x . ftext( )(ftext( )x)` `3 := lambda f . lambda x . ftext( )(ftext( )(ftext( )x))` and so on. These are higher order functions it takes a single-argument function `f`, and returns another single-argument function. The function `f` composed with itself `n` times, like `f^((n))` and `f^((0))` is considered the identity function. Logic and Predicates By definition these are called Church Booleans. TRUE and FALSE are defined as: `TRUE := lambda x . lambda y . x` `FALSE := lambda x . lambda y . y` These should be used with logical connectives like or, and, and not. These are defined as: `AND := lambda p . lambda q . ptext( )qtext( )p` `OR := lambda p . lambda q . ptext( )ptext( )q` `NOT := lambda p . ptext( )FALSEtext( )TRUE` And to define control flow use this: `IFTHENELSE := lambda p . lambda a . lambda b . ptext( )atext( )b` Now logical statements can be computed for example: `ANDtext( )TRUEtext( )FALSE` `-= (lambda p . lambda q . p q p)text( )TRUEtext( )FALSE ->_betatext( )TRUEtext( )FALSEtext( )TRUE` `-= (lambda x . lambda y . x)text( )FALSEtext( )TRUE ->_betatext( )FALSE` As can be seen `ANDtext( )FALSEtext( )TRUE` is `FALSE`. A predicate is a function that returns a Boolean value. The most fundamental predicate is `ISZERO`, which returns `TRUE` if its argument is the Church numeral `0`: `ISZERO := lambda n . ntext( )(lambda x . FALSE)text( )TRUE` Recursion How can you do loops? This is quite simple, using recursion. Recursion is defined with the y combinator or a fixed point combinator. `Y := lambda g . (lambda x . g (xtext( )x)) (lambda x . g (xtext( )x))` As a tip read To Mock a Mockingbird for logic puzzles based on lambda calculus.