The purpose of this assignment is to help you develop rudimentary skills with operational semantics, inference rules, and syntactic proof technique. You will use these skills heavily throughout the first two-thirds of the course, and you will use them again later if you ever want to keep up with the latest new ideas in programming languages or if you want to go on to advanced study.

Some of the essential skills are

Few of these skills can be mastered in a single assignment. When you’ve completed the assignment, I hope you will feel confident of your knowledge of exactly the way judgment forms, inference rules, and derivations are written. On the other skills, you’ll have made a start.

Part A: Reading Comprehension (individual work, 10 percent)

For questions 1–5, please read pages 18–26 (the book sections on environments and on operational semantics of expressions).

  1. ξ is an environment that maps names to:

  2. ϕ is an environment that maps names to:

  3. ρ is an environment that maps names to:

    Choices for questions 1–3:

    1. only user-defined functions.
    2. only the values of formal parameters.
    3. both primitive and user-defined functions.
    4. the values of both global variables and formal parameters.
    5. only primitive functions.
    6. only the values of global variables.
  4. In operational semantics, what kind of a thing does e stand for?

  5. In operational semantics, what kind of a thing does v stand for?

    Choices for questions 4 and 5:

    1. a variable
    2. an elaboration
    3. an expression
    4. a value
    5. a function

For questions 6 and 7, please read Section 1.1.5 (page 14) on the difference between primitive functions and predefined functions, and please study the rules for function application in Section 1.4.6, which starts on page 25.

  1. Function <= is in the initial basis but is not a primitive function (it is a predefined function). When evaluating (<= 0 n), what rule of the operational semantics is used at the root of the derivation?

  2. Function < is primitive. When evaluating (< n 10), what rule of the operational semantics is used at the root of the derivation?

    Choices for questions 6 and 7:

    1. ApplyLessThanEqTrue
    2. ApplyLessThanEqFalse
    3. ApplyUser
    4. ApplyLessThanTrue
    5. ApplyLessThanFalse
    6. ApplyPrim

Part B: Adding Local Variables to the Interpreter (Work with a partner, 23 percent)

Related reading: Section 1.5, particularly Section 1.5.2, which starts on page 44. These pages will walk you through how the impcore interpreter is implemented.

This exercise will help you understand how operational semantics is implemented, and how language changes can be realized in C code. You will do Exercise 33 from page 87 of Ramsey’s book. We recommend that you solve this problem with a partner, but this solution must be kept separate from your other solutions. Your programming partner, if any, must not see your other work.

For information on pair programming, consult the syllabus, the reading, and some timeless advice for pair programmers.

Part C: Operational semantics, derivations, and metatheory (Individual work, 67 percent)

Related reading:

These exercises are intended to help you become fluent with operational semantics. Do not share your solutions with any programming partners. We encourage you to discuss ideas, but nobody else may see your rules, your derivations, or your code. If you have difficulty, find a TA, who can help you work a couple of similar problems.

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. Either way, make sure that your PDF can be opened on a Halligan computer.

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 should 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 e1 and e2 are arbitrary expressions, you can always write (second e1 e2) instead of (begin e1 e2). For extra credit, answer any or all of the following questions:

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.

How your work will be evaluated

Adding local variables to Impcore

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

Exemplary Satisfactory Must improve
Locals

• Change to interpreter appears motivated either by changing the semantics as little as possible or by changing the code as little as possible.

• Local variables for Impcore pass simple tests.

• Course staff believe they can see motivation for changes to interpreter, but more changes were made than necessary.

• Local variables for Impcore pass some tests.

• Course staff cannot understand what ideas were used to change the interpreter.

• Local variables for Impcore pass few or no tests.

Naming

• Where the code implements math, the names of each variable in the code is either the same as what’s in the math (e.g., rho for ρ), or is an English equivalent for what the code stands for (e.g., parameters or parms for ρ).

• Where the code implements math, the names don’t help the course staff figure out how the code corresponds to the math.

• Where the code implements math, the course staff cannot figure out how the code corresponds to the math.

Structure

• The code is so clear that course staff can instantly tell whether it is correct or incorrect.

• There’s only as much code as is needed to do the job.

• The code contains no redundant case analysis.

• Course staff have to work to tell whether the code is correct or incorrect.

• There’s somewhat more code than is needed to do the job.

• The code contains a little redundant case analysis.

• From reading the code, course staff cannot tell whether it is correct or incorrect.

• From reading the code, course staff cannot easily tell what it is doing.

• There’s about twice as much code as is needed to do the job.

• A significant fraction of the case analyses in the code, maybe a third, are redundant.

Operational semantics

Here 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)

Exemplary Satisfactory Must improve
Rules

• Every inference rule has a single conclusion which is a judgment form of the operational semantics.

