HW 2  Lambda Calculus

HW 2 
COSC 4780
1 Lambda Calculus
1.1 Syntax
Recall the syntax of lambda terms:
Λ ::= x | (MN) | (λx.M)
where
x ∈ Var is a variable from a set Var = {w, x, y, z, w1, x1, y1, · · ·}.
M, N ∈ Λ are previously constructed lambda-terms.
The term (MN) is called an application and the term (λx.M) is called
an abstraction. Some conventions for reading syntax are that application
associates to the left, thus MN1N2 is the term (MN1)N2. Also, application
has higher precedence than abstraction so λx.MN is the term λx.(MN) not
(λx.M)N.
The idea of the abstraction terms is that it models a function of one
argument. So, if you define a function f, so that f(x) = x then the lambda
abstraction which is the same function as f is λx.x. The symbol λ is a
binding operator. In the term λx.M, the variable x (the binding occurrence)
is bound in the term M (called the body).Occurrences of the variable x in M
are bound occurrences. Also, if you wrote g(y) = y, you would say that f
and g are the same function. Similarly, λy.y is the same function as λx.x.
Renaming bound variables does not change the meaning of a function. An
application MN means to apply the term M to the term N. If M happens
to be an abstraction, we’ll see below that we can do some computation. In
a sense, if M is an abstraction, we know what to do.
The scope of the binding x in the term (λx.M) is the body M minus any
parts of M that might rebind x. To see this consider the following term.
λx .(λx. x)x
↑ ↑ ↑ ↑
1 2 3 4
Occurrence (1) of x is a binding occurrence associated with the outermost
λ. Occurrence (2) is another binding occurrence and binds occurrence (3).
Occurrence (4) of x is bound by (1).
The free variables of a term are collected by the following function which
is defined by recursion on the structure of the term:
1
F V (x) = {x}
F V (MN) = F V (M) ∪ F V (N)
F V (λx.M) = F V (M) − {x}
If S and T are sets, then S − T is the set difference defined as follows:
S − T
def = {y ∈ S | y 6∈ T}
1.2 Capture Avoiding Substitution
Computation in the lambda-calculus is performed by a kind of reduction –
by computing away applications of functions (lambda abstractions) to their
arguments. This operation is defined by capture avoiding substitution. We
write M[x := N] to denote the operation of replacing all free occurrences of
x in M by the term N.
The definition is given to avoid capture. This is the situation where N
contains a free variable (say y) and N replaces an occurrence of x in M which
is in the scope of a binding occurrence of y. For example, if I naively apply
the substitution [x := y] to the abstraction (λy.xy) I get λy.yy. This second
abstraction has two bound occurrences of y while the first only had one –
we have captured y. This changes the meaning of the function. To avoid
capture we can rename, thus, before performing the substitution [x := y] in
the term (λy.xy), first can rename y to some new name, say z. We get the
new term (λz.xz). Now, naive replacement of all x’s by y does not capture
y; we get (λz.yz) preserving the structure of bound variables in the new
term. This idea is captured by the line (3c) in the definition given below.
Note that [x := N] is a substitution - a function that maps the variable x to the term N. We are using the conventional postfix notation (the
substitution comes after the term it is being applied) to denote the application of the substitution to the term; thus, if σ is a substitution and M ts
a term, we write Mσ (instead of σ(M)) to denote the term resulting from
the application of the substitution σ to the term M. Note that substitution
associates binds tightly and associates to the left.
M[x := N1][y := N − 2] means (M[x := N1])[y := N − 2]
MN[x := N1] means M(N[x := N1])
λy.N[x := N1] means λy.(N[x := N1])
Capture avoiding substitution is defined by recursion on the structure
of the lambda term. Since there are three ways to construct a lambda term
2
there are three cases in the definition; depending on whether the term being
substituted into is a variable (lines 1a and 1b), or it is an application (2) or
it is a lambda term (lines 3a, 3b and 3c). We write x ˙=y to mean that - the
meta-variables x and y denote syntactically identical (concrete) variables.
y[x := N]
def =

N if x ˙=y (1a)
y otherwise (1b)
(M1 M2)[x := N]
def = (M1[x := N] M2[x := N]) (2)
(λy.M)[x := N]
def =



