We’re going to finish off a few things about the lambda calculus and then moving on to ML.

Back to the Y combinator

We looked over the Y combinator, which had the property:

Y f => f (Y f)

Let’s look at an example of using this: the recursive factorial function. Note that fac, below, is a single variable.

Y (λfac. λn. if (= n 0) 1 (* n (fac (- n 1))))

Let’s look at it by applying it to 3. Call the entire expression after the Y “f”.

Y (λfac. λn. if (= n 0) 1 (* n (fac (- n 1))))
  ^--------------------f---------------------^

f takes two things: a function fac and a number n.

(Y f) 3
β=> f (Y f) 3

At this point, we’re assigning fac = f (Y f) and n = 3.

2β=> if (= 3 0) 1 (* 3 ((Y f) (- 3 1))
2δ=> if (false) 1 (* 3 ((Y f) 2)
δ=> * 3 ((Y f) 2)
          ^ Is just 2 factorial

Order of application

Eh, recap of the lecture. But for the sake of completeness:

• Normal order: Reduce the leftmost, outermost β-reduction first (i.e. replace arguments before evaluating them).

• Applicative order: Reduce rightmost, innermost β-reduction first (i.e. evaluate arguments before replacing them).

And then back to the Church-Rosser theorems again. Apparently they come up on tests pretty frequently, so again, for completeness:

• First: If you have two expressions that are convertible to each other, i.e. E1 <=> E2, there exists some expression E such that E1 and E2 reduce to E. The corollary to this theorem is more important, however: every expression that has a normal form has a unique normal form. There’s no situation where applying a different order will get you a different normal form (assuming that a normal form exists for that theorem).

• Second: If a normal form exists, then normal-order reduction will get you to the normal form.

δ-reduction and Church encoding

How does δ-reduction work? How do we represent numbers and so on?

Take a look at the Wikipedia article for Church encoding for an in-depth description of this. But here are a few examples:

The numbers are encoded like this:

0 = λf.λx.x
1 = λf.λx. f x
2 = λf.λx. f (f x)
...

And so on. In words, 0 takes a function f and a value x and just returns the input. 1 applies a f once to x. 2 applies it twice. And so on.

true and false are represented like this:

true = λa.λb. a
false = λa.λb. b

So true returns the first argument, and false returns the second. You slap that in front of a pair of clauses: then-clause else-clause, and you get a sort if if-statement.

This isn’t necessary to know for the test, but it’s cool.

ML

Same sort of things from last lecture.

Here’s an example we didn’t go over: inserting an item into a list at a given index.

fun insert el _ [] = el::[]
 |  insert el 0 list = el::list
 |  insert el i (x::xs) = x :: (insert el (i-1) xs)

We’ll continue with ML and type inference next recitation.