• In every inference rule, every premise is either a judgment form of the operational semantics or a simple mathematical predicate such as equality or set membership.

• In every inference rule, if two states, two environments, or two of any other thing must be the same, then they are notated using a single metavariable that appears in multiple places. (Example: ρ or σ)

• In every inference rule, if two states, two environments, or two of any other thing may be different, then they are notated using different metavariables. (Example: ρ and ρ)

• New language designs use or change just enough rules to do the job.

• Inference rules use one judgment form per syntactic category.

• In every inference rule, two states, two environments, or two of any other thing must be the same, yet they are notated using different metavariables. However, the inference rule includes a premise that these metavariables are equal. (Example: ρ1 = ρ2)

• A new language design has a few too many new or changes a few too many existing rules.

• Or, a new language design is missing a few rules that are needed, or it doesn’t change a few existing rules that need to be changed.

• Notation that is presented as an inference rule has more than one judgment form or other predicate below the line.

• Inference rules contain notation above the line that does not resemble a judgment form and is not a simple mathematical predicate.

• Inference rules contain notation, either above or below the line, that resembles a judgment form but is not actually a judgment form.

• In every inference rule, two states, two environments, or two of any other thing must be the same, yet they are notated using different metavariables, and nothing in the rule forces these metavariables to be equal. (Example: ρ and ρ are both used, yet they must be identical.)

• In some inference rule, two states, two environments, or two other things may be different, but they are notated using a single metavariable. (Example: using ρ everywhere, but in some places, ρ is needed.)

• In a new language design, the number of new or changed rules is a lot different from what is needed.

• Inference rules contain a mix of judgment forms even when describing the semantics of a single syntactic category.

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

Exemplary Satisfactory Must improve
Semantics

• The program which is supposed to behave differently in Awk, Icon, and Impcore semantics behaves exactly as specified with each semantics.

• The program which is supposed to behave differently in Awk, Icon, and Impcore semantics behaves almost exactly as specified with each semantics.

• The program which is supposed to behave differently in Awk, Icon, and Impcore semantics gets one or more semantics wrong.

• The program which is supposed to behave differently in Awk, Icon, and Impcore semantics looks like it is probably correct, but it does not meet the specification: either running the code does not print, or it prints two or more times.

Derivations (exercises 13 and 14)

Exemplary Satisfactory Must improve
Derivations

• In every derivation, every utterance is either a judgment form of the operational semantics or a simple mathematical predicate such as equality or set membership.

• In every derivation, every judgement follows from instantiating a rule from the operational semantics. (Instantiating means substituting for meta variables.) The judgement appears below a horizontal line, and above that line is one derivation of each premise.

• In every derivation, equal environments are notated equally. In a derivation, ρ and ρ must refer to different environments.

• Every derivation takes the form of a tree. The root of the tree, which is written at the bottom, is the judgment that is derived (proved).

• In every derivation, new bindings are added to an environment exactly as and when required by the semantics.

• In one or more derivations, there are a few horizontal lines that appear to be instances of inference rules, but the instantiations are not valid. (Example: rule requires two environments to be the same, but in the derivation they are different.)

• In a derivation, the semantics requires new bindings to be added to some environments, and the derivation contains environments extended with the right new bindings, but not in exactly the right places.

• In one or more derivations, there are horizontal lines that the course staff is unable to relate to any inference rule.

• In one or more derivations, there are many horizontal lines that appear to be instances of inference rules, but the instantiations are not valid.

• A derivation is called for, but course staff cannot identify the tree structure of the judgments forming the derivation.

• In a derivation, the semantics requires new bindings to be added to some environments, and the derivation does not contain any environments extended with new bindings, but the new bindings in the derivation are not the bindings required by the semantics. (Example: the semantics calls for a binding of answer to 42, but instead answer is bound to 0.)

• In a derivation, the semantics requires new bindings to be added to some environments, but the derivation does not contain any environments extended with new bindings.

Metatheory (exercise 20)

Exemplary Satisfactory Must improve
Metatheory

• Metatheoretic proofs operate by structural induction on derivations, and derivations are named.

• Metatheoretic proofs classify derivations by case analysis over the final rule in each derivation. The case analysis includes every possible derivation, and cases with similar proofs are grouped together.

• Metatheoretic proofs operate by structural induction on derivations, but derivations and subderivations are not named, so course staff may not be certain of what’s being claimed.

• Metatheoretic proofs classify derivations by case analysis over the final rule in each derivation. The case analysis includes every possible derivation, but the grouping of the cases does not bring together cases with similar proofs.

• Metatheoretic proofs don’t use structural induction on derivations (serious fault).

• Metatheoretic proofs have incomplete case analyses of derivations.

• Metatheoretic proofs are missing many cases (serious fault).

• Course staff cannot figure out how metatheoretic proof is broken down by cases (serious fault).