HW 3

COSC 4780

1 Computation and equivalence in the λ-calculus

1.1 β-reduction and β-equivalence

Recall, a redexis a term having the following shape.

(λx.M)N

i.e. it is the application of a lambda term to any other term.

We gave the following definitions in class.

Definition 1.1 (One-step β-reduction)

1.) (λx.M)N →β M[x := N]

We can extend this definition to allow one redex to be reduced anywhere in

a term.

2.) M →β N ⇒ MZ →β NZ

3.) M →β N ⇒ ZM →β ZN

4.) M →β N ⇒ λx.M →β λx.N

Note that →β can be considered a a relation on terms.

→β= {hM, Ni | M →β N}

i.e. it is the set of all terms M and N such that M →β N.

Example 1.1. Note that clauses (2) and (3) allow reduction in either side

of an application term, but not in both simultaneously. For example, the

following two are valid beta-reductions by clause (1).

(λx.x)y →β y

(λy.y)w →β w

Clause (2) allows reduction on the left side of an application term, so, if

M = ((λx.x)y) and N = y, for any term Z we know the following holds.

((λx.x)y)Z →β yZ

If Z = (λy.y)w, then,

((λx.x)y)((λy.y)w) →β y((λy.y)w)

Similarly, by (3), if Z = ((λx.x)y) then,

((λx.x)y)((λy.y)w) →β ((λx.x)y)w

1

It is not the case that the following is a reduction satisfying the relation

→β.

((λx.x)y)((λy.y)w) →β yw

Which rule would you apply? The definition of →β says one side must stay

constant. You can’t get there from here … unless you apply two steps of

β-reduction.

((λx.x)y)((λy.y)w) →β y((λy.y)w) →β yw

or

((λx.x)y)((λy.y)w) →β ((λx.x)y)w →β yw

Example 1.2. Clause (4) allows reduction in the body of an abstraction.

Since (λx.x)y →β y, by (4), λz.(λx.x)y →β λz.y.

Definition 1.2 (β

∗

-reduction) The →∗

β

relation is the reflexive transitive

closure of the →β relation.

M →β N ⇒ M →∗

β N

M →∗

β M

M →∗

β N ∧ N →∗

β L ⇒ M →∗

β L

Problem 1.1. Beta-reduce the following lambda-terms by hand.

0.) (λy.y)z

1.) w ((λy.y)z)

2.) ((λy.y)z)w

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

4.) ((λx.(λy.(y x)))y)

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

We can make →∗

β

into an equivalence relation by making it symmetric.

Definition 1.3 (β-equivalence)

1.) M →∗

β N ⇒ M ≡β N

2.)M ≡β N ⇒ N ≡β M

3.)(M ≡β N ∧ N ≡β L) ⇒ M ≡β L

Clause (1) just says two terms are ≡β if they are already in the relation

→β. Clause (2) ensures that ≡β is symmetric. If you think of β-reduction

as computation, then ≡β allows backward steps of computation. Clause

2

(3) ensures ≡β is transitive. Note that since →β is reflexive, by clause

(1), so is ≡β. You might think that since →β is also transitive, clause (3)

here is redundant. It’s not, the transitivity in →β only includes “forward”

steps of computation, it does not allow a sequence containing forward and

“backward” steps.

1.2 η-Reduction

Next we introduce a different kind of reduction, η-reduction1

.

Definition 1.4. (η-reduction)

(λx.Mx) →η M if x 6∈ F V (M)

Look, because x is not free in M, M[x := N] = M and so

(λx.Mx)N →β (Mx)[x := N] = M[x := N]x[x := N] = MN

The idea of η-reduction is to say, why not just use M instead of λx.Mx

since any term (say N) that I apply this function to is just the same as I

will get by directly applying M.

An example of η-reduction you already know occurs in languages which

allow functions to be defined in Curried form, like Haskell and OCaml.

For example, if f x y = x + y, we can simply write g = f 5 instead of

g y = f 5 y. This is a form of η-reduction.

Note that →η is a relation just like →β,

→η= {hM, Ni | M →η N}

Definition 1.5 (→{β,η}) Remember, when we consider →β and →η as relations, we are thinking of them as sets of pairs of terms. We can union sets

together.

→{β,η}

def = →β ∪ →η

1.3 Recursion in the lambda Calculus

Recursion in the λ-calculus is performed with so-called fixedpoint combinators. A combinator is just a term with no free variables, also called a closed

term. defined as follows:

Y

def = λf.(λx.f(xx))(λx.f(xx))

1

η is the Greek letter named “eta”. Also, η reduction is described in chapter 6 (pg

167) of the Schmidt text.

3

Definition 1.6 (The Fixedpoint property) A term (say F) has the fixedpoint property if, for every term M,

FM ≡β M(FM)

Theorem 1.1. We prove that Y has the fixed point property, that is, for

every term M

Y M ≡β M(Y M)

The proof is as follows:

Y M = (λf.(λx.f(xx))(λx.f(xx)))M

→β (λx.M(xx))(λx.M(xx))

→β M((λx.M(xx))(λx.M(xx)))

←β M((λf.(λx.f(xx))(λx.f(xx)))M)

= M(Y M)

Now, recall that application associates to the left, so xyz means (xy)z.

And so, regarding η-reduction in particular, and this will be useful to solve

the next problem.

λy.NNy →η NN

If N is something complicated like (λx.M(λy.xxy)), then

λy.(λx.M(λy.xxy))(λx.M(λy.xxy))y →η (λx.M(λy.xxy))(λx.M(λy.xxy))

Definition 1.7. The Z combinator is defined as follows:

Z

def = λf.(λx.f(λy.xxy))(λx.f(λy.xxy))

Problem 1.2. Prove2

that, like Y , Z enjoys the fixed-point property when

we consider the equivalence ≡βη (the relation that allows us to use both β

and η reduction.) You must prove that for any term M, that

ZM ≡βη M(ZM)

2You will need to use one instance of η-reduction to get the proof to go through.

4