Module 11: Small-step reduction

This module is due at 1:15pm on Tuesday, October 18.

Write your team names here:
Pick an initial driver and write their name here:
Begin by pasting in your most recent implementation of the Arith language.
I promise that after fall break we will be done with Arith. ;-)

Bound variables

Consider the expression let x = e1 in e2. We say that this expression binds the variable x, that is, it introduces a local definition for x. We say that x is bound in e2, that is, any occurrences of x in e2 refer to the x defined by the let. (However, x is not bound in e1—we will think more about this later.)

For example, in

let x = 2+3 in x + if x < 10 then 3 else 7

both occurrences of x after the in refer to the x defined by the let, so this expression evaluates to 8.

Actually, it is not quite true that any occurrence of x in e2 refers to the x defined by the let. We have to take shadowing into account. For example, consider this expression:

let x = 5 in let x = 6 in x + x

What does this evaluate to, 10 or 12?
Why?
What does this expression evaluate to (be sure to guess before trying it)?
```
let x = 2+3 in let x = 2*x in 4+x
```
(Hint: remember that in let x = e1 in e2, x is bound in e2 but not in e1.)
What would it mean if let x = e1 in e2 bound x in both e1 and e2?
Do you think this could be a useful feature for the Arith language?
Try evaluating let x = 2+3 in let x = 2*x in 4+x as a Haskell expression (that is, just type it at a GHCi prompt). What do you think this means about let in Haskell?

Free variables and substitution

ROTATE ROLES and write the name of the new driver here:

A variable is free if it is not bound. For example, in the expression

let x = 2 in x + y

The x is bound, but y is free.

Write a function fv :: Arith -> S.Set String which computes the set of free variables of an Arith expression. You should add
```
import qualified Data.Set as S
```
at the top of the module; see the documentation for Data.Set here.

We won’t actually need the fv function, but it is a good warm-up exercise for thinking about bound and free variables.
Now write a substitution function,
```
subst :: String -> Arith -> Arith -> Arith
```
subst x e1 e2 should result in e2, but with every free occurrence of x replaced by e1. For example,
```
subst x 3 "x + let x = x+1 in x*6"  =  "3 + let x = 3+1 in x*6"
```
In the above example every free occurrence of x is replaced by 3, but the bound occurrences of x are left alone. (The above is not actually valid syntax; I am using strings as a shorthand for their parsed Arith equivalents. To help test subst and other functions later, it may be helpful to write a function p :: String -> Arith which tries to parse the given String and simply crashes with error if it does not. Then you can actually write things like subst "x" (p "3") (p "x + let x ...").)

Small-step reduction

ROTATE ROLES and write the name of the new driver here:

When we have written interpreters before, they have used what is called a big-step semantics: for example, they take an Arith and simply reduce it to a value in one “big step”. There is no way to extract any sort of intermediate expressions or states from the interpreter: running the interpreter is an all-or-nothing sort of operation.

We will now consider an alternative model, where we define what it means for an expression to take a (small) reduction step, resulting in another expression. A reduction step changes as little as possible while still making nontrivial progress. We can then write an interpreter by repeatedly applying reduction steps until the expression cannot take any more steps. For example, consider the expression if 3 + 5 < 7 then 2*5 else (let x = 3 in x+x). The interpArith function would simply take this expression and return 6 (by making recursive calls to interpArith to evaluate the subexpressions, and so on). On the other hand, if we evaluate the expression by repeatedly applying small reduction steps, it would reduce as follows:

if 3 + 5 < 7 then 2*5 else (let x = 3 in x+x)
if 8 < 7 then 2*5 else (let x = 3 in x+x)
if False then 2*5 else (let x = 3 in x+x)
let x = 3 in x+x
3+3
6

Writing an interpreter in this style is usually inefficient compared to a direct (big-step) implementation, but it can be a very useful way to think and reason about the semantics of a language. It is often useful to define both small-step and big-step semantics for a language, along with a formal proof that the two give equivalent results.

Write a function step :: Arith -> Maybe Arith which implements one step of reduction. If the input Arith cannot take a step (either because of an error, or because there is no more reduction left to do), step returns Nothing. Some notes to help you in your implementation are below, with keywords highlighted. Start writing your implementation and consult the list of notes as you go.
- Of course, literals cannot take a step.
- Variables cannot take a step either. Note we are not going to pass along an environment mapping variables to values, as we did with interpArith. A variable by itself simply cannot take a step. You will see how to deal with variables when you get to let.
- To step an application of a binary operator, $e_1 \mathbin{op} e_2$:
  1. First see if the left-hand argument $e_1$ can take a step (by calling step recursively). If $e_1 \longrightarrow e_1'$ (that is, $e_1$ can successfully take a step, resulting in $e_1'$), then the result of stepping $e_1 \mathbin{op} e_2$ is $e_1' \mathbin{op} e_2$.
    
    For example, "(3+2) * (2*3)" steps to "5 * (2*3)". (Again, these strings are really just standing in for appropriate parsed Arith values.)
  2. Otherwise, if the left-hand argument cannot take a step, see if the right-hand argument can take a step. For example, "5 * (2*3)" steps to "5 * 6".
  3. If neither argument can take a step, then see if they are both literals appropriate to the operator. If so, do the operation. For example, given "5 * 6", neither side can take a step (since they are already literals), so the whole expression steps to "30".
  4. Remember to check for division by zero. Instead of generating an error, however, an expression like "5 / 0" simply cannot take a step; it is “stuck”.
  5. Otherwise (e.g. if you have something like "5 + True"), the operator cannot take a step.
- I will let you think about if and let on your own. A few hints:
  - Use the example reduction from above (of if 3 + 5 < 7 then 2*5 else (let x = 3 in x+x)) to help guide you.
  - Remember the subst function!
- Once you get to the point where you are annoyed by pattern-matching on Maybe, consider these questions:
  - What is the type of Bin op <$> step e1 <*> Just e2? What does it evaluate to?
  - What is the type of
```
(Bin op <$> step e1 <*> Just e2) <|> (Bin op <$> Just e1 <*> step e2)
```
    ? What does it evaluate to?
  - Can you use these tools to write step without ever explicitly writing a case on the results of recursive calls to step?
Now write a function reduce :: Arith -> Arith which simply iterates step until the expression cannot take another step, and returns the final, un-steppable expression.
Finally, write a function eval2 :: String -> IO () which works similarly to eval but uses reduce instead of interpArith. You can use this to test your implementation of step, to make sure that stepwise reduction yields the same results as interpArith.

Feedback

How long would you estimate that you spent working on this module?
Were any parts particularly confusing or difficult?
Were any parts particularly fun or interesting?
Record here any other questions, comments, or suggestions for improvement.