Untyped Lambda Calculus

Since 2015, I have taught lectures at ITMO University that are connected in one way or another with functional programming. The first few lectures are usually devoted to the untyped lambda calculus, its construction, and the problems that can be solved with it. Students tend to struggle with such purely theoretical material and only truly grasp it when asked to implement the lambda calculus themselves. It therefore seems interesting to try to ~~combine the unpleasant with the useless~~ explain the calculus and implement it at the same time. Completeness and depth will naturally suffer, but for a proper theoretical understanding there is Barendregt, or—modestly—my lectures. Here, we will concentrate on the practical side.

Let us begin by introducing a formal language for describing lambda-calculus terms. The simplest elements of the calculus are variables: members of a set $V = {x, y, z, \ldots}$ of arbitrary symbols from the Latin alphabet. Any such variable is already considered a term:

x \in V \Rightarrow x \in \Lambda.

Another essential condition in the construction of any calculus is that a term in parentheses is also a term:

t \in \Lambda \Rightarrow (t) \in \Lambda.

We can already construct an infinite set of terms:

x, y, (x), ((x)), (((z))), \ldots

This is clearly not what we ultimately want, because our calculus must be able to express any computation. We therefore need more kinds of formulas. One intuitive and natural construction is application. A term representing a function is applied to some term representing an argument, producing a new term. In the lambda calculus, this is expressed as:

m, n \in \Lambda \Rightarrow (m \, n) \in \Lambda,

which enables us to write still more meaningless constructions:

(x \, y), ((x \, y) z), ((x \,y) z) (m n), \ldots

The final and extremely important construction is the abstraction of a term over a variable, which expresses the dependence of a function on its argument. For historical reasons, it is written with the letter $\lambda$ , which gave the calculus its name:

x \in V, m \in \Lambda \Rightarrow \lambda x. m \in \Lambda.

Assuming that we have some named terms—such as plus, prod, and pow—representing the corresponding operators (+, *, and ^), we can write an arbitrary arithmetic function:

f(x,y) = x^2 + 3 \cdot y \rightarrow \lambda x.\lambda y.((plus ((pow \, x) 2)) ((prod \, 3) y))

The abundance of parentheses makes the expression completely unreadable, so let us introduce a few conventions to simplify the notation. First come the associativity rules. We treat application as left-associative and abstraction as right-associative:

\begin{aligned} (m n) (k) = m \, n \, k \\ \lambda x. \lambda y. m = \lambda x \, y. m \end{aligned}

The same construction can now be written more briefly and clearly:

f(x,y) = x^2 + 3 \cdot y \rightarrow \lambda x \, y. plus \, (pow \, x \, 2) (prod \, 3 \, y)

To put parentheses even further out of mind, let us think of terms not as strings but as syntax trees. The rules for translating terms into trees are as follows:

Term	Tree
$x$
$m \, n$
$\lambda x. m$

Our function $f$ can now be represented by the following syntax tree:

We will encode such trees using algebraic data types:

import Data.Text (Text)

data Term = Var Text       -- variables
          | App Term Term  -- application
          | Lam Text Term  -- abstraction
  deriving (Show)

To construct the term $f$ , we also need support for the numeric literals 2 and 3. We could add them to the calculus with another constructor such as Lit Int, or simulate them with the variables two and tree:

