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
design.
Finger Problems:
Solve exercises 1.2, 1.4, and 1.6.
Problem:
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
expression language:
S is one of:
 mtS
 push(S,e)
 pop(S)
e is one of:
 a number n
 add1(e)
 depth(S)
 top(S)
The interpretation is the usual one:
mtS
is the empty stack;
push
places a number n
onto an existing stack S
;
top
retrieves the last element that was pushed;
pop
retrieves the last stack onto which an element was pushed;
and depth
determines how many elements the stack contains.
You may imagine that add1(e) is a placeholder for more complex
forms of expressions.
Tasks

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:
 mtS
 push(nS,n)

Develop a basic notion of reduction R for the stack expression
language. The notion of reduction should interpret all operations in the
specified manner.
This task demands that you extend the stack language with a collection of
S contexts.
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
expressions.

At this point you may conjecture that eval> and
evalS will always produce the same result when given the same
stack expression.
Formulate this conjecture with redexcheck. Borrow
equal? from Racket to compare terms. Report the counterexample
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
redexcheck found.