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

Sale!