Untyped λ-calculus via de Bruijn indices

Technically, we can specify the set of λ-terms in terms of de Bruijn notation as \[\def\Coloneqq{::=}\def\divd{\ |\ } M, N \Coloneqq n \divd (M N) \divd (λM)\] where \(n ∈ \{0, 1, 2, ...\}\).

In Haskell, we can give this encoding of λ-terms in terms of an algebraic data type. First, we should define a type for natural numbers:

data Nat = Zero | Succ Nat

λ-terms may then be encoded in a way that matches the definition given above:

data Lambda = Var Nat | App Lambda Lambda | Lam Lambda

Now that we are using de Bruijn indices, substitution becomes a bit tricky. But we can tame it by dividing the task up into parts that are manageable to do on their own.

First, let's define a very general function for doing arbitrary substitutions of variables by λ-terms. This function should have the following type:

subst :: (Nat -> Lambda) -> Lambda -> Lambda

It takes a function of type Nat -> Lambda determining how the relevant substitution (whatever that is) should be performed, and it provides a general protocol for managing this substitution for different kinds of λ-terms. For example, on variables, subst just performs the substution:

subst f (Var i) = f i

On applications, it does the substitution to both the function and the argument:

subst f (App t u) = App (subst f t) (subst f u)

Finally, on abstractions, something special has to be done. Because we don't want to mess around with variables which are bound by the abstraction, we need to instead do substitution using another function g just like the function f, but which is different in two ways. The first way it is different is that it maps Zero onto Var Zero, ensuring that it remains bound by the enclosing Lam. The second way it is different is that it maps any Succ i onto f i, since the Succ was only there in order to ``look past'' the enclosing Lam - it should really just be an i for the purpose of performing the substitution - and it then renames the result of performing the substitution f i by incrementing all free variables inside f i with a Succ, using a function rename. This last part helps to avoid the problem of variable capture, i.e., by making sure any free j inside f i still looks like a j outside of the enclosing Lam, which mean that it has to be a Succ j inside the enclosing Lam.

subst f (Lam t) = Lam (subst g t)
  where g :: Nat -> Lambda
        g Zero = Var Zero
        g (Succ i) = rename Succ (f i)

How exactly does rename work? It should take some function from Nat onto Nat and use this function to rename free variables inside a λ-term. Thus its type is

rename :: (Nat -> Nat) -> Lambda -> Lambda

Given some function h of type Nat -> Nat (e.g., Succ, as above), it renames variables by adjusting the natural number they correspond to using h:

rename h (Var i) = Var (h i)

On applications, as you might expect, it performs renaming on both the function and the argument:

rename h (App t u) = App (rename h t) (rename h u)

And on abstractions, it performs renaming on the body of the abstraction, but (as above) keeping bound variables intact and taking into account any extra Succ that might be lying around by using h' instead of h:

rename h (Lam t) = Lam (rename h' t)
  where h' :: Nat -> Nat
        h' Zero = Zero
        h' (Succ i) = Succ (h i)

That's it for the definition of subst! We can now use it to define a more immediately useful function

subst0 :: Lambda -> Lambda -> Lambda

which substitutes a λ-term t for Var Zero inside a λ-term u whose Lam has just been taken off. That is, we want to do a substitution inside a u whose free occurrences of Var Zero used to be bound by an enclosing Lam in the term Lam u. This yields the following definition:

subst0 t = subst f
  where f :: Nat -> Lambda
        f Zero = t
        f (Succ i) = Var i

Now that we have a definition of substitution, we want to use it to define a function which takes any given λ-term into its β-normal form, assuming it has one. This function should just take a λ-term onto a λ-term, where the latter is in normal form; thus it should have the following type:

betaNormal :: Lambda -> Lambda

Again, there are three kinds of λ-terms we need to consider as the argument to this function. First, variables.

betaNormal v@(Var _) = v

Variables are already in β-normal form, so nothing needs to be done to them. Next, let's consider abstractions.

betaNormal (Lam t) = Lam (betaNormal t) 

Here, we only need to look underneath the binder Lam and normalize the body of the abstraction. The reasoning is as follows. Let's say u is in β-normal form; does turning u into Lam u create a β-redex somewhere? No! So as long as we have the body in normal form, adding a Lam won't make a difference. Next, the more tricky case: applications.

betaNormal (App t u) = case betaNormal t of
                         Lam t' -> betaNormal (subst0 (betaNormal u) t')
                         t' -> App t' (betaNormal u)

If taking the function t into β-normal form results in an abstraction, we need to perform a β-reduction step between the function and the argument (which we normalize). The result may not be in normal form, so we have to call betaNormal again at the end. If taking t into β-normal form does not result in an abstraction, than we can just take u onto its normal form and put the two back together into an application. The reasoning here is that putting them back together can't possibly create any new β-redices.

To define printLambda, we'll start by defining a function

printLambda' :: [String] -> (Nat -> String) -> Lambda -> String

which takes a list of strings providing us with fresh variable names, along with a function of type Nat -> String that should actually use this list of names in some way. Given these two ingredients, it takes a Lambda onto a String.

We can define this function by first defining its behavior on variables:

printLambda' _ f (Var i) = f i

How should printLambda' be defined on applications? That is, fill out the rest of the following branch by filling in the _:

printLambda' freshVs f (App t u) = _

The third branch, which involves abstractions, is the trickiest. Here, the list of fresh variable names actually needs to be used. This branch would look as follows:

printLambda' (fresh:vs) f (Lam t) =
  "(λ" ++ fresh ++ "." ++ printLambda f' vs t ++ ")"
  where f' :: Nat -> String

Fill out the rest of the definition of this branch by saying what f' does!

Now that all three branches of printLambda' are defined, give a definition of printLambda using printLambda' by feeding it the appropriate pieces.