λy.M if x ˙=y (3a)
λy.(M[x := N]) if x 6= y ∧ y 6∈ F V (N) (3b)
λz.(M[y := z])[x := N] if x 6= y ∧ y ∈ F V (N) ∧ z new (3c)
Lines (1a) and (1b) describe what to do when a substitution of the form
[x := N] is applied to a variable y. Line (1a) says that if x and y are the
same variable then go ahead and do the substitution, i.e. return N. If x and
y are distinct variables, line (1b) says, do nothing, just return y unchanged.
The variable case is the only case where a variable is replaced by a term,
the rest of the definition just passes through the term structure, possibly
doing some renaming if necessary to avoid variable capture further down in
the term tree.
Line (2) describes what happens then the substitution [x := N] is applied
to an application of the form (M1 M2). In this case, just construct the
application formed from the recursively constructed terms M1[x := N] and
M2[x := N].
The lambda case is more complex and is described in lines (3a), (3b)
and (3c). Line (3a) shows that if the bound variable in the term being
substituted into is identical to the variable being substituted for, then do
nothing. Recall, the idea is to replace all free occurrences of the variable
x in (λx.M) by N. But there are no free occurrences of x in (λx.M) – so
there is no point in looking any further, just return (λx.M). Lines (3b) and
(3c) show the cases where the variable being substituted is different from
the bound variable. Line (3b) shows how to proceed if there is no danger of
capture and line (3c) shows what to do if there is the danger. In line (3b),
if we know that y 6∈ F V (N) then we know that replacing free occurrences
of x by N will not capture any occurrences of y – since there are no free
y’s in N. This means, if there is an x in M and we replace it with N, we
will not capture a y. To compute the answer in this case, construct the
abstraction with bound variable y whose body is the result of recursively
substituting N for x in M. Line (3c) is the most complex. We know that
replacing a free occurrence of x in M will result in a captured instance of y.
3
To fix the problem, we choose a completely new variable name (say z) and
then rename all the y’s in M to be z and then (and only then), go ahead
an recursively substitute [x := N] into the renamed term. This renaming
idea is based on the fact that changing the names of the arguments to a
function and carefully renaming all references to the old name to the new
name will preserve the behavior of the function. The function λx.x is the
same function as λy.y.
The condition z new means z is a new variable name, i.e. z is defined
to be such that
z new
def = z ∈ V ar ∧ z 6∈ F V (M) ∧ z 6∈ F V (N) ∧ z 6∈ {x, y})
i.e. z does not occur free in either of the terms M or N and is not the
variable x or the variable y.
Problem 1.1. Your assignment is to take the base code provided with this
assignment and extend the definition of subst to implement the case for
lambda.
1.3 Beta-reduction (reading for next class)
Computation proceeds by eliminating applications of abstraction (say, of the
form (λx.M)) to some other term (say N). The reduction is performed by
capture avoiding substitution, replacing bound variable x in M (the body
of the abstraction) by the term N. This process of reducing an application
is called β-reduction (beta-reduction) and is defined as follows.
(λx.M)N →β M[x := N]
The term M[x := N] is the result of the capture avoiding substitution.
A term of the form ((λx.M)N) is called a redex and the corresponding term
M[x := N] is called the contractum.
Here are some example step-by-step computations showing which line of
the substitution algorithm is being applied at each step:
(λx.x)y →β
(1a)
z }| {
x[x := y]
= y
4
(λx.xy)y →β
(2)
z }| {
(xy)[x := y]
=
(1a)
z }| {
x[x := y] y[x := y]
= y
(1b)
z }| {
y[x := y]
= yy
(λx.λy.xy)y →β
(3c)
z }| {
(λy.xy)[x := y]
= λz.
(2)
z }| {
((xy)[y := z])[x := y]
= λz.((
(1b)
z }| {
x[y := z] y[y := z])[x := y])
= λz.((x
(1a)
z }| {
y[y := z])[x := y])
= λz.
(2)
z }| {
(x z)[x := y]
= λz.
(1a)
z }| {
x[x := y] z[x := y]
= λz.y
(1b)
z }| {
z[x := y]
= λz.y z
For arbitrary terms M and N (e.g. where M is not necessarily an abstraction we write M →β N if and only if there is a sub-term R of M such
that R is a redex and if R →β R0
, N is the term obtained by replacing the
redex R in M by R0
. This sounds more complicated that it is, all we are
saying is that M →β N if N is the result of β-reducing some subterm of M
in place.
In the following examples we have underlined the redex being reduced
and then show the computation performing the substitution.
5
z
redex
z }| {
((λx.x)y) →β zy
redex
z }| {
((λx.xy)y) z →β (yy)z
(z
redex
z }| {
((λx.λy.xy)y))w →β (z(λz.yz))w
redex
z }| {
(λx.xx)(λx.x) →β
redex
z }| {
(λx.x)(λx.x)
→β (λx.x)
Note that for some lambda terms, reduction will not terminate. Run the
provided test cases. Be sure to submit you code (in ASCII) and yor test
runs.
(λx.xx)(λx.xx) →β (xx)[x := λx.xx] = (λx.xx)(λx.xx)
6