Computation and equivalence in the λ-calculus

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