{-# LANGUAGE OverloadedStrings #-}

f :: Term
f = Lam "x" (Lam "y" (App (App (Var "plus") xSqr) p3y))
  where xSqr = App (App (Var "pow") (Var "x")) (Var "two")
        p3y  = App (App (Var "prod") (Var "tree")) (Var "y")

The resulting expression is again overrun with parentheses and generally hard to digest.

Printing terms

To make this bearable, we should immediately write a pretty-printer that displays our terms nicely. Let us begin with a simple implementation that prints every pair of parentheses:

import Data.Monoid ((<>))

pretty :: Term -> Text
pretty (Var name)     = name
pretty (App algo arg) = "(" <> pretty algo <> " " <> pretty arg <> ")"
pretty (Lam var body) = "λ" <> var <> "." <> pretty body

The output can now be read, but the unnecessary parentheses clearly remain an obstacle:

ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx.λy.((plus ((pow x) two)) ((prod tree) y))

Parentheses must be removed around an application in three cases: when it is at the top level, when it is the algorithm (algo) of another application, and when it is the body of an abstraction. Let us modify our function accordingly:

data Parens = ParensLess | ParensFull

pretty :: Term -> Text
pretty = pretty' ParensLess
  where
    pretty' :: Parens -> Term -> Text
    pretty' _          (Var name)     = name
    pretty' ParensLess (App algo arg) = pretty' ParensLess algo <> " " <> pretty' ParensFull arg
    pretty' ParensFull app@(App _ _)  = "(" <> pretty' ParensLess app <> ")"
    pretty' _          (Lam var body) = "λ" <> var <> "." <> pretty' ParensLess body

We now obtain clear, attractive output:

ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx.λy.plus (pow x two) (prod tree y)

The final touch is to compress nested lambdas into one. This should happen whenever the current lambda is the body of another lambda. The general logic is this: if a lambda lies in another lambda's body, add its variable to the variable list; once the chain of lambdas ends, insert a full stop and print the body. Here is the implementation:

data Position = AppAlgo | AppArg | LamBody | Other

pretty :: Term -> Text
pretty = pretty' Other
  where
    prettyLB :: Term -> Text
    prettyLB (Lam var body) = var <> pretty' LamBody body
    prettyLB _              = undefined
    
    pretty' :: Position -> Term -> Text
    pretty' LamBody lam@(Lam _ _)  = " " <> prettyLB lam
    pretty' AppAlgo lam@(Lam _ _)  = "(" <> pretty' Other lam <> ")"
    pretty' _       lam@(Lam _ _)  = "λ" <> prettyLB lam
    pretty' LamBody term           = "." <> pretty' Other term
    pretty' _       (Var name)     = name
    pretty' AppArg  app@(App _ _)  = "(" <> pretty' Other app <> ")"
    pretty' _       (App algo arg) = pretty' AppAlgo algo <> " " <> pretty' AppArg arg

And the final output:

ghci> import Data.Text.IO as TIO
ghci> TIO.putStrLn (pretty f)
λx y.plus (pow x two) (prod tree y)

Reading terms

Besides attractive output, we need a way to enter terms into our calculator, because typing something like Lam "x" (Lam "y" (App ( is no fun at all. We therefore need a parser for lambda terms. Ideally, it should be able to parse any compact output from pretty, satisfying the following law:

parse \circ pretty = id

In reality, of course, we must handle syntax errors and related concerns, so our parse function will be slightly more complicated. Our parsing strategy is as follows: we treat every term as a potential application—that is, several consecutive terms. The application is only potential because there may be a single term, in which case it is not an application at all. We call a term that is not an application a natural term:

\begin{align*} term &::= {natural \, term}^n \\ natural \, term &::= (term) | variable | abstraction \end{align*}

Let us begin the implementation by importing the necessary parsing modules. I use my favourite, attoparsec; the approach is the same with classic parsec or fashionable but slow megaparsec. We will also write several helper functions.

import           Control.Applicative ((<$>), (<*>), (<|>))
import           Control.Monad       (void)
import           Data.Text           (Text, pack)
import           Data.Attoparsec.Text

-- One or more consecutive spaces
spaces :: Parser ()
spaces = void $ many' space

-- Parses an expression and every space after it, discarding the spaces.
spaced :: Parser a -> Parser a
spaced x = x <* spaces

-- Parses one full stop and discards the parser output.
dot :: Parser ()
dot = void $ spaced (char '.')

-- Parses a lambda symbol, \\ or L, and discards the parser output.
lambda :: Parser ()
lambda = void $ spaced (char '\\' <|> char 'λ' <|> char 'L')

-- Parses an expression in parentheses; spaces before the opening and
-- after the closing parenthesis are accepted and consumed.
parens :: Parser a -> Parser a
parens x = spaced (char '(') *> x <* spaced (char ')')

-- Parses a string that begins with a Latin letter and contains
-- Latin letters, digits, and the ' symbol.
name :: Parser Text
name = (pack .) . (:) <$> oneOf ['a'..'z'] <*> many' (letter <|> digit <|> char '\'')
  where
    oneOf = choice . (char <$>)

We can now implement the functions that read a term and a natural term as defined above:

-- Reads at least one natural term; if there is more than one,
-- combines them into an application using left associativity.
term :: Parser Term
term = foldl1 App <$> many1 (spaced naturalTerm)

-- Reads either a parenthesised term that may contain an application,
-- a variable, or a lambda abstraction.
naturalTerm :: Parser Term
naturalTerm = parens term <|> variable <|> abstraction

Only two parsers remain: one for variables and one for abstractions. They are just as straightforward as the parsers above:

-- Parses one variable.
variable :: Parser Term
variable = Var <$> name

-- Parses a lambda abstraction: a lambda symbol, at least one variable,
-- a full stop, and the term that forms the abstraction's body; folds
-- the variables into nested lambda abstractions by right associativity.
abstraction :: Parser Term
abstraction = do lambda
                 vars <- many1 (spaced name)
                 dot
                 expr <- term
                 pure $ foldr Lam expr vars

We can test our parsers with this function:

parseTerm :: Text -> Either String Term
parseTerm = parseOnly term

In the interpreter, let us check that everything is read correctly:

ghci> :set -XOverloadedStrings
ghci> Right t = parseTerm "λx y.plus (pow x two) (prod tree y)"
ghci> t
Lam "x" (Lam "y" (App (App (Var "plus") (App (App (Var "pow") (Var "x")) (Var "two"))) (App (App (Var "prod") (Var "tree")) (Var "y"))))
ghci> pretty t
λx y.plus (pow x two) (prod tree y)

Giving the calculus meaning

It is time to give our calculus meaning. To do that, we need to introduce several rules for rewriting terms into other terms; we will regard these rewrites as computations.

First, a couple of definitions. Depending on whether a variable occurs beneath a lambda symbol in an abstraction, we divide variables into free and bound variables. Let us begin with an intuitive example:

(\lambda \color{red}x \color{black}. (\lambda \color{green}x \color{black}. \color{green}x \color{black} \, y) \, \color{red}x \color{black}) \, \color{blue}x

The differently coloured occurrences of $x$ are “bound” by different lambdas. One intuitive way to trace this is to remove lambdas one at a time: doing so “frees” a variable because its name no longer denotes an argument of a function. After that rather vague explanation, let us give a proper definition. For an arbitrary term $t$ , its set of free variables $FV(t)$ is constructed by the following rules. From this point onward, assume that $x \in V$ and $M, N \in \Lambda$ :

\begin{align*} FV(x) &= \{x\} \\ FV(M \, N) &= FV(M) \cup FV(N) \\ FV(\lambda x. M) &= FM(M) \backslash \{x\} \end{align*}

The set $BV(t)$ of bound variables is defined similarly:

\begin{align*} BV(x) &= \varnothing \\ BV(M \, N) &= FV(M) \cup FV(N) \\ BV(\lambda x. M) &= BV(M) \cup \{x\} \end{align*}

The corresponding Haskell functions reproduce the definitions exactly:

import Data.Set (Set, delete, empty,
                 insert, singleton, union)
                 
free :: Term -> Set Name
free (Var var)      = singleton var
free (App algo arg) = free algo `union` free arg
free (Lam var body) = var `delete` free body

bound :: Term -> Set Name
bound (Var var)      = empty
bound (App algo arg) = bound algo `union` bound arg
bound (Lam var body) = var `insert` free body

The lambda calculus has only one non-trivial axiom: two terms are equal if they differ only in the names of their bound variables. The following terms are therefore equal:

\lambda \color{red}x \color{black} \, \color{green}y \color{black} . \color{red} x \color{black} = \lambda \color{red}z \color{black} \, \color{green}w \color{black} . \color{red} z \color{black} = \lambda \color{red}y \color{black} \, \color{green}x \color{black} . \color{red} y \color{black}

We will implement this by making our terms an instance of the Eq type class:

instance Eq Term where
  Var a == Var b        = a == b
  App a b == App a' b'  = a == a' && b == b'
  Lam v b == Lam v' b'  = b == substitute b' v' (Var v)
  _ == _                = False

This requires an additional substitution function that can replace variable names. In fact, we will implement a much more powerful form of substitution, capable of replacing every free occurrence of a variable with an arbitrary term. The lambda calculus has a conventional formal definition for this operation.

The substitution $M[x:=N]$ of a term $N$ for every free occurrence of the variable $x$ in the term $M$ is the term formed according to the following rules. As usual, $x \in V$ and $M, N, P, Q \in \Lambda$ :

\begin{align*} x[x:=N] &= N \\ y[x:=N] &= y \\ (P \, Q)[x:=N] &= (P[x:=N]) \, (Q[x:=N]) \\ (\lambda x. M)[x:=N] &= \lambda x. M \\ (\lambda y. M)[x:=N] &= \lambda y. (M[x:=N]), \text{ if } x \not\in FV(N) \end{align*}

The last rule has an additional condition. If we ignore it, some substitutions produce an unpleasant consequence: a change in the term's structure known as variable capture.

(\lambda x.y)[y:=x] = \lambda x.x \, \color{red}\text{(this is false!)}

There are several ways to solve the variable-capture problem:

Use different alphabets for bound and free variables—the Barendregt convention. This is a rich idea but difficult to implement in practice.

(\lambda \color{red}x' \color{black}. (\lambda \color{green}y' \color{black}. \color{green}y' \color{black} \, \color{red}x' \color{black}) \, \color{red}x' \color{black}) \, \color{blue}x

Remove the names of bound variables entirely and replace them with numbers indicating how many lambdas back the variable was bound. This representation is called de Bruijn indices, or de Bruijn notation, and is used in most programming languages because of its computational efficiency.

(\lambda (\lambda \color{green}1\color{black} \, \color{red}2\color{black}) \, \color{red}1 \color{black}) \, \color{blue}x

We will take a third route: whenever we encounter a substitution conflict, we rename bound variables to names that have not yet been used. This is less efficient but closely resembles what a human does when manipulating lambda terms by hand.

First, let us create a function that generates a new name that conflicts with none of the supplied names. The set of potential conflicts is passed as an argument.

import Data.Text (Text, pack)
import Data.Set  (Set, member)

-- Generate an infinite list of proposed names and take the first
-- one that has not yet appeared in the conflict set.
fresh :: Set Text -> Text
fresh conflicts = head . dropWhile (`member` conflicts) $ names
  where
    -- Primitive names are simply lower-case Latin letters
    primitiveNames = map (:[]) letters
    -- Compound names consist of a letter and a number
    complexNames = [(l:n) | n <- numbers, l <- letters]
    -- The complete list of names
    names = map pack $ primitiveNames ++ complexNames
    -- Letters and numbers in use
    letters = ['a' .. 'z']
    numbers = map show [1..]

Using this function, we can write another that renames every bound variable so that none occurs in the conflict set. Such a transformation of bound-variable names does not change the term itself and is called $\alpha$ -conversion:

alpha :: Set Text -> Term -> Term
alpha conflicts var@(Var _)    = var
alpha conflicts (App algo arg) = App (alpha conflicts algo) (alpha conflicts arg)
alpha conflicts (Lam var body) = if hasConflict then renamed_lam else alpha_lam
  where  
    hasConflict = var `member` conflicts
    alpha_lam   = Lam var (alpha conflicts body)
    renamed_lam = Lam new_var new_body
    new_var     = fresh $ conflicts `union` free body
    new_body    = substitute body var (Var new_var)

Writing this function required us once again to call substitute, because when the variable beneath a lambda changes, every occurrence of it in the abstraction's body must also be changed. We now have everything needed to implement this magical function:

substitute :: Term -> Text -> Term -> Term
substitute var@(Var var')     name expr = if var' == name then expr else var
substitute     (App algo arg) name expr = App (substitute algo name expr) (substitute arg name expr)
substitute lam@(Lam var body) name expr = if var == name then lam else new_lam
  where
    alpha_lam = alpha (free expr) lam
    new_body  = substitute body name expr
    new_lam   = if var `member` free expr then substitute alpha_lam name expr
                                          else Lam var new_body

Reduction

In the lambda calculus, we allow two kinds of reduction: one-way transformations, or “simplifications”, that represent computation. The first is trivial and is called $\eta$ -conversion:

\lambda x. M \, x = M

It follows from simple considerations that can be found in Barendregt. The implementation is almost as straightforward:

eta :: Term -> Term
eta (Lam var body) = case body of
                       App algo (Var v)
                         | var == v && v `notMember` free algo = algo
                       _                                       = Lam var (eta body)
eta (App algo arg) = App (eta algo) (eta arg)
eta var            = var

The main transformation, and the only inference rule in the lambda calculus, is $\beta$ -conversion:

(\lambda x.M) \, N = M[x:=N]

That is, an application of a lambda abstraction to a term is evaluated by replacing the abstraction's variable—its argument—with the concrete value. From this transformation, we can write the rules of one-step $\beta$ -reduction $M \rightarrow_{\beta} N$ :

$(\lambda x.M) \, N = M[x:=N]$ : a direct $\beta$ -conversion.
$M \rightarrow_{\beta} N \Rightarrow M \, Z \Rightarrow N \, Z$ : reduction in the first term—the algorithm—of an application.
$M \rightarrow_{\beta} N \Rightarrow Z \, M \Rightarrow Z \, N$ : reduction in the second term—the argument—of an application.
$M \rightarrow_{\beta} N \Rightarrow \lambda x. M \Rightarrow \lambda x. N$ : reduction in the body of an abstraction.

We implement it as follows:

beta :: Term -> Term
beta var@(Var _)        = var
beta     (Lam var body) = Lam var (beta body)
beta     (App algo arg) = case algo of
                            Lam var body -> substitute body var arg
                            _            -> if algo /= algo' then App algo' arg
                                                             else App algo arg'
  where
    algo' = beta algo
    arg'  = beta arg

That is all! We have a complete lambda-calculus calculator with a parser, attractive output, and several forms of reduction. The following simple function turns any term into normal form, if it has one:

reduce :: Term -> Term
reduce term | beta term == term = eta term
            | otherwise         = reduce (beta term)

You can practise applying the lambda calculus by encoding natural numbers and integers, for example, as described on Wikipedia.

To finish, here is the complete resulting listing:

module UntypedLambda where

import           Control.Applicative  ((<$>), (<*>), (<|>))
import           Control.Monad        (void)
import           Data.Text            (Text, pack)
import           Data.Attoparsec.Text
import           Data.Set             (Set, delete, empty,
                                       insert, singleton, union,
                                       member, notMember)

data Term = Var Text       -- variables
          | App Term Term  -- application
          | Lam Text Term  -- abstraction
    deriving (Show)

-- Pretty Print

data Position = AppAlgo | AppArg | LamBody | Other

pretty :: Term -> Text
pretty = pretty' Other
    where
    prettyLB :: Term -> Text
    prettyLB (Lam var body) = var <> pretty' LamBody body
    prettyLB _              = undefined
    
    pretty' :: Position -> Term -> Text
    pretty' LamBody lam@(Lam _ _)  = " " <> prettyLB lam
    pretty' AppAlgo lam@(Lam _ _)  = "(" <> pretty' Other lam <> ")"
    pretty' _       lam@(Lam _ _)  = "λ" <> prettyLB lam
    pretty' LamBody term           = "." <> pretty' Other term
    pretty' _       (Var name)     = name
    pretty' AppArg  app@(App _ _)  = "(" <> pretty' Other app <> ")"
    pretty' _       (App algo arg) = pretty' AppAlgo algo <> " " <> pretty' AppArg arg 

-- Parsing

spaces :: Parser ()
spaces = void $ many' space

-- Parses an expression and every space after it, discarding the spaces.
spaced :: Parser a -> Parser a
spaced x = x <* spaces

-- Parses one full stop and discards the parser output.
dot :: Parser ()
dot = void $ spaced (char '.')

-- Parses a lambda symbol, \\ or L, and discards the parser output.
lambda :: Parser ()
lambda = void $ spaced (char '\\' <|> char 'λ' <|> char 'L')

-- Parses an expression in parentheses; spaces before the opening and
-- after the closing parenthesis are accepted and consumed.
parens :: Parser a -> Parser a
parens x = spaced (char '(') *> x <* spaced (char ')')

-- Parses a string that begins with a Latin letter and contains
-- Latin letters, digits, and the ' symbol.
name :: Parser Text
name = (pack .) . (:) <$> oneOf ['a'..'z'] <*> many' (letter <|> digit <|> char '\'')
  where
    oneOf = choice . (char <$>)

-- Reads at least one natural term; if there is more than one,
-- combines them into an application using left associativity.
term :: Parser Term
term = foldl1 App <$> many1 (spaced naturalTerm)

-- Reads either a parenthesised term that may contain an application,
-- a variable, or a lambda abstraction.
naturalTerm :: Parser Term
naturalTerm = parens term <|> variable <|> abstraction 

-- Parses one variable.
variable :: Parser Term
variable = Var <$> name

-- Parses a lambda abstraction: a lambda symbol, at least one variable,
-- a full stop, and the term that forms the abstraction's body; folds
-- the variables into nested lambda abstractions by right associativity.
abstraction :: Parser Term
abstraction = do lambda
                 vars <- many1 (spaced name)
                 dot
                 expr <- term
                 pure $ foldr Lam expr vars

parseTerm :: Text -> Either String Term
parseTerm = parseOnly term

-- Logic

free :: Term -> Set Text
free (Var var)      = singleton var
free (App algo arg) = free algo `union` free arg
free (Lam var body) = var `delete` free body

bound :: Term -> Set Text
bound (Var var)      = empty
bound (App algo arg) = bound algo `union` bound arg
bound (Lam var body) = var `insert` free body

instance Eq Term where
    Var a == Var b       = a == b
    App a b == App a' b' = a == a' && b == b'
    Lam v b == Lam v' b' = b == substitute b' v' (Var v)
    _ == _               = False

-- Generate an infinite list of proposed names and take the first
-- one that has not yet appeared in the conflict set.
fresh :: Set Text -> Text
fresh conflicts = head . dropWhile (`member` conflicts) $ names
  where
    -- Primitive names are simply lower-case Latin letters
    primitiveNames = map (:[]) letters
    -- Compound names consist of a letter and a number
    complexNames = [(l:n) | n <- numbers, l <- letters]
    -- The complete list of names
    names = map pack $ primitiveNames ++ complexNames
    -- Letters and numbers in use
    letters = ['a' .. 'z']
    numbers = map show [1..]

alpha :: Set Text -> Term -> Term
alpha conflicts var@(Var _)    = var
alpha conflicts (App algo arg) = App (alpha conflicts algo) (alpha conflicts arg)
alpha conflicts (Lam var body) = if hasConflict then renamed_lam else alpha_lam
  where  
    hasConflict = var `member` conflicts
    alpha_lam   = Lam var (alpha conflicts body)
    renamed_lam = Lam new_var new_body
    new_var     = fresh $ conflicts `union` free body
    new_body    = substitute body var (Var new_var)

substitute :: Term -> Text -> Term -> Term
substitute var@(Var var')     name expr = if var' == name then expr else var
substitute     (App algo arg) name expr = App (substitute algo name expr) (substitute arg name expr)
substitute lam@(Lam var body) name expr = if var == name then lam else new_lam
  where
    alpha_lam = alpha (free expr) lam
    new_body  = substitute body name expr
    new_lam   = if var `member` free expr then substitute alpha_lam name expr
                                            else Lam var new_body

-- Evaluation

eta :: Term -> Term
eta (Lam var body) = case body of
                       App algo (Var v)
                         | var == v && (v `notMember` free algo) -> algo
                       _                                         -> Lam var (eta body)
eta (App algo arg) = App (eta algo) (eta arg)
eta var            = var

beta :: Term -> Term
beta var@(Var _)        = var
beta     (Lam var body) = Lam var (beta body)
beta     (App algo arg) = case algo of
                            Lam var body -> substitute body var arg
                            _            -> if algo /= algo' then App algo' arg
                                                             else App algo arg'
  where
    algo' = beta algo
    arg'  = beta arg

reduce :: Term -> Term
reduce term | beta term == term = eta term
            | otherwise         = reduce (beta term)

Printing terms#

Reading terms#

Giving the calculus meaning#

Reduction#

Printing terms

Reading terms

Giving the calculus meaning

Reduction