Types and Programming Languages Chapter 5 The Untyped Lambda Calculus

Syntax

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

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 reducie 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;