* Unit 10 --- Small-Step Operational Semantics
:PROPERTIES:
:CUSTOM_ID: unit-10-small-step-operational-semantics
:END:
*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]]

** Goals
:PROPERTIES:
:CUSTOM_ID: goals
:END:
- Define single-step reduction =→= for call-by-value λ-calculus
- Define reflexive-transitive closure =→*=
- Prove determinism: =t → t₁ ∧ t → t₂ ⇒ t₁ = t₂=

** Sources
:PROPERTIES:
:CUSTOM_ID: sources
:END:
- syndikos/lean4-stlc =Reduction.lean=, =Semantics.lean=
- Software Foundations Vol.2 "Smallstep"
- PLFA Part 2

** Exercises
:PROPERTIES:
:CUSTOM_ID: exercises
:END:
#+begin_src lean
open DBTerm

-- 10.1 — Single-step cbv reduction
-- Call-by-value: reduce the *argument* before substituting into the function body.
-- A value is a λ-abstraction (in pure STLC).
inductive Value : DBTerm → Prop where
  | lam : Value (lam b)

inductive Step : DBTerm → DBTerm → Prop where
  -- β-reduction: (λ. t) v → subst t 0 v   (where v is a value)
  | beta (t v : DBTerm) (hv : Value v) :
      Step (app (lam t) v) (subst t 0 v)
  -- Congruence: if f → f', then f a → f' a
  | appL (f f' a : DBTerm) (hstep : Step f f') :
      Step (app f a) (app f' a)
  -- Congruence: if v is a value and a → a', then v a → v a'
  | appR (v a a' : DBTerm) (hv : Value v) (hstep : Step a a') :
      Step (app v a) (app v a')

-- 10.2 — Multi-step (reflexive-transitive closure)
inductive StepStar : DBTerm → DBTerm → Prop where
  | refl (t : DBTerm) : StepStar t t
  | step (t₁ t₂ t₃ : DBTerm) (hstep : Step t₁ t₂) (hstar : StepStar t₂ t₃) :
      StepStar t₁ t₃

-- 10.3 — Determinism
theorem step_deterministic {t t₁ t₂ : DBTerm} (h₁ : Step t t₁) (h₂ : Step t t₂) : t₁ = t₂ :=
  by
    sorry

-- Hint: induction on h₁, then cases on h₂. The tricky case:
-- when one side is (lam t) and the other is a congruence rule that also
-- produces (lam t) — they match.

-- 10.4 — Stuck terms
-- A term is "stuck" if it's not a value and can't take a step.
-- Type soundness = "well-typed terms never get stuck".
def Stuck (t : DBTerm) : Prop :=
  ¬ Value t ∧ ¬ ∃ t', Step t t'

-- Find a stuck term in the untyped calculus
def stuckExample : DBTerm :=
  app (var 0) (var 1)  -- a free variable applied to another free variable

-- Show it's stuck (you'll prove something similar in Unit 12 with types)
#+end_src