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
Calculus.
Background:
All problems in this assignment refer to this core grammar:
(definelanguage Lambda0
(e x
(lambda (x) e)
(e e))
(x variablenototherwisementioned))
Furthermore, to help you along, this assignment comes with the definition
of a substitution metafunction for Redexstyle languages whose only
'binder' is lambda (see bottom).
Both pieces are provided via library module
that exports two identifier: Lambda0
and
substn
. Save the module and add
(require "4provided.rkt")
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
text book.
Problem 0:
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 twostep procedure. First, translate the given expressions
into the socalled "static distance" notation of problem
set 1, problem 4, though without leaving the parameter list in
place. Second, once the staticdistance 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.)
Problem 1:
Define terms in Lambda0
that encode the booleans
True
and False
; the Church numerals
Zero
, One
, and Two
; the
Add1
function and the Iszero
function; and the
If
conditional.
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
back separately.
Use the model to confirm the αequivalence of

(Add1 Zero)
and One

(Add1 One)
and Two

(((If True) M) N)
and M

(((If False) M) N)
and M

(Iszero Zero)
and False
The confirmations should take the shape of
(check =alpha ... ...)
statements in your Racket modules.
Problem 2:
Use the consistency result of chapter I.3 to design
=beta/semi
, a semialgorithm in Racket for equality (module
αequivalence) in the lambda calculus.
Here a semialgorithm 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 semialgorithm to solve exercise 3.15, i.e., ensure that the
algorithm can validate the following unit test:
(check =beta/semi (term (M (,Y M))) (term (,Y M)))
for a suitable definition of Y
.
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)
produces true
for any i
in 1, ..., 5.
Should the two terms produce identical fixed points?
Problem 3:
Use defineextendedlanguage
to extend Lambda0
to the syntax of the numeric variant of ISWIM (chapter I.4 [page
48]). Then specify a reductionrelation
that implements a
Redex model of the β_{v} reduction relation for ISWIM plus
the δ function for numerical primitives plus the if0
macro. Finally define the eval
function from I.4.5 as a
Racket function.
You do not need to design an αequivalence relation for this
exercise. You should develop a reasonably comprehensive test suite for
eval
, however.