Operational Semantics

Origin. Plotkin (1981) SOS. Program meaning via execution rules. Small-step and big-step styles. Foundation for language implementation. Basis for type soundness proofs.

Models. Syntax-directed reduction rules. Configurations: ⟨e, σ⟩ (expression, state). Transitions define evaluation. Structural induction for properties.

Formalism.

Small-step (structural): e → e' (one step reduction) e →* e' (many steps)

Big-step (natural): e ⇓ v (e evaluates to v)

Rules (small-step): E-App1: e₁ → e₁' ────────────── e₁ e₂ → e₁' e₂

E-App2: e₂ → e₂' ────────────── v₁ e₂ → v₁ e₂'

E-Beta: (λx.e) v → e[v/x]

Rules (big-step): E-App: e₁ ⇓ λx.e e₂ ⇓ v₂ e[v₂/x] ⇓ v ───────────────────────────────────── e₁ e₂ ⇓ v

Evaluation contexts: E ::= □ | E e | v E | ... E[e] → E[e'] if e → e'.

Call-by-value: Reduce arguments before substitution. Values don't reduce.

Call-by-name: Substitute unreduced arguments. Lazy evaluation variant.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Step	Small-step
→*	—	Steps	Transitive closure
⇓	U+21D3	Evaluates	Big-step
□	U+25A1	Hole	Evaluation context

Metatheory. Progress: well-typed doesn't get stuck. Preservation: types preserved by steps. Determinism (for deterministic languages). Correspondence: small ↔ big step.

Applies to. Language specification. Type soundness. Mechanized proofs. Compiler verification. Semantics comparison.

Limitations. Large rule sets. Non-determinism adds complexity. Concurrency requires extensions. Full abstraction not guaranteed.