G7400 F'10
Set 1
Set 2
Set 3
Set 4
Set 5
Set 6
Set 7
Set 8
Set 9
Set 10

Problem Set 5: Redex Models of ISWIM

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.


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.

last updated on Sun Nov 21 19:38:23 EST 2010generated with PLT Scheme