The Lambda Calculus is an abstract mathematical theory of computation, involving functions, and can be thought of as being the theoretical foundation of Functional Programming. It is “a formal system in mathematical logic for expressing computation [where its notation is thus] based on function abstraction and application using variable binding and substitution“(Ref#: B). It was was the American born mathematician and logician Alonzo Church who came up with Lambda Calculus (λ-calculus) back in the 1930s.
Lambda Functions or Anonymous Functions are featured in functional languages like Haskell, but also in languages like Python, or in mixed languages (which aim to combine functional elements into previously non-functional languages) such as recent versions of C++, or the Swift language.
“The λ calculus can be called the smallest universal programming language of the world … [it] consists of a single transformation rule (variable substitution) and a single function definition scheme. It was introduced in the 1930s by Alonzo Church as a way of formalizing the concept of effective computability” (Ref#: C).
The Lambda Calculus is said to be Turing complete since it can be used to simulate any Turing machine, where a Turing Machine can be thought of as a simple, state-based model of computation which comprises a set of rules governing different states and transitions (so we’re not talking about a real machine but a theoretical one).
However, importantly, the Lambda calculus, unlike in a Turing Machine, there is no internal state (it’s stateless). Alonzo Church was a mathematician and interestingly he also happened to become the Ph.D. supervisor of Alan Turing, hence the genesis of the idea of Turing Machines took some ideas from Church’s thoughts, and their collective works are where the idea of the Church-Turing Thesis originated.
Lambda Calculus can be used to encode any computation or any computer program. Being a universal model of computation we know that any Turing Machine program can be translated into Lambda calculus and vice-versa. In addition, functional programming languages are based on λ-calculus concepts, with “mixed” programming languages also now incorporating concepts deriving from Lambda Calculus.
What Does The Lambda Calculus Look Like?
The central concept in λ calculus is the “expression”. A “name”, which is also known as a “variable”, is an identifier that we could choose to represent with any lower case letter. “Lambda calculus consists of constructing lambda terms and performing reduction operations on them. In the simplest form of lambda calculus, terms are built using only the following rules:”
| Syntax | Name | Description |
|---|---|---|
| x | Variable | A character or string representing a parameter or mathematical/logical value |
| (λx.M) | Abstraction | Function definition (M is a lambda term). The variable x becomes bound in the expression. (this can be linked to the idea of an anonymous function) |
| (M N) | Application | Applying a function to an argument. M and N are lambda terms. |
producing expressions such as (λx.λy.(λz.(λx.z x) (λy.z y)) (x y)). Parentheses can be dropped if the expression is unambiguous.
Simple examples might look like:
- For an Increment Function:
λx.x+1(this takes one input x, and returns x + 1) - For addition:
λx.λy.x+y(this takes two inputs x and y, and gives us the output)
[Insert squaring number example]
So the lambda calculus can (in the same way a Turing Machine can) encode any computation (that is you can represent really any computer program using it). It can be regarded as the basis of any Functional Programming Language (such as Haskell). Therefore, we can regard the influence of the lambda calculus as being present in pretty much any modern programming language.
Further Topics: Free and Bound Variables, Reductions, Church Numerals, Ordered Pairs, Relational Operators, Recursion, Computability, Typed Lambda Calculus.
Free and Bound Variables
“In an abstraction like λx.xthe variable x is something that has no original meaning but is a placeholder. We say that is a variable bound to the λ.
On the other hand, in λx.y, i.e. a function which always returns y whatever it takes, y is a free variable since it has an independent meaning by itself” (Ref#: H).
Church Numerals
The Church Numerals are a representation of the natural numbers (which are numbers used for ordering and counting, like 1, 2, 3 or including the zero in some versions) through the use of lambda notation. “The higher-order function that represents natural number n is a function that maps any function f to its n-fold composition. In simpler terms, the “value” of the numeral is equivalent to the number of times the function encapsulates its argument” (Ref#: I).
Starting with 0 not applying the function at all, proceed with 1 applying the function once:
“
The Church numeral 3 represents the action of applying any given function three times to a value. The supplied function is first applied to a supplied parameter and then successively to its own result. The end result is not the numeral 3 (unless the supplied parameter happens to be 0 and the function is a successor function). The function itself, and not its end result, is the Church numeral 3. The Church numeral 3 means simply to do anything three times. It is an ostensive demonstration of what is meant by “three times”
” (Ref#: I).
Fixed-Point Combinators & Recursion
“Combinatory logic is a higher-order functions theory. A combinator is a closed lambda expression, meaning that it has no free variables. The combinators may be combined to direct values to their correct places in the expression without ever naming them as variables”(Ref: G). “In … combinatory logic, a fixed-point combinator (or fixpoint combinator) is a higher-order function fix that, for any function f that has an attractive fixed point, returns a fixed point x of that function. A fixed point of a function is a value that, when applied as the input of the function, returns the same value as its output”(Wikipedia). 
The Y Combinator, one of the fixed-point combinators in untyped lambda calculus, discovered by Haskell B. Curry, it is defined as: In the context of programming, it can be thought of as a way of doing recursion in a language which doesn’t have any recursion or any looping mechanism. Expressions can be defined recursively as below:
In the context of programming, it can be thought of as a way of doing recursion in a language which doesn’t have any recursion or any looping mechanism. Expressions can be defined recursively as below:|
1 2 3 |
<expression> := <name> | <function> | <application> <function> := λ<name>.<expression> <application> := <expression><expression> |
(Ref#: C) For some applications, terms for logical and mathematical constants and operations may be included.
The reduction operations include:
| Operation | Name | Description |
|---|---|---|
| (λx.M[x]) → (λy.M[y]) | α-conversion | Renaming the bound (formal) variables in the expression. Used to avoid name collisions. |
| ((λx.M) E) → (M[x:=E]) | β-reduction | Substituting the bound variable by the argument expression in the body of the abstraction |
Church–Rosser Theorem (Church & Rosser, 1936)
The Church–Rosser theorem states that “when applying reduction rules to terms in some typed variants of the lambda calculus, the ordering in which the reductions are chosen does not make a difference to the eventual result” (Wikipedia).
To put this another way, it asserts “that the λ-calculus is confluent under β-reductions. The standard proof of this result is due to Tait and Martin-Lof”(Ref#: D). “The Church-Rosser theorem states that lambda calculus as a reduction system with lambda conversion rules satisfies the Church-Rosser property“(Ref#: E). ” if a lambda-expression x can be reduced in two ways leading respectively to expressions y1 and y2 then there must be an expression z to which both y1 and y2 can be reduced. The choice of ways to reduce an expression arises from the possibility of separately reducing different “parts” of the expression.
The Church–Rosser theorem shows that either part can be worked on first, without the loss of any possibilities obtainable from starting with the other part. A corresponding theorem exists for combinatory logic.
More generally, any language for which there is a notion of reduction for expressions within the language is said to have the Church–Rosser property, or to be confluent, if it admits an appropriate version of the Church–Rosser theorem. The property plays an important role in term rewriting with equations” (Ref#: F).
Conclusion
The Lambda Calculus is an important idea which we see mapped to into functional programming languages and increasingly mixed programming languages. Understanding the theory and notation can help us to grasp the benefits of things like anonymous functions in programming languages.
References
A: Lambda Calculus – Computerphile. Retrieved from: https://www.youtube.com/watch?v=eis11j_iGMs
B: Lambda calculus. Retrieved from: https://en.wikipedia.org/wiki/Lambda_calculus
C: https://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf
D: https://www.cs.cornell.edu/~kozen/Papers/ChurchRosser.pdf
E: http://mathworld.wolfram.com/Church-RosserTheorem.html
F: https://www.encyclopedia.com/science-and-technology/mathematics/mathematics/church-rosser-theorem
G: https://en.wikipedia.org/wiki/Fixed-point_combinator
H: https://brilliant.org/wiki/lambda-calculus/
I: http://www.cse.unt.edu/~tarau/teaching/PL/docs/Church%20encoding.pdf
Updated: 1st June 2019
Comments