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

Problem Set 6: Standard Reduction for Flavors of ISWIM

Due date: 10/28 @ at the beginning of class

The goal of this problem set is to understand abstract syntax machines, i.e., standard reduction sequences.


You should import "6provided.rkt" It provides large fragments of a solution for problem set 5. If you prefer your own, you may copy the relevant parts of your solution.

Problem 1:

Develop a reduction model of the standard reduction semantics for call-by-value ISWIM* in Redex.

Define the function eval*-s, which maps closed ISWIM* expressions to the same kind of answers as eval*-v from problem set 5, problem 3.

Show how to define the ISWIM* functions sum and product. Both consume lists of numbers. The first one adds, the second one multiplies the numbers in the list.

Formulate a conjecture about the relationship between eval*-v and eval*-s as a metafunction. Test the conjecture with redex-check.

If testing finds a counter-example to your conjecture, formulate the counter-example as a failing test case and explain the failure with a one-line (max 80 chars) comment. Then comment out your redex-check line and the test case. Next, define new versions of the two evaluator functions and the metafunction that formulates the conjecture. (Append .v2, .v3 and so on to the names of the functions you need to redefine.) Do not edit existing functions so that it is possible to reconstruct the failure.

Repeat the above until redex-check succeeds for its default number of test attempts if it terminates. Explain why this conditional is necessary in fewer than 43 words and how it hints at a difference between the two evaluators.

Problem 2:

Revise function application from problem 1 to accommodate multi-argument functions in two different ways:

  1. First, introduce lambda expressions with an arbitrary number of parameters and function applications with an arbitrary number of arguments.
  2. Second, introduce mu-lambda expressions, which have a single non-parenthetical parameter. When applied to n values, a mu-lambda consumes all of these values in an ISWIM* list.
Equip your revised model with a call-by-value notion of standard reduction. (There is no need for a general one-step reduction.) Also formulate an eval metafunction.

A standard reduction fixes an order of evaluation. Is it possible to discover which order is chosen (not counting precision of floating number operations, which as you know from problem set 3 is independent of the order of reduction for sub-expressions). If so, how. If not, why not. Limit your answer to at most 65 words.

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