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
Revised on 19 Oct 2010.
All problems in this assignment refer to this core grammar:
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:
(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
subst-n. Save the module and add
to yours. Do not modify the module; I will link
your solution against my version of the module not yours.
Design the metafunction
consumes two expressions in
ISWIM0 and determines whether
they are α-equivalent. Compare with problem set 4(0).
Develop a Redex model of the standard reduction semantics for
ISWIM0. Challenge: Add reduction rules that
take stuck states to
ISWIM0 (or the language from
problem 1) with another collection of data of your
choice. Anything that Redex accommodates is acceptable except for
Extend ISWIM0 (or the languages from
problems 1 and 2) with a
(rec x (lambda (x) e) in e)
in are keywords.
In the concrete instance,
(rec x (lambda (x_1) e_1) in e)
x is bound in both
x_1 is bound only in
e_1. The evaluation of this
expression creates a recursive function that satisfies the equation
and binds it to
(x x_1) = e_1
x during the evaluation of
The result of the latter is the result of the entire expression.
Develop and prove a standard reduction theorem for language
from chapter I.1 in the text.