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:

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

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

We start by defining our types.

newtype Name = Name String deriving (Eq)
data Term = Var Name | Abs Name Term | App Term Term

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.

gen :: Int -> [Name]
gen 0 =[Name "a"]
gen 1 = map (Name . (:[])) ['a'..'z']
gen n = let ns = gen (n-1) in [Name (s:ss) | s <- ['a'..'z'], (Name ss) <- ns]

fresh :: [Name] -> Name
fresh ns =
  let n = length ns
      k = length $ takeWhile (<=n) $ iterate (*26) 1 
      ps = take (n+1) $ gen k in 
        head $ filter (not . (flip elem) ns) ps

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.

frees :: Term -> [Name]
frees (Var n) = [n]
frees (App s t) = frees s ++ frees t
frees (Abs x s) = filter (/=x) $ frees s

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.

sub (Var y) t x  = if x==y then t else (Var y)
sub (App u v) t x  = App (sub u t x) (sub v t x)
sub (Abs y s) t x = let ts = frees t in
  if y==x || y `elem` ts then let z = fresh (ts ++ frees s ++ [x]) in Abs z $ sub (sub s (Var z) y) t x 
  else Abs y (sub s t x)

bred :: Term -> Maybe Term
bred (App (Abs x s) v) =  Just $ sub s v x
bred _ = Nothing

Substitution and β-reduction are now straightforward.

lred :: Term -> Maybe Term
lred (Var x) = Nothing
lred u@(App s t) = bred u
  <|> do
    x <- lred s 
    return $ App x t
  <|> do
    x <- lred t
    return $ App s x 
lred (Abs x s) = lred s >>= Just . Abs x

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

bnf :: Term -> Term
bnf t = case lred t of
  Just t' -> bnf t'
  Nothing -> t

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.

rec append = func (x y) (
  if empty x 
  then y 
  else cons (head x) (append (tail x) y));

rec filter = func (p xs) (
  if empty xs
  then xs
  else (if p (head xs) 
    then cons (head xs) (filter p (tail xs)) 
    else filter p (tail xs)));

rec map = func (f xs) (
  if empty xs 
  then xs
  else cons (f (head xs)) (map f (tail xs)) );

rec concat = func (xss) (
  if empty xss 
  then xss
  else append (head xss) (concat (tail xss)));

rec length = func (xs) (
  if empty xs 
  then 0 
  else + 1 (length (tail xs)));

rec takeWhile = func (p xs) (
  if empty xs 
  then xs 
  else if p (head xs) 
    then cons (head x) (takeWhile p (tail x)) 
    else (takeWhile p (tail x)));

rec iterate = func (f x) (
  cons x (iterate f (f x)));

rec take = func (n xs) (
  if == 0 n 
  then nil 
  else cons (head x) (take (- n 1) (tail xs)));

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.

rec elemStr = func (x xs) (
  if empty xs 
  then false 
  else if =s x (head xs) 
    then true 
    else elemStr x (tail xs));

Now we can start recreating our program in LamE.

rec frees = func (t) (match t as
  (Var n) ([n])
  (App u v) (append (frees u) (frees v))
  (Abs n v) ( filter (func (m) (not (=s n m))) (frees v)));

The function frees is quite straightforward.

val names = ["a","b","c","d","e","f","g","h","i","j","k","l","m","n","o","p","q","r","s","t","u","v","w","x","y","z"];
val chars = ['a','b','c','d','e','f','g','h','i','j','k','l','m','n','o','p','q','r','s','t','u','v','w','x','y','z'];

rec gen = func (n) (
  if == n 0 
  then ["a"]
  else (if == n 1 
    then names
    else let val ns = gen (- n 1) in (
      let val f = func (s) (
        let val g = func (t) (
          +s s t) 
        in concat (map g names)) 
      in (concat (map f chars)))));

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

val fresh = func (ns) (
  let val n = length ns in (
  let val k = length (takeWhile (leq n) (iterate (func (x)  (* x 26)) 1)) in (
  let val ps = take (+ 1 n) (gen k) in (
    head (filter (func (x) (not (elemStr x ns))) ps)))));

rec sub = func (s t x) (match s as
  (Var a) (if =s x a then t else s)
  (App a b) (App (sub a t x) (sub b t x))
  (Abs a b) (let val ts = frees t in (
    if or (=s x a) (elemStr a ts) 
    then let val z = fresh (concat [ts, frees b, [a]]) in (Abs z (sub (sub s (Var z) y) t x ) )
    else Abs a (sub t x b))));

Defining fresh and sub is straightforward.

val bred = func (t) (match t as 
  (Var x) (nil)
  (App p q) (match p as
    (Var x) (nil)
    (App a b) (nil)
    (Abs x s) ([sub s q x]))
  (Abs x s) (nil));

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

rec lred = func (t) (match t as
  (Var x) (nil)
  (App p q) (
    if empty (bred (App p q)) 
    then (if empty (lred p) 
      then (if empty (lred q) 
        then nil  
        else App p (head (lred q)))  
      else App (head (lred p)) q ) 
    else head (bred (App p q)))
  (Abs x s) (if empty (lred s) 
    then nil 
    else Abs x (head (lred x))));

Leftmost reduction is rather tedious to define.

rec bnf = func (s) ( 
  let val xs = lred s in 
  (if empty xs 
  then s 
  else bnf (head xs))

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

The program compiles into this very long term