Types and Programming Languages Chapter 5 The Untyped Lambda Calculus

Syntax

t ::=
      x     // variable
      λx.t  // abstraction
      t t   // application

Abstraction is analogous to a function definition:

function (n) { t }
λn. t

Application is analogous to a function call:

(function (n) { t }(x))
(λn. t) x

Precedence

s t u = (s t) u                    // application associates to the left
λx. λy. x y x = λx. (λy. ((x y) x) // abstraction bodies extend to the right

Scope

x is free when it is not bound by an enclosing abstraction on x, e.g.

x y
λy. x y

x is bound:

λx. x
λz. λx. λy. x (y z)

The first x is bound and the second is free:

(λx.x) x

A term with no free variables is closed (also called a combinator):

id = λx.x

Beta reduction

Normal order strategy

Under the normal order strategy, the leftmost, outermost reducible expression is always reduced first.

   id (id (λz. id z))
   ------------------
 → id (λz. id z)
   -------------
 → λz. id z
       ----
 → λz.z

Call by name

The call by name strategy is yet more restrictive, allowing no reductions inside abstractions.

   id (id (λz. id z))
   ------------------
 → id (λz. id z)
   -------------
 → λz. id z

Call by value

Most languages use a call by value strategy, in which only outermost reducible expressions are reduced and where a reducible expression is reduced only when its right-hand side has already been reduced to a value — a term that is finished computing and cannot be reduced any further.

   id (id (λz. id z))
      ---------------
 → id (λz. id z)
   -------------
 → λz. id z

Church booleans

tru = λt. λf. t;
fls = λt. λf. f;
test = λl. λm. λn. l m n;
and = λb. λc. b c fls;

Substitution

Variable capture

Inference rules

We finished the meeting by talking through the inference rules presented in the book that describe the call-by-value strategy for evaluating our programs.

We worked through an example of identifiying the values and terms in an expression:

(λx. x) ((λx. x) (λz. (λx. x) z))

Then applied the inference rules to reduce the expression. We realised that it wasn't obvious on first reading, but the inference rules for call-by-value are mutually exclusive. If you can apply any rule to an expression there is only one rule you can apply.

We then tried the exercise to re-write the inference rules to describe full beta reduction.

Mostly this required us to replace references to values in the rules with references to terms and this showed us that we now had a choice of which rule to apply at any given moment. The final rule we added was E-ABS:

    t1 ⇒ t1ʹ
----------------
λx. t1 ⇒ λx. t1ʹ

There was some confusion in the room about why this was neccessary, and we explained that this is because in λx. x the other rules don't apply because they apply to two terms next to each other, and λx. is not a term on it's own, so we need E-ABS to let us "go inside" the abstraction and work on the x (the function definition).

Thanks

Thanks to Leo and Geckoboard for hosting and lending use of their bread knife. Thanks to all those who provided snacks, especially James for his homemade Lambda Focaccia.