Questions: Operational Semantics

Question 1

What is the key structural difference between small-step and big-step operational semantics?

• A. Small-step semantics can only handle terminating programs, while big-step handles non-termination
• B. Small-step defines a single transition (one computation step) and iterates it, while big-step relates a program directly to its final value in one judgment
• C. Small-step is more expressive because it supports more language features
• D. Big-step semantics is more formal because it uses inference rules while small-step does not

Answer: (B)

Small-step semantics defines a relation config -> config' that takes one atomic step (e.g., reducing 2+3 to 5 within a larger expression). Full evaluation is the transitive closure ->* of this relation. Big-step semantics defines a relation config => value that directly gives the final result, with the derivation tree capturing the entire computation. Both use inference rules. The practical difference: small-step makes intermediate states observable (important for concurrency, interleaving, and non-termination -- a diverging program takes infinite steps but never produces a big-step derivation). Big-step is often simpler for deterministic, terminating computations and maps naturally to interpreters.

Question 2

In small-step operational semantics, non-terminating programs are modeled as infinite sequences of transitions rather than as a special 'diverge' outcome.

• T. True
• F. False

Answer: True

This is a fundamental advantage of small-step semantics over big-step. A non-terminating program like 'while true do skip' generates an infinite chain of configurations: config_0 -> config_1 -> config_2 -> ... that never reaches a final state. There is no finite derivation tree, which matches the intuition that the program runs forever. In big-step semantics, non-termination is problematic: the evaluation relation simply has no derivation for the diverging program. The program's meaning is 'undefined' in the relation, but this is indistinguishable from a stuck program (one that reaches an error). Small-step semantics cleanly distinguishes divergence (infinite transitions) from getting stuck (no transition available from a non-final configuration).

Question 3

Write the small-step rule for the if-then-else construct: if the condition is 'true', the entire expression steps to the 'then' branch.

Model answer: if true then e1 else e2 -> e1. This is an axiom (no premises needed). The companion rule is: if false then e1 else e2 -> e2. A third congruence rule handles the case where the condition is not yet a value: if e0 -> e0', then (if e0 then e1 else e2) -> (if e0' then e1 else e2). This congruence rule specifies that the condition is evaluated first.

These three rules together completely specify the evaluation of conditionals. The two axioms handle the base cases (condition already reduced to a Boolean value). The congruence rule ensures the condition is fully evaluated before the branch is selected -- it encodes left-to-right evaluation order. This pattern of axiom rules for computed values plus congruence rules for sub-expression evaluation is the hallmark of structural operational semantics (SOS), formalized by Plotkin (1981).

Question 4

Why is operational semantics considered a prerequisite for formal program verification rather than an alternative to it?

Model answer: Hoare logic, weakest preconditions, abstract interpretation, and type systems all reason about program behavior. But what does a program 'do'? Operational semantics provides the mathematical definition: the transition relation IS the program's meaning. Hoare logic's soundness theorem says that if {P} C {Q} is derivable, then for every state satisfying P, the operational execution of C from that state (if it terminates) yields a state satisfying Q. Without operational semantics, soundness is circular -- you would be verifying programs against an informal notion of what they compute. The semantics is the ground truth against which all verification techniques are proven correct.

This foundational role is why operational semantics appears in any rigorous treatment of programming languages and formal methods. The standard proof technique for type soundness, for instance, is 'progress and preservation': progress says well-typed programs can always take a step (using the small-step transition relation), and preservation says each step preserves typedness. Both are stated and proved with respect to the operational semantics.