The \(\lambda\)-calculus (lambda calculus) is often described as the world’s smallest universal programming language. It was introduced in the 1930s by Alonzo Church and is a formal system for expressing computation based on function abstraction and application (the two concepts that will be discussed in detail later in this report). [1]
The primary motivation behind \(\lambda\) calculus is that any program (and hence any programming language) can be theoretically studied using \(\lambda\) calculus. This result follows from the conclusion that untyped lambda calculus is Turing complete, as stated by the (Church-Turing) thesis. Consequently, most functional programming languages are based upon the lambda calculus - including Haskell and Racket as we have seen in CSCC24. [2]
The \(\lambda\) calculus consists of three fundamental elements: variables, function abstraction, and function application.
Parentheses may also be used to make grouping explicit when
necessary. (eg. MNP is interpreted as (MN)P.)
To generalize the syntax, consider the following Context-Free Grammar (CFG) for the \(\lambda\) calculus [3]:
C = (\(\Sigma\), V, S, P), where
\(\Sigma = \{\lambda, ., (, ), a, b, c,...., z\}\)
\(V = \{\text{<expr>, <var>, <function>, <application>}\}\)
\(S = \text{<expr>}\)
\(P:\)
\(\text{<expr>} \to
\text{<var>} \mid \text{<function>} \mid
\text{<application>} \mid \text{(<expr>)}\)
\(\text{<function>} \to \lambda \
\text{<var>}.\text{<expr>} \qquad{\text{*}}\)
\(\text{<application>} \to
\text{<expr><expr>}\)
\(\text{<var>} \to a \mid b \mid c \mid
\dots \mid z\)
Now that we have defined the syntax, we consider how functions are represented and evaluated in the \(\lambda\)-calculus and we also formalize the definition of function application and abstraction.
Consider a simple function in calculus, \(f(x) = x\). This is the identity function, i.e, the output is the same as the input. In \(\lambda\)-calculus, this is encoded as the following abstraction:
\[\lambda x. x\]
This is an example of a function abstraction, the variable \(x\) following the \(\lambda\) is the parameter, and the expression, in this case \(x\) after the dot is the body.
Now, if we want to apply this function on an input, we use function application. To apply this function to an expression, for example the some constant \(a\), this would be written as:
\((\lambda x.x) a\)
In order to correctly perform substitution, it is important to distinguish between free and bound variables.
Example 1: \[\lambda x. x \ y\]
Here, \(x\) is bound, while \(y\) is free.
Example 2: \[x (\lambda x.x)\]
Here, the first x (outside the parantheses) is free. The second x (inside the body of the abstraction) is bound by \(\lambda x\) immediately preceding it.
Additionally, in a \(\lambda\)-expression, the specific name of a bound variable does not affect the meaning of the function. Two \(\lambda\)-expressions are considered \(\alpha\)-equivalent if they differ only by the names of their bound variables. The process of replacing the variables is called \(\alpha\)-reduction.
For example, the following are all \(\alpha\)-equivalent:
\[\lambda x. x \equiv_\alpha \lambda y. y \equiv_\alpha \lambda z. z\]
[4] We now formalize this process of evaluation. In general, applying a function to an argument is performed using \(\beta\)-reduction, defined as:
\[ (\lambda x. M)\ N \to_\beta M[x := N] \]
Here, all free occurrences of \(x\) in \(M\) are replaced with the expression \(N\). The notation \(M[x := N]\) formally expresses this substitution.
Example 1: \[ (\lambda x. x)\ a \to_\beta a \]
The bound variable \(x\) in the body is replaced by the argument \(a\). The variable \(y\) is free, so it remains unchanged during the reduction.
\[ (\lambda x.x \ x) y \to_\beta y \ y\]
In this case, the function duplicates its input. Both free occurrences of \(x\) in the body \((x x)\) are replaced by the argument y.
In the \(\lambda\)-calculus, all functions take exactly one argument. Functions with multiple arguments are represented using currying, where functions return other functions.
For example, a function of two variables can be written as:
\[\lambda x. \lambda y. x\]
This function takes an argument \(x\) and returns a new function that takes \(y\) and returns \(x\).
\[(\lambda x. \lambda y. x)\ a\ b \to_\beta (\lambda y. a)\ b \to_\beta a\]
\[(\lambda x. \lambda y. x \ y)\ f\ z \to_\beta (\lambda y. f \ y)\ z \to_\beta f \ z\]
This demonstrates how multi-argument functions are encoded through nested abstractions.
The motivation for the first example is Boolean Values. As it can be seen from CFG, there is not inherently defined identifiers True, or False, but it can be encoded with lambda calculus by the function that chooses between two arguments. True always chooses the first argument and False chooses the second argument. This might seem a bit unintuitive, but examples below would provide a better understanding [5].
Informally, we can think of it as \(\lambda b. b \ F \ T\) i.e., Not = \(\lambda b . b \ \lambda x. \lambda y. y \ \lambda x. \lambda y. x\)
We will use shortened version of Not, False as F, and True as T:
Not = \(\lambda b. b \ F \ T\)
Apply Not with True:
\[ (\lambda b. b \ F \ T) \ T \to_\beta (T \ F \ T) \]
\[ (T \ F \ T) \to_\beta F \qquad[\text{Since T returns the first argument}]\]
Similarly,
\[ (\lambda b. b \ F \ T) \ F \to_\beta (F\ F \ T) \]
\[ (F\ F \ T) \to_\beta T \qquad[\text{Since F returns the second argument}]\]
The logical AND operation returns True if both operands are True, and False otherwise.
And = \(\lambda p. \lambda q. p \ q \ F\) where \(F\) is the False encoding: \(\lambda x. \lambda y. y\)
Informally, we can think of it as: “If \(p\) is True, return q; otherwise if p is False return False.
True AND True:
\[ (\lambda p. \lambda q. p \ q \ F) \ T \ T \]
\[\to_\beta (\lambda q. T \ q \ F) \ T\]
\[\to_\beta T \ T \ F\]
\[\to_\beta T \qquad [\text{Since T selects the first argument, which is T}]\]
True AND False: \[(\lambda p. \lambda q. p \ q \ F) \ T \ F\]
\[\to_\beta (\lambda q. T \ q \ F) \ F\]
\[\to_\beta T \ F \ F\]
\[\to_\beta F \qquad [\text{Since T selects the first argument, which is F}]\]
False AND True:
\[(\lambda p. \lambda q. p \ q \ F) \ F \ T\]
\[\to_\beta (\lambda q. F \ q \ F) \ T\]
\[\to_\beta F \ T \ F\]
\[\to_\beta F \qquad [\text{Since F selects the second argument, which is F}]\]
False AND False:
\[(\lambda p. \lambda q. p \ q \ F) \ F \ F\]
\[\to_\beta (\lambda q. F \ q \ F) \ F\]
\[\to_\beta F \ F \ F\]
\[\to_\beta F \qquad [\text{Since F selects the second argument, which is F}]\]
Notably, because of the absence of loops, we relied on recursion heavily in our functional programming paradigm in this course. Since, lambda calculus is claimed to be the foundation of functional programming, it should also encode recursion.
Recursion as we’ve seen so far, requires a function to have a call to itself (with a different argument). However, in lambda calculus, we don’t have the notion of a “named” function since all the functions are lambda terms (anything that can be encoded by the CFG presented) and so it seems to be a challenge to encode recursion. This challenge makes us appreciate the following lambda function even more. Here’s the encoding for recursion in lambda calculus, also famously known as Y-Combinator.
\(\lambda f. \ (\lambda x. f (x \ x)) \ (\lambda x.f(x \ x))\)
For the sake of presentation, we name this as \(Y\). An important thing to note here is that Y-combinator has a unique property i.e., \(Y F\) is equivalent to \(F(Y F)\) which will be used in the example to follow. To see this, consider the following:
\(Y F\) = \(\lambda f. \ (\lambda x. f (x \ x)) \ (\lambda x.f(x \ x)) F \quad[{\text{replacing Y with its } \lambda \text{ expression}}]\)
\(\lambda f. \ (\lambda x. f (x \ x)) \ (\lambda x.f(x \ x)) F \to_\beta (\lambda x. F (x \ x)) \ (\lambda y.F(y \ y)) \quad[{\beta \text{-reduction and } \alpha \text{-reduction}}]\)
\((\lambda x. F (x \ x)) \ (\lambda y.F(y \ y)) \to_\beta F \ ((\lambda \ y.F(y \ y)) (\lambda y.F(y \ y))) \quad[{\beta \text{-reduction}}]\)
\(F \ ((\lambda \ y.F(y \ y)) (\lambda y.F(y \ y))) = F \ (Y \ F) \quad[\text{by definition of Y}]\)
For the sake of presentation, we’re referencing the encoding of true as T, and false as F, so
T = \(\lambda x. \lambda y. x\),
F = \(\lambda x. \lambda y. y\)
The motivation for this example is to simulate the behavior of a while loop using lambda calculus. In a typical while loop, the body is executed when the condition of while loop is satisfied, and the process repeats until the condition becomes false.
To simulate this behavior, we define a function that:
Consider the following \(\lambda\) function,
\(\lambda r. \ \lambda b.b \ s \ (r \ T)\), and let’s name it as G
Here, r represents the recursive call, b represents the boolean condition and s represents the final result.
Here, the termination happens when b = T, and recursion happens when b = F.
Now, consider the function:
\(Flip = Y G\),
where \(Y\) refers to the \(Y\)-combinator defined previously.
$Flip F (Y G) F (G(YG)) F $
\((G(YG))\ F \to_\beta (\lambda b.\ b\ s\ ((YG)\ T))\ F \qquad [\text{by applying G to YG}]\)
\((\lambda b.\ b\ s\ ((YG)\ T))\ F \to_\beta F\ s\ ((YG)\ T) \qquad [\text{by }\beta\text{-reduction}]\)
\(F\ s\ ((YG)\ T) \to_\beta (YG)\ T \qquad [\text{F selects the second argument}]\)
\((YG)\ T \to_\beta (G(YG))\ T \qquad[\text{property of the } Y\text{-combinator}]\)
\((G(YG))\ T \to_\beta (\lambda b.\ b\ s\ ((YG)\ T))\ T \qquad [\text{by definition of G}]\)
\((\lambda b.\ b\ s\ ((YG)\ T))\ T \to_\beta T\ s\ ((YG)\ T) \qquad [\text{by }\beta\text{-reduction}]\)
\(T\ s\ ((YG)\ T) \to_\beta s \qquad[\text{T selects the first argument}]\)
The process above can be intuitively observed as follows:
Starting with F, the computation performed recursion once like the condition of while loops allow execution of body,
The next step evaluated T
When T is reached, it terminates and returns s.
[1]R. Rojas, “A Tutorial Introduction to the Lambda Calculus.” Available: https://personal.utdallas.edu/~gupta/courses/apl/lambda.pdf
[2]Wikipedia Contributors, “Lambda calculus,” Wikipedia, Jan. 02, 2020. https://en.wikipedia.org/wiki/Lambda_calculus
[3]“Lambda Calculus — Programming Language Principles and Paradigms 0.4 documentation,” Github.io, 2016. https://eecs390.github.io/notes/theory.html
[4]J. Alama and J. Korbmacher, “The Lambda Calculus (Stanford Encyclopedia of Philosophy),” Stanford.edu, 2012. https://plato.stanford.edu/entries/lambda-calculus/
[5]“Learn Lambda Calculus in Y Minutes,” Learnxinyminutes.com, 2025. https://learnxinyminutes.com/lambda-calculus/