Operational Semantics

Operational Semantics Definition

• Approach to semantics

• Inductive binary relation between terms

• Specifies program behaviour through evaluation rules

• Includes big step and small step

Big Step Semantics

• Binary relation between terms and values

• Represents evaluation as E ⇓ V

• Meaning is based on possible evaluated values

Big Step Advantages

• Straightforward modeling of runtime environment
• Defines relations between runtime states and values
• Describes operators by their actions, not meanings

Big Step Disadvantage

• Does not account for non-terminating programs
• Only relates terminating programs to final values

Big Step Toy - Constants

• n ⇓ n (literal evaluates to itself)
• true ⇓ true
• false ⇓ false

Big Step Toy - Less Than

• E1 ⇓ n, E2 ⇓ m:
  • n < m implies E1 < E2 ⇓ true
  • n ≮ m implies E1 < E2 ⇓ false

Big Step Toy - Addition

• E1 ⇓ n, E2 ⇓ m:
  • n + m = n₀ implies E1 + E2 ⇓ n₀

Big Step Toy - Conditional

• E1 ⇓ true, E2 ⇓ V:
  • if E1 then E2 else E3 ⇓ V
• E1 ⇓ false, E3 ⇓ V:
  • if E1 then E2 else E3 ⇓ V

Big Step Toy - Let

• E1 ⇓ V, E2[V/x] ⇓ V':
  • let (x:T) = E1 in E2 ⇓ V'
• Substitution replaces variable with value

Big Step Toy - Application

• E1 ⇓ (x:T)E₁', E2 ⇓ V₂:
  • E₁'[V₂/x] ⇓ V' implies E1 E2 ⇓ V'
• Represents function application

Big Step Derivation Tree

• Proof tree for big step evaluation
• Justifies conclusions using evaluation rules
• Leaves are axioms for constants and values

Small Step Semantics

• Inductive relation between program states
• Represents runtime configurations as E → E'
• Changes program counter through term modifications

Small Step Advantages

• Models step-by-step execution
• Shows program behavior during evaluation
• Handles non-termination with infinite sequences

Small Step Toy - Less Than Reduction

• n < m → true
• n ≮ m → false
• E → E' implies n < E → n < E'

Small Step Toy - Addition Reduction

• n + m → n₀ where n + m = n₀
• E → E' implies n + E → n + E'

Small Step Toy - Conditional Reduction

• if true then E₂ else E₃ → E₂
• if false then E₂ else E₃ → E₃
• E₁ → E₀ implies if E₁ then E₂ else E₃ → if E₀ then E₂ else E₃

Small Step Toy - Let Reduction

• let (x:T) = V in E₂ → E₂[V/x]
• E₁ → E₀ implies let (x:T) = E₁ in E₂ → let (x:T) = E₀ in E₂

Small Step Toy - Application Reduction

• (x:T)E₁ V → E₁[V/x]
• E₂ → E₀ implies (x:T)E₁ E₂ → (x:T)E₁ E₀
• E₁ → E₀ implies E₁ E₂ → E₀ E₂

Small Step Derivation Trees

• Validating each single step through proof trees
• Leaves are axioms for primitive reductions
• Context rules propagate steps

Small Step Sequence

• Chain of reductions: E₁ → E₂ → E₃ → … → Eₙ
• Represents the complete evaluation path from initial to final value

Relating Big Step and Small Step

• E →\* E' as reflexive transitive closure of →
• Theorem: E ⇓ V iff E →\* V
• Proof by induction over derivation trees