Due by the start of class on Monday, February 23rd

Semantics of Impcore

  1. (Ramsey, Problem 2.15) Prove that the execution of an Impcore expression does not change the set of variables bound in the environment (with the exception of it. In other words, prove that

    The first few cases of this proof were distributed in class, of course, and you do not need to reproduce them here (simply giving them as "CASE X: see notes 01/29" will do).

  2. (Ramsey, Problem 2.18) Prove that Impcore is deterministic. That is, for any e and any environments <ξ,φ,ρ>, there is at most one <v,ξ',φ,ρ'> such that <e,ξ,φ,ρ> evaluates to <v,ξ',φ,ρ';>.

    (EXTRA CREDIT: a fully-correct version of this theorem must also account for the effect of e on the environments ξ and ρ. To really complete the proof of determinism, show also thatξ' and ρ' are unique.

  3. The deterministic character of Impcore evaluation depends crucially on the fact that evaluation order is precisely defined from left to right. For example, the rules for primitive operator application such as ApplyAdd, unambiguously constrain the evaluation of the left operand, e1 before the right (e2).

    1. Add a rule or rules to the Impcore semantics that allow a choice at any point of left to right or right-to left evaluation. As covering all of the arithmetic primitives will prove tedious, you need only choose one.

    2. Prove that determinism no longer holds in the presence of the extra rule(s). (HINT: give a counterexample, for which two distinct derivations can be shown, leading to distinct v and v'.)
  4. Extend the operational semantics of Impcore to include the declaration of local variables, by adding the following construct to the abstract syntax:

    LET(x,ei,ebody)

    The idea here, taken from the Lisp/Scheme family, is that we first evaluate ei in the current environment. The result of this evaluation is some value, v (and any potential hanges to existing bindings). We extend the "local" environment (called the "formals", ρ) with this binding and evaluate the "body" expression, body, after which, the binding x -> v is removed.

John H. E. Lasseter