Due date: 10/15 @ at the beginning of class
The goal of this problem set is to understand the basics of the Lambda
calculus as a computing system and to increase your familiarity with
Redex and its interaction with Racket.
Warning: It is nearly impossible to solve the problems 0
through 2 of this problem set separately. They are closely related and it
is best to proceed sequentially. Problem 3 is about ISWIM, not the Lambda
All problems in this assignment refer to this core grammar:
Furthermore, to help you along, this assignment comes with the definition
of a substitution metafunction for Redex-style languages whose only
'binder' is lambda (see bottom).
Both pieces are provided via library module
that exports two identifier:
(lambda (x) e)
subst-n. Save the module and add
to yours. Do not modify the module; I will link
your solution against my version of the module not yours.
In contrast to the text book, your lambda calculus model is used modulo
α-equivalence, an idea that is spelled out in chapter I.4 of the
Design the function
=alpha, which consumes two expressions in
Lambda0 and determines whether they are α-equivalent.
Hint: One way to compute α-equivalence efficiently
is to use a two-step procedure. First, translate the given expressions
into the so-called "static distance" notation of problem
set 1, problem 4, though without leaving the parameter list in
place. Second, once the static-distance representation has been computed,
it suffices to use
equal? to compare the results. (A
proof of this idea can be found in the appendix of Barendregt's tome on
the Lambda Calculus, Its Syntax and Semantics.)
Define terms in
Lambda0 that encode the booleans
False; the Church numerals
Add1 function and the
Iszero function; and the
Develop a Redex model of the lambda β calculus.
That is, the model should use β as the only notion of reduction.
As for the η notion of reduction, it is ignored; α is brought
Use the model to confirm the α-equivalence of
The confirmations should take the shape of
(Add1 Zero) and
(Add1 One) and
(((If True) M) N) and
(((If False) M) N) and
(Iszero Zero) and
statements in your Racket modules.
(check =alpha ... ...)
Use the consistency result of chapter I.3 to design
=beta/semi, a semi-algorithm in Racket for equality (module
α-equivalence) in the lambda calculus.
Here a semi-algorithm is a function that produces true
(meaning the given terms are equal) in some cases but may diverge in
others. What does divergence mean? In order to make this function total,
equip it with an optional fuel argument that is suitable decreased and
that causes the function to stop when it is zero or negative.
Use the semi-algorithm to solve exercise 3.15, i.e., ensure that the
algorithm can validate the following unit test:
for a suitable definition of
(check =beta/semi (term (M (,Y M))) (term (,Y M)))
Finally investigate whether
(define Apply (term (lambda (f) (lambda (x) (f x)))))
(define Ident (term (lambda (x) x)))
(=beta/semi (term (,Y Ident)) (term (,Y ,Apply)) i)
true for any
i in 1, ..., 5.
Should the two terms produce identical fixed points?
define-extended-language to extend
to the syntax of the numeric variant of ISWIM (chapter I.4 [page
48]). Then specify a
reduction-relation that implements a
Redex model of the βv reduction relation for ISWIM plus
the δ function for numerical primitives plus the
macro. Finally define the
eval function from I.4.5 as a
You do not need to design an α-equivalence relation for this
exercise. You should develop a reasonably comprehensive test suite for