Type Systems, Exc. 1 Arithmetic expressions
English only

### Exercise 1 Arithmetic Expressions

In this exercise, you are asked to familiarize yourself with Scala by implementing an evaluator for arithmetic expressions. The grammar of expressions is repeated here (production E). An expression is sometimes also called term. Some terms are called values(prod. V) and of these, some are numeric values (prod. NV).

 ```E ::= true false zero succ E pred E iszero E if E then E else E```
 ```V ::= true NV ::= zero false succ NV NV ```

An evaluation means reducing terms until they are no longer reducible. If all goes well, the result is a value. If it is not a value, then evaluation is stuck. The behaviour of an evaluator can be described concisely by writing deduction rules of the form

 pre1   ...   preN conc

Such a rule says, that if all premises hold, than the conclusion holds. If there is just a conclusion and no premises, then the line is omitted. Here, we are interested in the reduction relation →. It is a binary relation on terms, where "a → b" says than we can reduce a to b.

The reduction relation for arithmetic expressions was given in the course . Let's repeat them here:

Computation Congruence
 if true then E1 else E2 → E1 if false then E1 else E2 → E2 isZero zero → true isZero succ NV → false pred zero → zero pred succ NV → NV
 E → E' if E then E1 else E2 → if E' then E1 else E2
 E → E' isZero E → isZero E'
 E → E' pred E → pred E'
 E → E' succ E → succ E'

The meta variables `E, E', E1, E2, NV` stand for arbitrary terms generated by the corresponding grammar production. Note that computation rules for `isZero` and `pred` are defined for numeric values, not arbitrary terms.

### Preparation

1. First, setup your environment following the instructions (in French).
3. make a directory "types2004" and unpack the jarfile with `jar xf expr.jar`.
4. In that directory, you can compile your program with
`scalac -d classes src\arithexpr\*.scala`
and run it with
`scala arithexpr.Main [-print] <sourcefile>`
You might find the quick overview of Scala syntax useful

Write an evaluator that reduces terms according the reduction relation.

Start by completing method `toString()` in `arithexpr.Expr`. You can test whether printing works by using the `-print` option, e.g.

```scala arithexpr.Main -print test/test1.expr
```

This does not run the evaluator.

Then proceed to the methods in `arithexpr.Evaluator`.

Give one term whose evaluation gets stuck (which does not reduce to a value).

### Errata

Please note this error in `EvaluatorPhase.scala`
```  /** evaluates an expression */
def apply(t: Expr): Expr = {
val s = eval(t);
if(!isVal(s)) { // instead of !isVal(t)
Console.println("Evaluation is stuck.");
}
s
}
```
This is a good example of an programming error that no type system will find :-/.

### Solution

Here are the complete files Expr.scala and EvaluatorPhase.scala.

### Remarks

The implementation of the exercise yields an interpreter that is not very efficient. However, it is easy to see that it corresponds exactly to the definition of the reduction relation.

It can be seen that congruence rules are just there to recursively search for redexes. The only interesting thing about congruence rules is, where they lead the search for redexes. Note that a premise `E → E'` translates directly to a recursive call `reduce(E)` to obtain `E'`. Note further that congruence rules have to come after computation rules in the pattern match, because for the Scala compiler, the pattern in the conclusion of a congruence rule is always 'more general' then the pattern for a computation rule. If congruence rules would come first, they would always match and redexes would not be found correctly.

In the given framework, `reduce` is called from within a loop until a `NoRuleApplies` exception is thrown. This can only work if a call to `reduce` really makes the term smaller using a computation rule, or throws an exception.