In the 1930s, Alonzo Church created Lambda Calculus as a universal model of computation. This means that this model is capable of computing anything that can be computed algorithmically. This is typically used as the basis model of computation for functional programming, which utilizes recursion above all else.
λ-Calculus is based on the use of lambda terms and functions to represent natural numbers and operations.
- x is a variable
- (λx.M) is an abstraction, with M being a lambda term
- (M N) is an application, with both M and N being lambda terms
- (λx.λy.(λz.(λx.z x) (λy.z y)) (x y)) is an example expression that Wikipedia gives
There are two reduction operations that can take place in λ-Calculus expressions: α-conversion and β-reduction. Renaming bound variables is α-conversion. β-reduction is substituting bound variables in an expression for their applications. An example of reduction:
(λx.λy.(x (λx.y x))) (λz.z)
(λx.λy.(x (λw.y w))) (λz.z) : α-conversion (renamed x -> w)
(λy.((λz.z) (λw.y w))) : β-reduction
(λy.λw.y w) : β-reduction
(λx.λy.x y) : α-conversion
(λxy.x y) : alternate notation
So functions can be reduced. This of course doesn’t mean anything unless we create meanings for these functions. Numbers are defined:
0 := λfx.x
1 := λfx.f x
2 := λfx.f (f x)
3 := λfx.f (f (f x))
… and so on
Because numbers are defined as functions, they can be applied to other functions and have other functions applied to them. It takes a long time to work out the applications of these numbers on one another, but eventually it becomes obvious that (M N), where M and N are numbers in that form, evaluates to NM. Other operations can be computed using certain functions (such as repeated use of the successor function).
Because λ-Calculus is a universal model of computation, it is equivalent to a Turing machine. Various programming languages are based on λ-Calculus, including Haskell and Lisp. Most programming languages also have anonymous functions (lambda functions) based on these principles. Because all variables are bound in lambda expressions, these languages and functions must rely primarily on recursion, rather than structures such as loops. I’ll be studying recursion and functional programming languages.