Due date: 10/29 @ at the beginning of class

The goal of this problem set is to continue the exploration of abstract
syntax machines, Redex, and the idea of correctness of implementations.

**Problem 1**:

Implement the standard reduction semantics of one of the three variants of
ISWIM (from problems 5(1), 5(2), or 5(3)) in the programming language of
your choice. Your implementation
must (1) produce the same results as the standard reduction semantics
(2) print the evaluation context and the reducible expression for each
step. Use the `traces`

function from the Redex library like
this

` (traces ->iswim (term ((lambda (x) (+ x 1)) (+ 10 20))))`

to study reduction sequences. You do not need to supply tests for the
print effect of your program.
If the programming language of your choice is not Racket, it must include
an XML library and you must be familiar with programming XML in this
language. Also, please let me know immediately if you will not work with
Racket.

**Problem 2**:

Extend the model of the ISWIM language of problem 5(2) with global
definitions. That is, a program should now consist of a sequence of
definitions followed by an expression. The definitions should look like
Racket definitions, binding names (variables) to values. Both the last
expression in a program and the right-hand sides of the definitions may
refer to the defined names.

Here is a complete sample program:

```
(define evenP (lambda (x) (if0 x 0 (oddP (- x 1)))))
(define oddP (lambda (x) (if0 (- x 1) 0 (evenP (- x 1)))))
(oddP 13)
```

**Challenge**
In Racket, definitions allow arbitrary expressions as right-hand
sides. Revise your ISWIM model to admit such definitions.

Make sure to test your model adequately.

**Problem 3**:

Prove the following claim:

If
`e =`_{v} e'

then
```
e
⇾
```_{v} e_{0}
_{v}⇽ e_{1}
⇾_{v} e_{2}
_{v}⇽ ...
⇾_{v} e_{n-1}
_{v}⇽ e_{n}
⇾_{v} e'

The relation ⇾_{v} denotes the reduction generated by the
notion of reduction **v**, i.e., its transitive-reflexive and
compatible closure.