# 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.

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.

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.

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

The program compiles into this very long term