Teaching G7400 F'10 Assignments 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. 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.

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