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