This homework covers material from Lecture 10: Introduction to Semantics and Lecture 11: Operational Semantics. You will cross the boundary from syntax to semantics — formalizing what programs mean, tracing evaluation through environments, reading and deriving inference rules, and constructing proof trees.
All questions require written responses. Show your work where applicable, and provide clear justifications for your answers. Several questions require independent research — cite your sources. Partial credit will be awarded based on the quality of your reasoning.
In LN 10, we defined the meaning function $M : \text{AST} \to \text{Semantic Domain}$ and introduced the principle of compositionality — the idea that the meaning of a compound expression is determined entirely by the meanings of its parts.
State the formal definition of compositionality from LN 10. Then demonstrate it concretely on the Petal expression (2 + 3) * 4: show that *. Identify the semantic domain each sub-expression belongs to.
The C preprocessor defines macros via textual substitution. Consider:
#define SQUARE(x) x * x
int result = SQUARE(1 + 2);
After macro expansion, this becomes int result = 1 + 2 * 1 + 2;, which evaluates to 5, not 9.
Explain why this violates compositionality. Specifically: what is the "meaning" of the argument 1 + 2, and why can't the meaning of SQUARE(1 + 2) be determined from it? What external information, beyond the meanings of the sub-expressions, does the macro system depend on?
Explain why compositionality is a desirable property for programming language design. Connect your answer to the pipeline we have built across this course — how does compositionality enable the transition from parser (LN 9) to interpreter (LN 11)?
In LN 10, we saw that natural language descriptions of program behavior break down when hidden semantic choices are involved. For each of the following programs, identify the ambiguity, give two valid interpretations with their resulting values, and name a real programming language that picks each interpretation.
Evaluation Order
x = 1;
y = (x = 2) + x;
What is the value of y? Identify the hidden semantic decision and give both possible results.
Short-Circuit Evaluation
x = 0;
if (x != 0) && (10 / x > 2) {
print 1;
}
Does this program crash? Explain the two possible behaviors depending on whether the language uses short-circuit or eager evaluation of &&. For the short-circuit case, explain which inference rule concept from LN 11 formalizes the idea of "not evaluating an expression" — connect to how the conditional rules in LN 11 leave one branch unevaluated.
Integer Overflow
What does 2147483647 + 1 evaluate to? Using the LN 10 error-handling comparison table, give the result in at least three different languages and identify the semantic choice each language makes.
In LN 10, we formalized the environment as a mapping from variable names to values: $\sigma : \text{Identifier} \to \text{Value}$. The update operation
Formal Environment Tracing
Trace the complete environment evolution for the following Petal program. For each statement, show the environment update using the
x = 3 + 4;
y = x * 2;
x = y - 5;
z = x + y;
print z;
print x;
Your trace should begin with
Environment Update Algebra
Compute each environment step-by-step using the formal update definition above. No Petal syntax — just the mathematical notation.
Reverse-Engineering from Final State
You are given the following observable information about a Petal program that uses only assignments and print statements:
Reconstruct a valid Petal program that produces this exact final state and output. Then verify your answer by tracing the environment forward from
(There are multiple valid programs — you only need to provide one.)
In LN 10, we distinguished lexical scope (variables resolved by where a function is defined) from dynamic scope (variables resolved by where a function is called). Most modern languages use lexical scope, but some use dynamic scope by default.
Consider the following Emacs Lisp program:
(setq x 1)
(defun f ()
(print x))
(defun g ()
(let ((x 2))
(f)))
(g)
Predict what this program prints. Which scoping strategy does Emacs Lisp use? Trace the variable lookup for x inside f: does it follow the definition chain (lexical) or the call chain (dynamic)? Justify your answer using the formal scoping definitions from LN 10.
Now consider this OCaml program:
let x = 1
let f () = print_int x
let g () =
let x = 2 in
f ()
let () = g ()
Predict what this program prints. Which scoping strategy does OCaml use? Explain why the result differs from (or matches) the Emacs Lisp program above, and connect the difference to the formal distinction between definition-site and call-site variable resolution from LN 10.
In LN 11, we formalized operational semantics using inference rules — premises above the line, conclusion below — and introduced the Omega (Ω) technique for reading them: start at the bottom-left (what you have), loop up through the premises (what you must check), and come back down to the bottom-right (what you get).
The Omega Technique
For each of the following inference rules, trace the Ω path and explain what the rule does in plain English. Identify each rule's name and state whether it is an axiom (no premises) or a proper rule (has premises).
Rule 1:
Rule 2:
Rule 3:
Rule 4 (novel — not from LN 11):
Big-Step Evaluation
Evaluate the following Petal program using the big-step inference rules from LN 11. For each statement, write the complete big-step judgment, cite the rule you are applying, and show the resulting environment and output.
a = 4 + 2;
b = a * 3;
print b - a;
Start from
Small-Step Evaluation
Now evaluate the same program from Q5b using the small-step (SOS) transition rules from LN 11. Show each transition
After completing the trace, answer:
In LN 11, we showed that inference rules are mechanically derived from the tree grammar — every production becomes one or more rules. This question tests your ability to derive new rules, reverse-engineer existing ones, and connect rules to code.
Ternary Conditional Expression
Petal currently has an if-else statement. Suppose we want to add a ternary conditional expression: $e_1\; \textbf{?}\; e_2\; \textbf{:}\; e_3$. Unlike the if-else statement from LN 11, this is an expression — it evaluates to a value rather than transforming state.
Follow the 4-step derivation process from LN 11:
Do-While Loop
Suppose we want to add a do-while loop to Petal: $\textbf{do}\; s\; \textbf{while}\; e$. Unlike the while loop from LN 11, the body executes before the condition is checked — the body always runs at least once.
Follow the same 4-step process:
while rules from LN 11 — what structural difference does "body first, then check" create?while rules from LN 11 side-by-side for comparison:while unfolding rule from LN 11 rewrites the loop into a conditional. How does the do-while unfolding differ?Reverse Engineering
The following inference rule describes a construct that was not covered in LN 11. No name or description is provided — only the rule itself.
By reading these rules:
Rules-to-Code Reasoning
In LN 11, we showed that every big-step inference rule maps directly to a clause in a recursive interpreter. Consider the print rule and its corresponding JavaScript code from LN 11:
The Rule:
The Code:
case "Print": {
const value = evaluate(node.expression, env);
console.log(value);
return;
}
Now consider the while rule and its code:
The Rule:
The Code:
case "While":
while (evaluate(node.condition, env) !== 0) {
for (const stmt of node.body) evaluate(stmt, env);
}
return;
while loop correctly implement the two big-step rules (the termination rule and the continuation rule) despite appearing as a single construct?In LN 11, we showed that inference rules compose into proof trees (derivation trees) — tree-shaped proofs that a specific program produces a specific result. Each node is a judgment, each edge is a rule application, and the leaves are axioms.
This is a guided exercise. Each sub-question builds on the previous one. By the end, you will have constructed a complete proof tree for a Petal program with arithmetic, assignment, and control flow.
Consider the following Petal program:
x = 2 + 3;
if x - 4 {
y = x * 2;
} else {
y = 0;
}
print y;
Step 1: The Innermost Expression
Build the proof tree for evaluating the expression 2 + 3 in the initial empty environment
2 and 3 (the leaves)Write the proof tree using the nested fraction notation from LN 11. For example, the proof tree from LN 11 for 3 + 5 looks like:
Step 2: The First Assignment
Now build the proof tree for the complete first statement:
Your expression proof tree from Q7a becomes the premise of the assignment rule. State the resulting environment
Step 3: The Conditional and Full Program
Now tackle the rest of the program:
x - 4 in environment When Proof Trees Get Stuck
Consider the program print x; with the initial empty environment
Attempt to build the proof tree. Which rule do you try to apply? What premise cannot be satisfied? In your own words, define what a stuck configuration is and explain how the absence of an applicable rule models a runtime error.
When Proof Trees Never End
Consider the program while 1 { print 0; }.
Concrete Operational Semantics
In LN 11, we showed that ASTs can be translated into instructions for a stack machine using a post-order traversal, and that the stack reconstructs the tree's nesting at runtime.
Consider the following Petal program:
y = (1 + 2) * 3;
print y;
PUSH, ADD, MUL, STORE, LOAD, PRINT).Interpreters in the Wild
Choose one of the following language implementations to research:
For your chosen implementation, answer the following:
LOAD_FAST, BINARY_ADD, ...").if-else or while) and describe how the implementation handles it in terms that connect to the LN 11 formalism.Cite your sources.
The Meaning Function in the Wild
Choose a programming language not discussed in LN 10 or LN 11 (i.e., not Petal, Python, JavaScript, C, Rust, Haskell, or Java).
Find a specific semantic edge case in that language — a situation where the language must make a choice about evaluation order, error handling for undefined variables, division by zero behavior, integer overflow, or scoping rules.
| Section | Question | Points |
|---|---|---|
| Part 1: Semantic Foundations | Q1: Compositionality | 8 |
| Q2: When Informal Semantics Fails | 7 | |
| Part 2: Environments and Scoping | Q3: Environments and State | 15 |
| Q4: Scoping in Unfamiliar Languages | 5 | |
| Part 3: Operational Semantics | Q5: Reading and Applying Rules | 15 |
| Q6: Deriving and Understanding Rules | 20 | |
| Part 4: Proof Trees | Q7: Proof Trees | 15 |
| Part 5: Semantics in Practice | Q8: Connecting Semantics to Real Languages | 15 |
| Total | 100 |