λ-Calculus – optimix

The untyped λ-calculus is a formal system in mathematical logic that expresses computations. Each computation is presented as a term, and terms may themselves be composed of additional terms. Every term is either a variable, an abstraction or an application. Evaluating a program is equivalent to starting with a term and performing a series of substitutions, based on a set of formal rules.

Grammar

The ABNF grammar for the untyped λ-calculus is shown below. For simplicity, we assume that whitespace is not significant except as a delimiter between terms (where needed).

term := var | abs | app
abs  := "λ" var "." term
app  := term term

Example

Given below is an example of a well-formed term, where $x$ , $y$ and $z$ are variables, $\lambda x.x$ and $\lambda xy.xyz$ are abstractions, $xyz$ and the term as a whole are applications. Here, we take the liberty of assuming that $xy$ actually denotes two separate variables (the application of $x$ to $y$ ).

(\lambda x.x)(\lambda xy.xyz)

Note that there are actually four variables in this expression – the $x$ variables in the two parenthesized terms are completely unrelated as they are bound to different abstractions. When a variable is not bound to any abstraction, it is said to be free.

\left(\overbrace{\lambda x.\underbrace{x}_{\text{\footnotesize Bound Variable}}}^{\text{\footnotesize Abstraction}}\right)\left(\overbrace{\lambda xy.xy\underbrace{z}_{\text{\footnotesize Free Variable}}}^{\text{\footnotesize Abstraction}}\right)

Substitution Rules

α-conversion

Within the scope of an abstraction, a bound variable may be freely substituted with any symbol that isn’t already in use (which means it is neither free nor bound within the current context). This is known as an α-conversion. For instance, the example above is equivalent to the following expressions.

\left(\lambda x.x\right)\left(\lambda wk.wkz\right)

\left(\lambda y.y\right)\left(\lambda xy.xyz\right)

However, it is not equivalent the following expression, as it inadvertently converts the free $z$ into a bound one.

\left(\lambda x.x\right)\left(\lambda zy.zyz\right)

β-reduction

When an abstraction is applied to a term, the former can be reduced by substituting every occurrence of the first bound variable of the abstraction with the term it is applied to. This is known as a β-reduction. In traditional programming languages, this corresponds to function application, converting a complex expression into something simpler. Our original example above reduces to the following.

\left(\lambda x.x\right)\left(\lambda wk.wkz\right)\xrightarrow{β}\lambda wk.wkz

The first term, $(\lambda x.x)$ , is equivalent to a function that returns its argument as-is – the identity function. Applying the identity function to the second term simply returns the second term.

Note that β-reduction doesn’t always simplify the term. In some cases, further reduction may yield the same term ad infinitum, in which case the term is said to be in a ‘minimal form’. In other cases, the term may actually become bigger with each reduction, in which case it is said to diverge. In all other cases, when no further β–reduction is possible, the term is said to be in β-normal form.

\left(\lambda x.x x\right)\left(\lambda x.x x\right) \tag{\text{Minimal}}

\left(\lambda x.xxy\right)\left(\lambda x.xxy\right) \tag{\text{Divergent}}

Writing an interpreter for the untyped λ-calculus is relatively straightforward in Haskell.

Preparation

Make sure the stack is installed on your system.
Clone the package from GitHub to run the code.

$ git clone https://github.com/rri/untype.git
$ cd untype
$ stack build
$ stack test
$ stack exec -- untype

A Quick Walkthrough

Link to GitHub

The core data structure to represent terms mimics the ABNF grammar described earlier. This recursive type declaration is easy to define in Haskell, as it uses a non-strict evaluation strategy.

data Term
    = Var Sym       -- ^ Variable
    | Abs Sym Term  -- ^ Abstraction
    | App Term Term -- ^ Application
    deriving (Eq)

For contrast, a similar data structure in Rust would have looked like this (notice the Box type that adds a level of indirection).

pub enum Term {
    Var(Sym),
    Abs(Sym, Box<Term>),
    App(Box<Term>, Box<Term>),
}

The general strategy here is to accept an expression as newline-terminated text, apply a parser to the input to derive an abstract syntax tree, apply α-conversion and β-reduction strategies on the term until it converges, and then finally print it to the screen.

We use attoparsec, a nifty parser-combinator library, to write simple parsers and combine them into larger ones. As we apply a few basic parsers recursively, we need to look out for a few gotchas, called out in the code, that might cause the parser to loop indefinitely or give us incorrect results.

Finally, determining when to generate fresh variables and how to name them is surprisingly challenging. Here is an example when variable names must be substituted prior to reduction.

\overbrace{\left(\lambda x y.x y y\right)}^{\text{\footnotesize Term 1}}\overbrace{\left(\lambda u.u y x\right)}^{\text{\footnotesize Term 2}}

Here, Term 2 needs to replace the $x$ within Term 1 as part of the β-reduction step. However, Term 2 already has a $y$ , conflicting with the $y$ – a distinct bound variable – in Term 1. We therefore need to replace the $y$ in Term 1 with a fresh variable, and only then proceed with the substitution.

We leverage a simple strategy for generating fresh variables. First, we collect free variables across the whole term. Then, as we traverse the term, we keep track of all bound variables in the current context. Whenever we need a fresh variable, we take the original and append an apostrophe (') at the end. We then check this new variable against the list of free variables as well as the list of bound variables in the current context. If there are no collisions, we’re done; if not, we repeat the process.

That’s all for today, folks! 🖖

Tag: λ-Calculus

The Untyped λ-Calculus