A lambda-term that finds beta-normal forms


The untyped lambda calclus is Turing Complete, in the sense that every program can be defined by a \(\lambda\)-term. Furthermore, there is an algorithm that finds the \(\beta\)-normal form of a \(\lambda\)-term (if it has one): repeated left-most reduction.

So, let's try to find the term that defines that algorithm!

The strategy is:

  1. Write a program to find \(\beta\)-normal forms in Haskell
  2. Translate this into a small toy language
  3. Write a compiler (in Haskell) from said language into λ-terms

Finding \(\beta\)-normal forms in Haskell

We start by defining our types.

We have some choice of how to handle variables. It is important that we are able to generate a "fresh" variable from any finite collection - this will be needed when we implement substitution. This would be easily done if we used integers to name variables ("one plus the biggest one"), but it is not so hard to do with strings (as we will see below), and string variables are nice to use.

The expression gen n returns the list of all variables consisting of lowercase letters of length n. Crucially they are all distinct. We use it in frees ns to get a list of (length ns)+1 distinct names so that we can find one which is not in ns.

The function frees is used to find the free variables in a term. Our approach here is certainly naive. Why not put the free variables in a Set, or at least an ordered list? As it turns out, the overhead induced by more efficient data structures actually makes frees noticably slower for reasonably sized inputs.

Substitution and β-reduction are now straightforward.

We can use the Alternative instance of Maybe to cleanly implement left-most reduction.

And repeat.

A small language

Click here to read about LamE (The LAMbda Evaluater). Most of the rest of this post will be written in LamE. The syntax is a blend of Lisp and Haskell, and is hopefully mostly obvious.

Translating to LamE

LamE doesn't have all the high-level features of Haskell. So we'll have to get our hands dirty and implement them ourselves.

Let's start by defining some functions about lists: append, filter, map, concat, length, iterate, take, takeWhile, and elem are what we'll need.

Now elem :: Eq a => a -> [a] -> Bool is a little troublesome. We don't have typeclasses in LamE, so we can't overload the == operator. So we'll need to write a specialized function for checking if a string is a member of a list of strings.

Now we can start recreating our program in LamE.

The function frees is quite straightforward.

We can rewrite list comprehensions in terms of concat and map to get this rather verbose definition of gen.

Defining fresh and sub is straightforward.

We don't have Maybe, but we can simulate it with lists, where [] = Nothing and [a] = Just a.

Leftmost reduction is rather tedious to define.

Finally, we get \(\beta\)-reduction!

The program compiles into this very long term