Assignment: Operational Semantics

From exercise 10 on page 79 of Build, Prove, and Compare, complete parts (a) and (d). Your informal English must not use any symbols that refer to environments—talk about environments using your knowledge of what names stand for. Make your explanations as simple as possible, and use only language that a COMP 11 student would understand. (In other words, it is OK to talk about “variables,” but it is not OK to talk about “environments.”)

From exercise 11 on page 79 of Build, Prove, and Compare, complete parts (a), (c), and (d). Notes:

• The convention of the field is that new metavariables are implicitly universally quantified. For example, if you just write a global-variable environment ξ, you’re assumed to be talking about any possible ξ. If what you’re saying is true for just some environments, the conventional opening is to say “there exists a ξ such that.” (Or more likely, “There exist ξ, ϕ, ρ, v, ξ′, and ρ′ such that.”)

• If you need to write an implication, use the words “if” and “then.” Do not use inference-rule notation—every new inference rule adds a case to every metatheoretic proof.

• Some of the statements in this problem most easily formalized in the form “if evaluation judgment then conclusion.”

Exercise R. The following notation suggests an alternative to the WhileEnd rule of Impcore. Either explain why this rule is effectively the same as the original rule, or explain why it’s different.

          ⟨e1,ξ,φ,ρ⟩ ⇓ ⟨0,ξ′,φ,ρ′⟩
  ---------------------------------------- (WhileEnd')
  ⟨while(e1, e2), ξ, φ, ρ⟩ ⇓ ⟨0, ξ′, φ, ρ′⟩

The following notation suggests an alternative to the FormalAssign rule of Impcore. Either explain why this rule is effectively the same as the original rule, or explain why it’s different.

    x ∈ dom ρ    ⟨e,ξ,φ,ρ⟩ ⇓ ⟨v,ξ′,φ,ρ′⟩
  ------------------------------------------------ (FormalAssign')
  ⟨set(x, e), ξ, φ, ρ⟩ ⇓ ⟨v, ξ′, φ, ρ′⟩

Note: A convincing explanation of why two rules are different is should include not only an explanation in English but also a code example on which the two rules behave differently.

Do all parts of exercise 16 on page 82 of Build, Prove, and Compare. This is an exercise in language design. The exercise will give you a feel for the kinds of choices a language designer might have made in a language you have never seen before. It will also give you a tool you can use to think about the consequences of language-design choices even without an implementation.

To complete the exercise, you must analyze three variations on a design: the Impcore standard and two alternatives, which resemble the languages Awk and Icon. For the Impcore standard, you can confirm the results of your analysis using the Impcore implementation. But for the Awk-like and Icon-like variations, you don’t have an implementation that you can use to verify the results of your analysis. To get the problem right, you have two choices: think carefully about the semantics you have designed and the program you have written—or build two more interpreters, so that you can actually test your code. (Each new interpreter requires only a two-line change to file eval.c, so if you wanted to build new interpreters, you wouldn’t be deep in the weeds.)

Part (d) involves coding from scratch, and it could involve new functions. But these functions are not trying to do anything useful with data; instead, they are trying to tease out differences in language semantics. Moreover, unless you choose to build interpreters, you cannot run unit tests of the Awk-like and Icon-like semantics. For these reasons, the only steps we expect from our recommended design process are a name and a contract for each function you choose to write (steps 3 and 4).

We will assess your code by running it in three interpreters. This assessment leaves you vulnerable to these common mistakes:

• You might define a function and forget to call it. If you forget to call your function, then when we run your code, the last thing the interpreter does will probably not be to print 0 or 1, which is what is called for in the exercise.

• You might forget that after evaluating an expression, the interpreter prints the result of the expression.

• You might use print or printu where you really meant println.

• You might include unit tests in your code. In that case, the last thing the interpreter prints will be the results of running the unit tests.

Do exercise 12 on page 79 of Build, Prove, and Compare. The purpose of the exercise is to develop your understanding of derivations, so be sure to make your derivation complete and formal. You can write out a derivation like the ones in the book, as a single proof tree with a horizontal line over each node. If you prefer, you can write a sequence of judgments, number each judgment, and write a proof tree containing only the numbers of the judgments, which you will find easier to fit on the page.

In this exercise, or in writing any derivation, the most common mistake made is to copy judgments blindly from the rules of the semantics. This kind of copying results in superfluous primes. In the rules, the primes in ξ′ and ρ′ are a way of saying “I don’t know.” In particular, what’s unknown is the exact nature of the subexpressions, and therefore the results of evaluating them. (Notice that the syntactic forms VAR and LITERAL don’t have any subexpressions, and their rules don’t have any primes.) In the expression (begin (set x 3) x), all of the subexpressions are known, and a correct derivation doesn’t have any primes.

Do part (a) of exercise 13 on page 79 of Build, Prove, and Compare. Now that you know how to write a derivation, in this exercise you start reasoning about derivations. This problem calls for a math-class proof about formal semantics, so any formal derivations you write need to be supplemented by a few words explaining what the formal derivation is and what role it plays in the proof.

As in the previous exercise, be wary of primes. The ξ′, ρ′, ξ″ and ρ″ in the problem are not necessarily different from the initial environments or from each other. The primes say only that they might be different.

Exercise F: Metatheory. This final exercise requires you to raise your game again by reasoning about the set of all valid derivations. It’s metatheory. Metatheoretic proofs are probably unfamiliar, but you will have a crack at them in lecture and in recitation.

Metatheory is a fantastic tool, because it gives you results that can apply to any program written in a language. But it’s hard to get started: there are useful metatheoretic results, and there are easy metatheoretic results, but I don’t know any useful, easy metatheoretic results. Here are a couple of results that are useful but not easy:

• Impcore is deterministic: the same program gives the same answer every time (not true of Java!).

• Impcore can be evaluated using a call stack (like C and Java).

To make it possible to do something relatively interesting but also relatively easy, I’ll ask you to investigate a metatheoretic conjecture that’s not true:¹

Conjecture: If global variable y is defined, and if y does not appear in expression e, and if expression e evaluates to some value, then the evaluation of e does not change the value of y.

To disprove a metatheoretic conjecture, it is sufficient to find a counterexample, but to show insight into how metatheory works, you will also explain what parts of the proof fail and how. To structure your explanations, you’ll rely on a stylized structure that applies to every metatheoretic proof: as described in the book in section 1.7.3, a proof needs a case for each rule in the semantics.

Using the detailed definitions below, complete the following four tasks, each of which relates to the conjecture.

1. Exhibit a counterexample.

2. Since the conjecture relates to a change in the value of a variable, the cases for assignment (set) are likely to be relevant. Both those cases actually work; show that they go through.

   Note that the two cases are actually different; both need to be handled in full.

   (To prove these cases, which are inductive, you will be proving an implication. Please identify the induction hypothesis, which is the left-hand side of that implication. You may wish to review the handout “Overview of Induction” by Chris Phifer.)

3. Find one case of the metatheoretic proof that fails, and explain why the proof doesn’t go through for that case.

4. Briefly explain, in language a COMP 11 student would understand, why the conjecture fails. (A sentence or two is plenty.)

To reduce bureaucracy, you will show that the conjecture fails in Simplified Impcore. Simplified Impcore is a restricted subset of Impcore in which:

• There are no while or begin expressions.
• Every function application has exactly two arguments.
• The only primitive function is +.

Using Simplified Impcore reduces the number of cases to something manageable.

Here’s the conjecture in detail: whenever ⟨e, ξ, ϕ, ρ⟩ ⇓ ⟨v, ξ′, ϕ, ρ′⟩ and y is a variable that is in dom ξ but does not appear (“free”) in e, then ξ′(y) = ξ(y). We will not formalize “appearing free” just yet, but the appearance of a free variable is defined inductively over the abstract syntax. Here is the definition for Impcore:

• x appears free in VAR(x).
• x appears free in SET(x, e).²
• If x appears free in any of e’s subexpressions, then it also appears free in e. For example, if x appears free in e₁, then it also appears free in IF(e₁, e₂, e₃).

This concept is so central to the proof that it benefits from notation: for the set of variables that appear free in e, we write fv(e). We can then make things more formal:

• fv(VAR(x)) = {x}.
• fv(SET(x, e)) = {x} ∪ fv(e).
• If e has subexpressions, its set of free variables is the union of the free variables of the subexpressions. For example, fv(IF(e₁, e₂, e₃)) = fv(e₁) ∪ fv(e₂) ∪ fv(e₃). As another example, fv(APPLY(f, e₁, …, e_n)) = fv(e₁) ∪ ⋯fv(e_n).

And we can also formalize the conjecture:

• Whenever ⟨e, ξ, ϕ, ρ⟩ ⇓ ⟨v, ξ′, ϕ, ρ′⟩ and y ∈ dom ξ and y ∉ fv(e), then ξ′(y) = ξ(y).

This is the form of the conjecture that will be most useful for your solutions.

Notes:

• To “find a counterexample” means to exhibit a choice of e, v, and five environments for which the evaluation judgment holds—but in which evaluating e changes the value of a defined global variable, even though the variable does not appear free in e. Environments ξ and ρ must be written out. For your environment ϕ, you may state simply “the ϕ from the initial basis,” or if you wish, you may say “ϕ includes the initial basis plus the user-defined functions added by the following definitions,” and give the definitions.

• If e calls a function f, then f’s variables (its formal parameters and any global variables it mentions), are not considered free in e. Only variables mentioned in the actual parameters appear free in e.