Translating operational semantics into English. 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 beginning programmer (e.g., a CS 11 student) would understand. (In other words, it is OK to talk about “variables,” but it is not OK to talk about “environments.”)

Translating English into operational semantics. 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 risks inadvertently changing the language definition, and it adds an additional obligation (a new 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. Meanings of rules. 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.

Specifying new language features with new rules. 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.

Hint: For part (d), retrieval question I (page 75) is especially relevant.

Proof by derivation. 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.

If it helps to make your derivation fit on the page, you are welcome to use abbreviations like Lit for Literal, ForVar for FormalVar, GloVar for GlobalVar, and so on.

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.

Proof using derivations. 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. That counterexample will include an expression e whose evaluation changes the value of some variable y, even though y won’t appear in e.

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 beginning programmer 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.

How to get started and what a solution should look like

If you’re lucky, you’ll have a flash of insight that will tell you exactly what is wrong with the conjecture—and you’ll have your counterexample. But that is neither likely nor necessary to solve the problem. This problem should be solved by applying the method “How to attempt a metatheoretic proof” in the book in section 1.7.3, which starts on page 62. So, to get started, attempt a case of a proof for each rule in Simplified Impcore.

• Begin with the cases for rules FormalAssign and GlobalAssign, which you have to do anyway for part b. Each case should follow the template in section 1.7.3, with its six numbered steps.

• Keep going with other cases, one for each rule of Simplified Impcore, until you find a case for which the proof fails. You can use insight here, or you can just plod through until you find a case that fails.

• Once you’ve found a case for which the proof fails, explain why. That’s part c. If you’re not certain why it fails, find the counterexample, then go back to part c.

• Still working with the case for which the proof fails, you want to exhibit a counterexample. The counterexample refutes the conjecture. (That is, it demonstrates conclusively that the conjecture is no good.)

  To exhibit a counterexample you must 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. The syntactic form of e is going to be an instance of the form in the conclusion of the rule that fails. For example, if the IfTrue case were to fail, then e would be an If expression. (Hint: it doesn’t and it’s not.)

  Once you find an expression e that refutes the conjecture, you need to say the environments in which e is to be evaluated. Environments ξ and ρ can be tiny, so they must be written out in full. But writing out ϕ in full would be tiresome, so instead, you may say “ϕ contains all the functions in the initial basis, plus the following additional function definitions,” and then show the code for the definitions. (If you solve the problem without any additional definitions, that is OK.)

  The counterexample is part a.

• The last part of the problem, part d, is to show that you understand what is going on. Write out your explanation in a sentence or two.

Your solution should be written in two parts:

• The cases for the proof that you attempted. At minimum these must include the two successful set cases from part b, plus the failing case from part c. If you proved other cases successfully, you are welcome to include them.

• Answers to parts a, b, c, and d in an organized sequence.

  • The answer to part a must include the e, ξ, ϕ, ρ, v, ξ′, and ρ′ that refute the conjecture. A few words of explanation are also appropriate.

  • The answer to part b should simply say that the two cases are included.

  • The answer to part c should identify the case (rule) for which the proof fails, and should include a short explanation as to why the proof doesn’t go through.

  • The answer to part d should include a sentence or two suitable for a beginning programmer (e.g., CS 11 student).

Note: Free variables, formal parameters, and actual parameters

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. If you are not confident on the distinction between formal and actual parameters, here is an explanation:

(define square (x)
  (* x x))

(square 10)

(while (> n 0)
  (begin
    (println (square n))
    (set n (- n 1))))