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.

**Problem 1**:

The goal of this exercise is to equip the calculational model of
arithmetic from class with three additional operations: `-`

,
`*`

, `if0`

:

```
(define-language Expressions
(e n
(e + e)
(e * e)
(e - e)
(e / e)
error
x
(if0 e e e))
(n number))
```

The interpretation of the operations is the obvious one. In particular, an
`if0`

expression reduces to the second sub-expression if its
first one reduces to `0`

and to the third sub-expression
otherwise.
Also the model comes with `error`

so that your model can deal
with division by 0. Specifically, your model should reduce expressions
such as `(1 / 0)`

to `error`

, and operations that
encounter `error`

should propagate it, e.g., ```
(1 +
error)
```

should reduce to `error`

.

The variable `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
documentation.

**Background for Problems 2 through 4**:

All remaining problems in this assignment refer to this core grammar:

```
(define-language Lambda0
(e x
(lambda (x) e)
(e e))
(x variable-not-otherwise-mentioned))
```

This language is defined and exported from the library module
`"4provided.rkt"`

. In addition to the
language, the module provides a capture-avoiding substitution function,
`subst-n`

.
Save the module under its given name and add
` (require "4provided.rkt")`

to your solution file. Do not modify the module. Program to its interface
only.

**Problem 2**:

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
terms in `Lambda0`

are indeed α-equivalent:

```
;; 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))
```

It assumes the definition of the function `sd`

, which
translates a `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.
Design the `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 `dummy`

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
comparison via `equal?`

in `alpha=`

above.

**Problem 3**:

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.

**Problem 4**:

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.