The implementation of functional programming language

Ref:

Jones, The implementation of functional programming language

\(\lambda\) expression

<exp> :: = <constant>
      |  = <variable>
      |  = <exp> <exp>
      |  = lambda <variable>.<exp>

Free and bound variables: Free = External, Bound = Local
CONS, HEAD, TAIL
```
CONS = (lambda a . lambda b . lambda f . f a b)
HEAD = (lambda c . c (lambda a . lambda b . a))
TAIL = (lambda c . c (lambda a . lambda b . b)) 
```
How to understand the three definitions?
```
CONS x y = lambda f . f x y
CONS (CONS x y) z = lambda f . f (CONS x y) z = lambda f . f (lambda f . f x y) z 
```
We may think of (lambda f . f ) as kind of a bracket, which encloses x and y inside. Then what about HEAD? Note that (CONS x y) is a function that requires a function as input, and HEAD requires a function as its input, and this function itself must take a function as input.
```
(lambda a . lambda b . a) x y = (lambda b x) y = x 
```
So the key is the inside part of HEAD.
Beta reduction, beta conversion
Alpha conversion: change name of variable
Eta conversion: equivalence of lambda abstractions
Proving interconvertibility: if two expressions can be converted into the same expression, then the two are equivalent.
E[M/x] = (lambda x . E) M

(E F)[M/x] = (lambda x . (E F)) M = E[M/x] F[M/x]
(lambda x . E)[M/x] = (lambda x (lambda x . E)) M = (lambda x . E)
(lambda y . E)[M/x] = (lambda x (lambda y . E)) M = lambda y . E if x does not appear free in E
                                                  = lambda y . E[M/x] if y does not appear free in M
                                                  = lambda z . (E[z/y])[M/x] otherwise

Reduction order: no redexes = normal form
- Not every expression has a normal form.
```
(lambda x x x) (lambda x x x) = ((lambda x x x) (lambda x x x)) 
```
  which is equal to itself.
- Dependence on reduction path
```
(lambda x 3) (D D) = 3, or infinite loop?
```
Uniqueness of order reduction
- Church-Rosser theorem I
  If \(E_1\leftrightarrow E_2\), then there exists an expression \(E\), such that \[ E_1 \rightarrow E\ \text{and}\ E_2 \rightarrow E.\]
  Welch 1975; Rosser 1982
- Hence all reduction sequences which terminate will reach the same result.
- Normal order reduction: the leftmost outermost redex should be reduced at first.
  Intuition: function should be evaluated ealier than its parameters; from outer to inner.
- Church-Rosser theorem II
  If \(E_1\leftrightarrow E_2\), and \(E_2\) is in normal form, then there exists a normal order reduction sequence from \(E_1\) to \(E_2\).
- Optimal reduction orders: normal order does not guarantee to be the fastest; for some cases (tree reduction) it is provably least favorable; for graph reduction is is almost optimal.
Recursive functions
- FAC = (lambda n . IF (= n 0) 1 (* n (FAC (- n 1)))), but this is not lambda abstraction.
- FAC = H FAC, where H = (lambda fac . (lambda n . (... fac ...))). FAC is a fixed point of H.
- Fixed point combinator Y: Y H = H (Y H)
- Y can be defined as a lambda abstraction:
  Y = (lambda h . (lambda x . h (x x)) (lambda x . h (x x)))
  Y H = (lambda x . H (x x)) (lambda x . H (x x)) = H ((lambda x . H (x x)) (lambda x . H (x x))) = H Y H
  (lambda x . h (x x)) does not have a finite type.
- Uniqueness of the Y operation? Check domain theory.