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 e0 v⇽ e1 ⇾v e2 v⇽ ... ⇾v en-1 v⇽ en ⇾v e'

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