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
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
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.
We can use the
Alternative instance of
Maybe to cleanly implement left-most reduction.
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:
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)));
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.
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
map to get this rather verbose definition of
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))));
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