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

1. Develop a metalanguage representation for the stack language.

2. Design a metafunction that counts the number of occurrences of push in a stack expression.

3. Design a metafunction that replaces all occurrences of numbers in a stack expression with 0.

4. 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)
   

5. 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.

6. 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.

7. 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.

8. 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 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 redex-check found.