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

The goal of this problem set is to understand abstract syntax machines.
**Note:** Problems 0 and 1 are "warm up" exercises and serve
as the platform for the problems 2 and 3, which are independent of each
other.

Revised on 19 Oct 2010.

**Background**:

All problems in this assignment refer to this core grammar:

```
(define-language ISWIM0
(e x ;; parameter reference
(lambda (x) e) ;; procedures
(e e) ;; application
(if0 e e e) ;; branching on 0
n ;; numbers
(op e e)) ;; primitive operations
(op + ;; addition
- ;; subtraction
* ;; multiplication
^) ;; exponentation
(n number)
(x variable-not-otherwise-mentioned))
```

Furthermore, to help you along, this assignment comes with the definition
of a substitution metafunction for Redex-style languages whose only
'binder' is lambda (see bottom).
Both pieces are provided via library module
that exports two identifier: `ISWIM0`

and
`subst-n`

. Save the module and add
` (require "5provided.rkt")`

to yours. Do not modify the module; I will link
your solution against my version of the module not yours.

**Problem 0**:

Design the **meta**function `=alpha`

, which
consumes two expressions in `ISWIM0`

and determines whether
they are α-equivalent. Compare with problem set 4(0).

**Problem 1**:

Develop a Redex model of the standard reduction semantics for
call-by-value `ISWIM0`

. Challenge: Add reduction rules that
take stuck states to `(term STUCK)`

.

**Problem 2**:

Extend `ISWIM0`

(or the language from
problem 1) with another collection of data of your
choice. Anything that Redex accommodates is acceptable except for
booleans.

**Problem 3**:

Extend ISWIM0 (or the languages from
problems 1 and 2) with a `rec`

construct:

` (rec x (lambda (x) e) in e)`

The tokens `rec`

and `in`

are keywords.
In the concrete instance,

` (rec x (lambda (x_1) e_1) in e)`

`x`

is bound in both `e_1`

and `e`

while
`x_1`

is bound only in `e_1`

. The evaluation of this
expression creates a recursive function that satisfies the equation
` (x x_1) = e_1`

and binds it to `x`

during the evaluation of `e`

.
The result of the latter is the result of the entire expression.

**Problem 4**:

Develop and prove a standard reduction theorem for language `B`

from chapter I.1 in the text.