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 metafunction =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.