Due date: 10/14 @ 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's testing facilities.
The goal of this exercise is to equip the calculational model of
arithmetic from class with three additional operations:
The interpretation of the operations is the obvious one. In particular, an
(e + e)
(e * e)
(e - e)
(e / e)
(if0 e e e))
if0 expression reduces to the second sub-expression if its
first one reduces to
0 and to the third sub-expression
Also the model comes with
error so that your model can deal
with division by 0. Specifically, your model should reduce expressions
(1 / 0) to
error, and operations that
error should propagate it, e.g.,
error) should reduce to
x is to remain uninterpreted. It serves as a
reminder that this kind of expression language could appear as a part of
a full-fledged programming language.
Equip the model with a collection of test reductions that show that the terms
are reduced to normal form. Since testing reductions is a common activity
for semantics engineers, Redex comes with appropriate constructs. See
Background for Problems 2 through 4:
All remaining problems in this assignment refer to this core grammar:
This language is defined and exported from the library module
(lambda (x) e)
"4provided.rkt". In addition to the
language, the module provides a capture-avoiding substitution function,
Save the module under its given name and add
to your solution file. Do not modify the module. Program to its interface
In contrast to the text book, this homework explores the lambda calculus
model modulo α-equivalence, an idea that is spelled out in chapter
I.4 of the text book.
Here is a definition of a Racket function that determines whether two
Lambda0 are indeed α-equivalent:
It assumes the definition of the function
;; e[Lambda0] e[Lambda0] -> Boolean
;; are t1 and t2 alpha equivalent?
(define (alpha= t1 t2)
(define sd1 (term (sd ,t1)))
(define sd2 (term (sd ,t2)))
(equal? sd1 sd2))
Lambda0 term into the so-called
"static distance" notation of problem set 1, problem
5. In class, this form is referred to as the "arrow" form of terms.
sd function and all necessary auxiliaries in
Redex. Do not escape to Racket for any reason.
In addition to replacing bound variables into static distance
numbers, the function must also change all parameters to
or some other fixed name. Doing so is legitimate because parameter names
no longer play a role in static-distance notation. It enables the simple
Develop a Redex model of the lambda β calculus.
That is, the model should use β as the only notion of reduction.
Demonstrate with three reduction tests that the model can reduce
Lambda0 to normal form, i.e., to terms that do not contain a
β redex. At least one of the tests must demonstrate that doing so may
require several steps. Another test must demonstrate that you can predict
the outcome only up to α equivalence.
Implement the stacks from problem set 2 via
Lambda0 expressions. Do not use recursion, i.e.,
the Y combinator. Instead use the OO-encoding model.
Demonstrate with reduction tests that the expressions implement the
reduction laws of stacks for concrete examples. Note: when I worked
through this exercise, I had to disable 'debugging' in DrRacket to get
decent performance. I only did so after debugging the model of course.