Programming Languages Concepts

CSE 461: Programming Languages Concepts

Solutions: Homework 5
 

1. Given the lambda-calculus term (λf · λx · f(f x))(λy · y ∗ 3)2. Using beta reduction, we
reduce it to the normal form as follows

(λf · λx · f(f x))(λy · y ∗ 3)2 −→ β (λf · λx · f(f x))(2 ∗ 3)

−→ β (λf · λx · f(f x))6. Put f x = λx · x
−→ β (λf · λx · f(λx · x))6
−→ β λx ·(6)(λx · x)
−→ β (λx · 6)(λx · x)
= 6

 

2. We say λx · e binds the variable x with scope e. Variables that occur in e but are
not bound are called free variables, and we say that a variable x may occur free in an
expression e. For example, y is free in λx·x y but not x. Given the lambda-calculus term
(λx · λy · y x)(λz · y), we have
(a) The set of free variables of M, denoted by FV(M), is defined inductively as follows.

F V (x) = {x}
F V (M N) = F V (M) ∪ F V (N)
F V (λx · M) = F V (M) − {x}

Now, let M = (λx · λy · y x) and N = (λz · y). Therefore, using FV function we get

F V (M N) = F V (λx · λy · y x) ∪ F V (λz · y). Put y x = λx · x

= [F V (λy · λx · x) − {x}] ∪ [F V (y) − {z}]
= [F V (λx · x) − {y} − {x}]∪ [{y} − {z}]
= [F V (x) − {x} − {y} − {x}] ∪ [{y}]
= [{x} − {x} − {y} − {x}] ∪ {y}
= ∅ ∪ {y}
= {y}

Hence, y is the free variables of the given lambda-calculus term.
(b) Given the lambda-calculus term (λx · λy · y x)(λz · y). The bound variables in the
first term are x and y. We rename x with p and y with q in the first term. Using
beta reduction, we reduce it to the normal form as follows

(λp · λq · q p)(λz · y) −→ β (λp · λq · λp · p)(λz · y)
−→ β (λp ·(λq ·(λp · p)))(λz · y)
= (λq ·(λp ·(λz · y)))

(c) If, however, we did not rename the bound variables, we wouldn’t manage to reduce
the given problem to normal form by applying beta-reduction technique.
3. Given the following Algol-like program fragment:

function f(x)
return x-3
end;
function g(y)
return 4+y
end;
f(g(10));

(a) We need to convert the above program into an equivalent lambda-calculus term.
From the program, we have f(x) = x − 3 and g(y) = 4 + y. The lambda-calculus
term for each function is

f = λx · x − 3 and g = λy · y + 4

The functional composition is denoted by (fog)(x) = f(g(x)). Having λ-notation we

can first explicitly denote the result of composition (with some redundant parenthe-
ses)

fog = λx · f(g(x))

As a second step, we realize that o itself is a function, taking two functions as
arguments and returning another function. Ignoring the fact that it is usually written
in infix notation, we define

o = λf · λg · λx · f(g(x))

 

Therefore, the equivalent lambda-calculus term of the above program is

f = λx · x − 3
g = λy · y + 4
f(g(10)) = ((o(f))(g))10

= (((λf · λg · λx · f(g(x)))(λx · x − 3))(λy · y + 4))10
(b) Now we can calculate f(g(10)) by applying the β-conversion as follows.
f(g(10)) = (((λf · λg · λx · f(g(x)))(λx · x − 3))(λy · y + 4))10
−→ β ((λg · λx ·(λx · x − 3)(g(x)))(λy · y + 4))10
−→ β (λx ·(λx · x − 3)((λy · y + 4)(x)))10
−→ β (λx ·(λx · x − 3)(x + 4))10
−→ β (λx ·(x + 4) − 3)10
−→ β (λx · x + 1)10
−→ β 10 + 1
= 11