Assignment: Operational Semantics

; (sqrt n) approximates the square root of natural number n.
; It returns the largest integer whose square is no greater than n.

(define sqrt (n)
   [locals i]
   (begin
     (while (<= (* i i) n)
        (set i (+ i 1)))
     (- i 1)))

Do exercise 13 on page 82 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 exercise 14 on page 82 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.

Do exercises 21 and 22 on page 83 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 these exercises, 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 crazy.)

Exercise 22 does involve coding from scratch, and it could involve new functions. However, 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).

In exercise 22, we will assess your results by running your code 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 20 on page 83 of Build, Prove, and Compare. In this exercise you prove that given a set of environments, the result of evaluating any expression e is completely determined. That is, in any given starting state, evaluation produces the same results every time. This proof requires you to raise your game again, 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.

These proofs are stylized. To tackle the problem, assume you have two valid derivations with the same e and the same environments on the left, but different v’s on the right—let’s call them v₁ and v₂. You then prove that if both derivations are valid, v₁ = v₂. In other words, no matter what e is, you show that whenever ⟨e, ξ, ϕ, ρ⟩ ⇓ ⟨v₁, ξ′, ϕ, ρ′⟩ and ⟨e, ξ, ϕ, ρ⟩ ⇓ ⟨v₂, ξ″, ϕ, ρ″⟩, it is also true that v₁ = v₂.

The structure of your proof will resemble the structure given in section 1.6.3, which starts on page 61, but because your proof involves reasoning about two derivations, it will be a little more complex. Your proof will proceed by induction on just one of the two derivations. You pick which one.

Note well that the theorem you are setting out to prove applies only to valid derivations that begin with the same initial state, including environments. But the conclusion of the theorem tells you only that the values are the same—it says nothing about the environments. If you set out naively, you’ll find yourself in trouble on some of the induction steps. I know of two ways forward:

• Write a separate proof about the environments (not recommended).

• Find a stronger theorem that can also serve as an induction hypothesis, prove it, and then show that “Impcore is deterministic” follows as a corollary (recommended).

Whichever you choose, be explicit about your induction hypothesis.

To reduce bureaucracy, you will do this proof in Theoretical Impcore. Theoretical 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 Theoretical Impcore reduces the number of cases to a manageable number. This step will relieve some of the tedium (which, in this sort of proof, is regrettably common).

Organizing the answers to Part C

For these exercises you will turn in two files: theory.pdf and awk-icon.imp. For file theory.pdf, you could consider using LaTeX, but unless you already have experience using LaTeX to typeset mathematics, it’s a bad idea. We recommend that you write your theory homework by hand, then scan or photograph it.

If you do already know LaTeX and you wish to use it, you may benefit by emulating our LaTeX source code for a simple proof system or Sam Guyer’s LaTex source code for typesetting operational semantics. You might also like Matthew Ahrens’s video tutorial on typesetting proof trees.

To help us read your answers to Part C, we need for you to organize them carefully:

• The answer to each question must start on a new page.

• The theory answers must appear in this order: exercises 13, 14, 21, and finally 20.

• Your answer to exercise 22 must be in file awk-icon.imp.

Extra credit: Eliminating begin

Theoretical Impcore has neither while nor begin. You already have an idea that you can often replace while with recursion. For extra credit, show that you can replace begin with function calls.

Assume that ϕ binds the function second according to the following definition:

(define second (x y) y)

I claim that if e₁ and e₂ are arbitrary expressions, you can always write (second e₁ e₂) instead of (begin e₁ e₂). For extra credit, answer any or all of the following questions:

• X1. Using evaluation judgments, take the claim “you can always write (second e₁ e₂) instead of (begin e₁ e₂)” and restate the claim in precise, formal language.

  Hint: The claim is related to the claims in exercises 14 and 15 on page 82 in the Impcore chapter.

• X2. Using operational semantics, prove the claim.

• X3. Define a translation for (begin e₁⋯e_n) such that the translated code behaves exactly the same as the original code, but in the result of the translation, every remaining begin has exactly two subexpressions. For example, you might translate

  (begin e1 e2 e3)

  into

  (begin e1 (begin e2 e3))

  You may use any notation you like, but the cleanest way to define the translation is by using algebraic laws.

Once you’ve defined the translation in step X3, you’ll be ready to write a translation that eliminates begin entirely. But that translation is more appropriate to next week’s homework.

How to organize and submit your work

Before submitting code, test what you can. We do not provide any tests; you write your own. All code can be fully tested except the code for exercise 22.

• To complete part A, which you do by yourself, download the questions, then edit the answers into the file cqs.opsem.txt. If your editor is not good with Greek letters, you can spell out their names: ξ is “xi,” ϕ is “phi,” and ρ is “rho.”

  You won’t submit part A until you also have the files for part C.

• To submit part B, which you may have done with a partner, cd into bare/impcore-with-locals. The directory should contain your code and a README file that documents your solution.

  As soon as you have these files, run submit105-opsem-pair to submit a preliminary version of your work. Keep submitting until your work is complete; we grade only the last submission. Only one partner should submit.

• To complete part C, which you do by yourself, create files awk-icon.imp and theory.pdf. Please leave your name out of your PDF—that will enable your work to be graded anonymously.

  Please also create a file called README, in which you tell us anything else you think is useful for us to know. We provide a template for your README at http://www.cs.tufts.edu/comp/105/homework/opsem-README-template.

  As soon as you have the files for parts A and C, cd into the appropriate directory and run submit105-opsem-solo to submit a preliminary version of your work. You’ll need files README, cqs.opsem.txt, awk-icon.imp, and theory.pdf, but preliminary versions are good enough. Keep submitting and resubmitting until your work is complete; we grade only the last submission.

When you submit theory.pdf, the provide program should email you a copy of the PDF. Check the email and be sure that the PDF opens and displays what you expect. If there is a problem with the PDF, resubmit the file or ask for help on Piazza.

How your work will be evaluated

Adding local variables to Impcore (exercise 33)

Everything in the general coding rubric applies, but we will focus on three areas specific to this exercise:

Operational semantics

Below is an extensive list of criteria for judging semantics, rules, derivations, and metatheoretic proofs. As always, you are aiming for the left-hand column, you might be willing to settle for the middle column, and you want to avoid the right-hand column.

Changed rules of Impcore (exercise 21)

Program to probe Impcore/Awk/Icon semantics (exercise 22)

Derivations (exercises 13 and 14)

Metatheory (exercise 20)