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.
Background:
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:
-
First, introduce
lambda expressions with an arbitrary number
of parameters and function applications with an arbitrary number of
arguments.
-
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.