Lambda calculus was originally created by Alonzo Church. It is the world’s smallest programming language. While it does not have numbers, strings, booleans, or any non-function datatype, it can represent any Turing machine.
Lambda calculus has 3 elements:
Functions exist, i.e
\[ square\_sum(x, y) = x^{2} + y^{2} \]
This can be understood as, "a tuple of x and y maps to \(x^{2} + y^{2}\). Well, with that being said:
\[ id(x) = x \]
can be rewritten to its anonymous form, which is
\[ x \mapsto x \]
This is supposed to demonstrate the fact that lambda calculus only uses functions with a single input. Functions that require more than one can be rewritten to functions with one argument, but return another function, which also then returns a single input. For example:
\[ (x, y) \mapsto x^{2} + y^{2} \]
can be reworked into
\[ x \mapsto ( y \mapsto x^{2} + y^{2} ) \]
This is known as currying: transforming a function that takes multiple arguments into a chain of functions each with a single argument. Below is a expanded function application of a curried function as an example.
\[ \begin{aligned} & ((x \mapsto ( y \mapsto x^{2} + y^{2} ))(5))(2) \\ & = (y \mapsto 5^{2} + y^{2})(2) \\ & = 5^{2} + 2^{2} \\ & = 29 \end{aligned} \]
Lambda calculus consists of lambda terms and transformation rules which allow for manipulation of the terms. Functions in lambda calculus are anonymous (not named). They take in only one variable and leverage currying to implement functions that would otherwise use multiple variables.
What is a lambda term? A lambda term is defined as a valid lambda calculus expression. There are a few rules that allow you to precisely verify whether something conforms to lambda term syntax, however, the basic gist is that the syntax is composed of the 3 elements outlined earlier: variables, abstractions (functions), and applications (think of invoking functions). Nothing else is a lambda term.
What is an abstraction? An abstraction \(\lambda x.t\) is an anonymous function that takes a single input, replacing the body (expression \(t\)) with the input where it occurs. The function/abstraction just sets up the function, it does not invoke it.. The abstraction \(\text{\underline{binds}}\) the variable \(x\) in the term \(t\).
What is an application? An application is simply the calling of a function.
There is no concept of variable declaration in lambda calculus. Dangling “variables” are just unknown values.
Functions in lambda calculus are first-class values. What does this mean? It means you can use the functions as inputs and outputs from other functions. It’s also worth noting that function application in lambda calculus is left-associative, this means stx would act as (st)x.
Lambda calculus consists of constructing lambda terms and performing reduction operations on them. There are two types of reduction.
| Names | Descriptions |
|---|---|
| \(\alpha\) conversion | Renaming the bound variables in the expression. Used to avoid naming collisions |
| \(\beta\) reduction | Replacing the bound variables with the argument expression in the body of the abstraction. |
The idea behind alpha equivalence merely is that the naming of variables in abstractions doesn’t really matter. Variables by themselves, though, such as x and y are not said to be alpha-equivalent since they are not bound in an abstraction where they would evaluate to the same expression.
It is important to note a few terms before defining \(\beta\)-Reduction.
Ok, so what are \(\beta\)-reductions?. The \(\beta\)-reduction is simply stating that: \((\lambda x, t)s\) reduces to \(t[x := s]\), which simply means replace the body \(t\) that has any input \(x\) with the value passed in from the invocation \(s\).
This may remind you of functional programming languages like OCaml. It’s almost like a computation. It seems beta reductions can be applied continuously such that it eventually terminates. Though, it is very possible to have an abstraction such as \((\beta x, xx)\), where subsequent beta reductions would never terminate the reduction process. This is a property of untyped lambda calculus, but not typed lambda calculus. Another difference between these two types of lambda calculus is that untyped lambda calculus doesn’t care what kind of data it’s working with. Typed lambda calculus does, i.e. if you wanted an abstraction that only worked on numbers. In untyped lambda calculus there is no way to constrain it to certain types of inputs.
Combinators are simply \(\lambda\)-terms that do not have free variables. There are a few special combinators. Here are some: