Assignment 3

Due: Feb 11

Exercise 4.2

The Elf interpreter for Mini-ML contains some obvious redundancies. For example, while constructing an evaluation of case e₁ of z => e₂ | s x => e₃ the expression e₁ will be evaluated twice if its value is not zero. Write a program for evaluation of Mini-ML expressions in Elf that avoids this redundant computation and prove that the new interpreter and the natural semantics given here are equivalent. Implement this proof as a higher-level judgment relating derivations.

Exercise 4.3

Implement the optimized version of evaluation from Exercise 2.11 in which values that are substituted for variables during evaluation are not evaluated again. Based on the modified interpreter, implement bounded evaluation e >=n=> v with the intended meaning that e evaluates to v in at most n steps (for a natural number n). You may make the simplifying but unrealistic assumption that every inference rule represents one step in the evaluation.