Teaching G7400 F'11 Assignments Set 1 Set 2 Set 3 Set 4 Set 5 Set 6 Set 7 Set 8 Set 9

### Problem Set 5: From Lambda to ISWIM

 Due date: 10/21 @ at the beginning of class The goal of this problem set is to revisit representations in the lambda calculus and to get acquainted with ISWIM. Background: The file "5provided.rkt" provides all the items that "4provided.rkt" provides, plus a reduction relation that implements beta one-step, a Racket function that determines α equivalence, and several useful `Lambda` terms (for booleans and pairs). The latter come with verified equations. Problem 1: An alternative way to encode numerals in `Lambda` is to say that `0` corresponds to the identity function and that `n+1` is represented by the pair of `ff` (false) and the representation of `n`. Your first task is to design a metafunction that maps Racket's natural numbers to their numeral representation in `Lambda`. Your second task is to define `Lambda` representations of the following functions on natural numbers: `succ`, which creates the successor for a given numeral; `pred`, which extracts `n` from the representation of `n+1`; and `iszero`, which produces `tt` (true) for `0` and `ff` for all other numerals. Third, formulate reduction tests that show that your functions satisfy or falsify the following properties for numerals `n`: `````` (iszero zero) =β tt (iszero (succ n)) =β ff (pred (succ n)) =β n (succ (pred n)) =β n `````` Warning: do not use `redex-check`. Use small numbers for which the tests terminate in a reasonable amount of time (less than 30s). Finally, prove the above properties unless you have falsified them. Each line in your proof must either justify the step as "by def. of ..." or as "by beta" or "by equation for ...". You may collapse several (un)foldings of definitions or several beta steps into one line. Keep the proofs concise. Problem 2: Develop a model of the numeric variant of ISWIM (chapter I.4 [page 48]). The model should provide the βv reduction relation for ISWIM plus a δ reduction relation for the numerical primitives. Also equip the language with an `if0` construct, though introduce a syntactic reduction that just translates an `if0` expression into an expression in the rest of the language. Define the `eval-v` function, which maps closed ISWIM expressions to numbers if they are provably reducible to numbers and `'closure` if the are provably reducible to `lambda` expressions. Recall that our `eval-v` functions are partial on their domain. Use the imports from "5provided.rkt" to reduce your work load. Problem 3: Extend the language of problem 2 with a Racket-style lists data type. It should come with the following constants and functions: `empty`, `empty?`, `cons`, `cons?`, `first`, and `rest`. Like in Racket, `cons` combines two values into one, and a list is a tree of `cons`es (of values) whose right-most spine ends in `empty`. We call the extended language ISWIM*. Define the `eval*-v` function, which maps closed ISWIM* expressions to numbers, `empty`, or `cons` trees of values if they are provably reducible to those or `'closure` if the are provably reducible to `lambda` expressions.

 last updated on Tue Nov 15 15:51:00 EST 2011 generated with Racket