Due date: 9/30 @ at the beginning of class
The goal of this problem set is to understand reduction relations in
the spirit of chapter I.1 of the Redex book, both in theory and in
practice. The latter continues the introduction to systematic program
Solve exercises 1.2, 1.4, and 1.6.
A famous characterization of APIs (application programming interfaces) is
that they are languages waiting to be liberated. In this exercise, we deal
with one of these APIs, the language of stacks.
Here is a sketch of a stack API's syntax and its integration with some
S is one of:
e is one of:
-- a number n
The interpretation is the usual one:
mtS is the empty stack;
push places a number
n onto an existing stack
top retrieves the last element that was pushed;
pop retrieves the last stack onto which an element was pushed;
depth determines how many elements the stack contains.
You may imagine that add1(e) is a placeholder for more complex
forms of expressions.
Develop a metalanguage representation for the stack language.
Design a metafunction that counts the number of occurrences of
push in a stack expression.
Design a metafunction that replaces all occurrences of numbers
in a stack expression with 0.
Design the metafunction evalS. The function maps stack
expressions to normalized stack expressions. This task demands that
you extend the stack language with a language of normalized stacks:
nS is one of:
Develop a basic notion of reduction R for the stack expression
language. The notion of reduction should interpret all operations in the
This task demands that you extend the stack language with a collection of
Implement your model in Redex via a language and a reduction system.
Notions of reductions are relations. In contrast to a function, a relation
pairs up several "results" with a given "input". If this is true for your
notion of reduction for the stack language, create an expression that has
at least two paths to a normalized stack using a traces expression.
As the book explains, even relations can be used to define a mathematical
evaluation function. Design the metafunction eval->, which
uses your notion of reduction to map stack expressions to normalized stack
At this point you may conjecture that eval-> and
evalS will always produce the same result when given the same
Formulate this conjecture with redex-check. Borrow
equal? from Racket to compare terms. Report the counter-example
that it finds via a failing test case at the bottom of your file.
Finally make a suggestion as to how to eliminate the problem that