When Alonzo Church developed λ-calculus in the 1930s, it was a theoretical construct designed to create a formal system for the foundations of logic and mathematics that was simpler than Russell’s type theory and Zermelo’s set theory. This calculus was type-free with unrestricted quantification but without the law of excluded middle. However, it failed miserably due to the Kleene-Rosser Paradox which demonstrated that the calculus was inconsistent by showing that both a proposition and its negation could be derived from the same premises. The paradox exploited the calculus’ ability to encode self-referential constructions, leading to a contradiction that undermines the entire logical foundation. The calculus later evolved into a symbolic computational framework based on substitution and reduction, capable of performing any mechanical calculation. This is also known as the Church-Turing Thesis.
Several decades ago, when I first encountered λ-calculus, I fell in love with it—with its strangeness, simplicity, and elegance. Now that pair programming with an LLM is an option, I thought I could implement one. Actually, I created three: one I spitballed in clojure, a straightforward object-oriented implementation in Scala using classes and class inheritance, and yet another implementation again in Scala, but based on some magma, homomorphism, and catamorphism magic.
In this post, I am going to explain my view on the mathematical foundations of the subject in order to explain some of the weird choices I made in my last implementation in Scala.
I must clarify here: because the classical λ-calculus lacks double negation elimination
\[ \frac{(P\implies \bot)\implies \bot}{P} \]
(i.e., the Law of Excluded Middle), it models intuitionistic logic. Extending it to support classical logic requires additional constructs, such as control operators or continuation mechanisms, as found in the λμ-calculus of Parigot. The clojure version, and the OO version I implemented follows Parigot’s λμ-calculus, while the version I implemented on magmas is the classical λ-calculus.
To formally describe the syntactic structure of the untyped λ-calculus, we must first distinguish between two levels of representation: the concrete syntax, which consists of strings generated by a formal grammar, and the abstract syntax, which identifies the essential syntactic constructs free from superficial details such as parentheses or concrete variable names. The formalism of formal languages and abstract syntax trees provides a precise framework for this distinction.
The λ-calculus consists of three syntactic forms: variables, abstractions, and applications.
A variable can be any symbol, typically denoted by lowercase letters such as \(x\) or \(y\).
A function abstraction is written as \(\lambda x.M\) where \(x\) is the formal parameter and \(M\) is the function body. In this expression, the variable \(x\) is said to be bound. Any variable that appears in an expression but is not bound by a corresponding λ is called free.
A function application is of the form \(MN\), which denotes the application of function \(M\) to argument \(N\). Both \(M\) and \(N\) are themselves λ-terms.
The calculus is governed by three core equivalences:
Here \(M[x:=N]\) denotes substitution of \(N\) for all free occurrences of \(x\) in \(M\). From these simple rules emerges a computational system as powerful as any programming language or Turing machine.
Let us fix a countably infinite set of variable symbols \(\mathcal{V} = \{x, y, z, x_1, x_2, \dots\}\). The λ-calculus defines a formal language over this alphabet by means of a context-free grammar. In Backus–Naur Form (BNF), the set \(\Lambda\) of λ-expressions (or terms) is defined by the following production rules:
\[ \begin{array}{rl} M ::= & x \mid \lambda x. M \mid M\,M \end{array} \]
where \(x \in \mathcal{V}\). This grammar states that every term \(M \in \Lambda\) is either:
The formal language generated by this grammar is the smallest set \(\Lambda \subseteq \text{Expr}(\mathcal{V})\) satisfying the following inductive clauses:
Abstract syntax trees are inductively defined algebraic data structures that capture the hierarchical structure of expressions. The set of abstract syntax trees for λ-calculus corresponds to the following inductive type:
\[ \text{Term} ::= \begin{cases} \text{Var}(x) & \text{for } x \in \mathcal{V} \\ \text{Lam}(x, M) & \text{for } x \in \mathcal{V},\ M \in \text{Term} \\ \text{Appl}(M_1, M_2) & \text{for } M_1, M_2 \in \text{Term} \end{cases} \]
Thus, every λ-expression corresponds canonically to a binary
tree whose internal nodes are labeled by syntactic constructors
(abstraction, application), and whose leaves are variable names. The
concrete syntax, which includes parentheses, operator precedence, and
naming conventions, is merely a readable encoding of these trees. The
abstraction \(\lambda x. \lambda y.
x\,y\) corresponds, in its tree form, to nested Lam
and Appl nodes.
In categorical terms, one can view this abstract syntax as the free term algebra over the signature \(\Sigma = \{\text{Var}, \text{Lam}, \text{Appl}\}\), where each operation has arity \(\text{Var} : \mathcal{V} \to \text{Term}\), \(\text{Lam} : \mathcal{V} \times \text{Term} \to \text{Term}\), and \(\text{Appl} : \text{Term} \times \text{Term} \to \text{Term}\). The algebra of terms then supports structural induction and recursion principles naturally.
A magma is the most basic algebraic structure: a set equipped with a single binary operation. Formally, a magma is a pair \((M, \cdot)\), where \(M\) is a nonempty set and \(\cdot : M \times M \to M\) is a binary operation on \(M\). Crucially, the definition imposes no further conditions on the operation \(\cdot\): it need not be associative, commutative, nor admit an identity or inverse. In this sense, the magma is the minimal algebraic structure supporting binary composition. For example, the natural numbers \(\mathbb{N}\) with addition form a magma \((\mathbb{N}, +)\) that happens to be both associative and unital (with identity element \(0\)), but these additional properties are not required by the magma axioms.
Given a set \(A\), the free magma \(\mathsf{M}(A)\) generated by \(A\) is the initial object in the category of magmas under the forgetful functor to sets. It captures the formal, unrestricted compositions of elements of \(A\) under an abstract binary operation. The set \(\mathsf{M}(A)\) is defined inductively as the smallest set satisfying:
Here the binary operation \(\cdot\) is purely structural—it simply constructs a binary tree with two subtrees, without any semantic interpretation or computation. There is no requirement, for instance, that \((x \cdot y) \cdot z = x \cdot (y \cdot z)\), and hence the shape of the binary tree faithfully retains the syntactic structure of composition. The operation is not associative, commutative, or subject to any algebraic laws; it merely records the order and nesting of binary combinations. Consequently, the expression \(((a \cdot b) \cdot c)\) is distinct from \((a \cdot (b \cdot c))\), reflecting that the operation preserves the exact parenthesization structure as different tree shapes.
Algebraically, \(\mathsf{M}(A)\) consists of all finite binary trees whose leaves are labeled by elements of \(A\), and whose internal nodes are unlabeled and represent applications of the binary operation. Each such tree corresponds to a fully parenthesized expression over \(A\), where the parenthesization reflects the binary structure.
trait Magma[A]:
def op(x: A, y: A): A
extension (x: A) def $ (y: A): A = op(x, y)
enum BinTree[A]:
case Leaf(value: A)
case Branch(left: BinTree[A], right: BinTree[A])
object BinTree:
given binTreeMagma[A]: Magma[BinTree[A]] with
def op(x: BinTree[A], y: BinTree[A]): BinTree[A] = Branch(x, y)
def leaf[A](value: A): BinTree[A] = Leaf(value)This construction is particularly important in the formal semantics of programming languages and symbolic computation. The tree-like structure of syntax is thus formally grounded in the algebraic notion of a free magma.
We may now formalize the idea that the abstract syntax trees
(ASTs) of the untyped λ-calculus can be encoded as elements of
the type BinTree[Term[A]]. This representation captures the
recursive binary structure of applications, while variables and
λ-abstractions are encoded as atomic leaves carrying term-level
information.
The key idea is that application is now encoded not
as a syntactic form in the term data type, but as the structure of
the tree itself. That is, the binary tree serves as a free magma on
\(\mathsf{Term}(A)\), with the binary
operation corresponding to application. We define a Magma
instance on BinTree[A] where the binary operation
op(x, y) constructs the application of one term to another
by forming a Branch(x, y). Consequently, the expression
tree constructed by nested applications is built as a binary tree whose
leaves are labeled by atomic terms of type Term[A], and
whose internal nodes represent application.
Let us make the semantic correspondence precise with an example. If we write a term such as
\[ (\lambda x. x)\, (\lambda y. y) \]
then it is represented as:
case class Var[A](index: A)
case class Lambda[A](param: Var[A], body: BinTree[Term[A]])
type Term[A] = Either[Var[A], Lambda[A]]
Branch(
Leaf(Right(Lambda(Var("x"), Leaf(Left(Var("x")))))),
Leaf(Right(Lambda(Var("y"), Leaf(Left(Var("y"))))))
)In this structure:
Leaf(Right(...)) represents a λ-abstraction node,Leaf(Left(...)) represents a variable reference,Branch composes subterms via application.From the standpoint of universal algebra, we observe that the set
BinTree[Term[A]] is precisely the free
magma generated by the set Term[A], equipped with
the binary operation of application. The function Branch
serves as the magma’s binary operation, and Leaf(t) injects
atomic terms into the magma. This faithfully models the concrete
application structure of λ-calculus without conflating it with the
term constructors themselves.
The free magma structure models only the syntactic generation of λ-expressions: it captures the inductive formation of terms via variables, abstractions, and applications. However, the untyped λ-calculus is not, in a semantic sense, a free magma. This is because its equational theory includes nontrivial identifications among syntactic expressions, namely those induced by the reduction rules of α-, β-, and η-conversion. The presence of these equations requires quotienting the syntactic magma by the congruence they generate.
The syntactic structure of the untyped λ-calculus can be described algebraically as a magma generated by term constructors, subject to an equational theory defined by the rewriting rules of α-conversion, β-reduction, and η-conversion. This places λ-calculus within the tradition of algebraic presentations by generators and relations, analogous to defining a group as the quotient of a free group by the normal closure of relations.
We begin with the observation that the raw syntax of λ-terms—before any notion of reduction—is modeled by the free magma \(\mathsf{FM}(T)\), freely generated by the set \(T\) of atomic terms (variable symbols and λ-abstractions). The binary operation of the magma is application, denoted syntactically by juxtaposition or, in our formalization, by binary trees with application nodes. This free magma contains all well-formed binary trees over atomic terms and admits no identification beyond syntactic equality.
To define the λ-calculus proper, we impose an equational theory \(\equiv_{\alpha\beta\eta}\) generated by the rewriting rules of the \(\lambda\)-calculus. This theory induces a congruence on the free magma \(\mathsf{FM}(T)\). The quotient
\[ \Lambda := \mathsf{FM}(T) / {\equiv_{\alpha\beta\eta}} \]
is the set of λ-terms modulo computation. Application remains a well-defined binary operation on \(\Lambda\) because the congruence respects application:
\[ M_1 \equiv M_1',\quad M_2 \equiv M_2' \quad \Longrightarrow \quad M_1\, M_2 \equiv M_1'\, M_2'. \]
Hence, \(\Lambda\) inherits a magma structure from \(\mathsf{FM}(T)\), though it is no longer free: the imposed equations identify many syntactically distinct trees. The resulting structure \((\Lambda, \cdot)\) is a quotient magma, analogous to how a group defined by generators and relations is a quotient of the free group.
This analogy becomes illuminating when we examine the computational interpretation of composition. In group theory, multiplying two reduced words may produce a non-reduced word, which is then simplified using the group’s relations. For instance, if \(a^2 = e\), then the product \(a \cdot a \cdot b\) reduces to \(b\). The key property enabling this process to yield consistent results is confluence: any reduction sequence leads to a unique normal form (modulo equivalence). This ensures that group multiplication is well-defined on equivalence classes of reduced words.
The same principle holds in the λ-calculus. The Church–Rosser Theorem guarantees that the rewriting system generated by \(\rightarrow_{\alpha\beta\eta}\) is confluent: if a term \(M\) reduces to both \(M_1\) and \(M_2\), then there exists a term \(N\) such that \(M_1 \rightarrow^* N\) and \(M_2 \rightarrow^* N\). In other words, reduction paths are joinable:
\[ M \twoheadrightarrow M_1,\quad M \twoheadrightarrow M_2 \quad \Rightarrow \quad \exists N.\ M_1 \twoheadrightarrow N,\ M_2 \twoheadrightarrow N. \]
This ensures that any reduction strategy, as long as it terminates, yields a canonical representative of the equivalence class \([M]\). Composition of equivalence classes can therefore be implemented by composing representatives and reducing the result to normal form.
Thus, just as in the group-theoretic case, one may view the computation \([M] \cdot [N] := [M \cdot N]\) operationally as:
In other words, the Church-Rosser Theorem is equivalent to the following fact:
The subset of the free magma \(\mathsf{FM}(A)\) recognized by the language of \(\lambda\)-calculus is a magma with relations given by the reduction rules of the calculus.
The crucial point is that this procedure is well-defined precisely because the reduction system is confluent. In the absence of confluence, different reduction strategies could yield incomparable normal forms, and the quotient structure would be ill-posed.
A more effective approach to eliminate α-conversion is identifying a canonical representative of each α-equivalence class, which can be accomplished via the de Bruijn encoding. This encoding eliminates variable names entirely. In the de Bruijn representation, each variable occurrence is replaced by a natural number counting the abstractions between the variable occurrence and its binder. The innermost binder corresponds to index 0, the next outermost to index 1, and so on. For example:
\[ \lambda x. x \mapsto \lambda. 0, \qquad \lambda x. \lambda y. x \mapsto \lambda. \lambda. 1 \]
The key property of this encoding is that two λ-expressions are α-equivalent if and only if their de Bruijn representations are syntactically identical. Thus, the quotient by α-equivalence is canonically represented by nameless syntax.
This correspondence is formalized via a transformation:
\[ \mathsf{db} : \mathsf{BinTree}(\mathsf{Term}[A]) \to \mathsf{BinTree}(\mathsf{Term}[\mathbb{N}]), \]
where each leaf term Var(a) is replaced by
Var(n) for some \(n \in
\mathbb{N}\), computed with respect to its lexical depth. This
transformation is structure-preserving with respect to application, and
thus satisfies:
\[ \mathsf{db}(x \cdot y) = \mathsf{db}(x) \cdot \mathsf{db}(y), \]
where the operation \(\cdot\) corresponds to binary application, implemented via tree branching. The transformation on leaf terms is defined as:
\[ \mathsf{db}(\text{Leaf}(t)) = \text{Leaf}(\mathsf{db}_0(t)), \]
where \(\mathsf{db}_0\) converts variables to indices relative to their binding context. This requires an auxiliary context \(\Gamma \in \mathsf{List}[A]\), which maintains the ordered stack of currently bound variables. The transformation is defined recursively as:
\[ \begin{aligned} \mathsf{db}_\Gamma(\text{Var}(x)) &:= \text{Var}(n) \quad \text{where } x \text{ is at position } n \text{ in } \Gamma, \\ \mathsf{db}_\Gamma(\text{Lambda}(x, M)) &:= \text{Lambda}(0, \mathsf{db}_{x :: \Gamma}(M)), \\ \mathsf{db}_\Gamma(\text{Branch}(M_1, M_2)) &:= \text{Branch}(\mathsf{db}_\Gamma(M_1), \mathsf{db}_\Gamma(M_2)). \end{aligned} \]
The transformation \(\mathsf{db}_\Gamma\) thus replaces variable names with their de Bruijn indices in a manner consistent with lexical scoping and preserves the magma structure of application.
A catamorphism is the canonical homomorphism from an initial algebra into any other algebra of the same signature. It formalizes the notion of structural recursion or folding over inductively defined datatypes. In particular, if \(\mu F\) is the initial algebra of a functor \(F\), and \((A, \alpha: F(A) \to A)\) is an \(F\)-algebra, then there exists a unique morphism \([\alpha]: \mu F \to A\) making the diagram commute. This morphism \([\alpha]\) is the catamorphism induced by \(\alpha\), and it implements recursion over the structure of elements of \(\mu F\) by collapsing them into values of type \(A\) using the operations defined by \(\alpha\).
In the present setting, the inductive data structure under consideration is the term tree \(\mathsf{Expr}(A) := \mathsf{BinTree}(\mathsf{Term}[A])\), representing expressions in the untyped λ-calculus as binary trees of atomic terms. This structure is governed by the functor
\[ F_A(X) = A + X \times X, \]
where \(A = \mathsf{Term}[A]\) is the base set of leaf terms, and the inductive structure arises from the binary operation of application. A catamorphism over \(\mathsf{BinTree}(A)\) amounts to defining a function \(f : \mathsf{BinTree}(A) \to B\) such that
\[ f(\text{Leaf}(a)) = \phi(a), \quad f(\text{Branch}(x, y)) = f(x) \cdot f(y), \]
where \(\phi : A \to B\) and \(\cdot\) is the binary operation on \(B\) making it an algebra for \(F_A\).
The de Bruijn transformation \(\mathsf{db}_\Gamma : \mathsf{BinTree}(\mathsf{Term}[A]) \to \mathsf{BinTree}(\mathsf{Term}[\mathbb{N}])\) is an instance of such a catamorphism, albeit enriched by context sensitivity. It collapses the tree structure by applying a context-aware algebra:
\[ \alpha_\Gamma : \mathsf{Term}[A] + (\mathsf{BinTree}(\mathsf{Term}[A]) \times \mathsf{BinTree}(\mathsf{Term}[A])) \to \mathsf{BinTree}(\mathsf{Term}[\mathbb{N}]), \]
which operates as follows. If the node is a variable \(\text{Var}(x)\), it is mapped to \(\text{Var}(n)\) where \(x\) is at position \(n\) in \(\Gamma\). If the node is a λ-abstraction \(\text{Lambda}(x, M)\), it is mapped to \(\text{Lambda}(0, M')\), where \(M'\) is obtained by recursively applying the catamorphism to \(M\) under the extended context \(x :: \Gamma\). If the node is a binary application \(\text{Branch}(M_1, M_2)\), the catamorphism descends into both subtrees and reconstructs the application node via \(\text{Branch}(\cdot, \cdot)\).
Because the transformation satisfies
\[ \mathsf{db}_\Gamma(M_1 \cdot M_2) = \mathsf{db}_\Gamma(M_1) \cdot \mathsf{db}_\Gamma(M_2), \]
it is a homomorphism of magmas. Moreover, the threading of the context \(\Gamma\) throughout the recursion preserves binding structure and enables the transformation to compute de Bruijn indices correctly.
Although catamorphisms are typically defined for context-free structural recursion, the de Bruijn transformation is an example of a context-sensitive catamorphism, or more precisely a paramorphically enriched fold, where additional information (in this case, the context) is threaded through the recursion in a principled way. This form of structural recursion with state is well understood in categorical functional programming.
Thus, the de Bruijn transformation is a context-sensitive
catamorphism between two magmas: respectively between the subsets of
BinTree[Term[A]] and BinTree[Term[Int]]
recognized by the formal grammar of the \(\lambda\)-calculus. The tranformation
serves as a canonical normalization function that computes
representatives of α-equivalence classes in nameless form, thereby
eliminating the need for α-reduction as an explicit rewriting step. This
facilitates the definition of subsequent operations—such as substitution
and evaluation—in a purely structural and unambiguous manner.