- 7th Sep 2021
- 04:31 am
- Admin
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