Sequent Calculus Reference

Translation rules and reduction semantics for Ziku's IR based on the λμμ̃-calculus.

Translation Rules (Surface → IR)

The translation ⟦−⟧ transforms surface language terms to sequent calculus IR:

⟦x⟧                     =  x
⟦⌜n⌝⟧                   =  ⌜n⌝
⟦t₁ ⊙ t₂⟧               =  μα. ⊙(⟦t₁⟧, ⟦t₂⟧; α)
⟦if t₁ then t₂ else t₃⟧ =  μα.ifz(⟦t₁⟧, ⟨⟦t₂⟧ | α⟩, ⟨⟦t₃⟧ | α⟩)
⟦let x = t₁ in t₂⟧      =  μα.⟨⟦t₁⟧ | μ̃x.⟨⟦t₂⟧ | α⟩⟩
⟦λx.t⟧                  =  cocase {ap(x; α) ⇒ ⟨⟦t⟧ | α⟩}
⟦t₁ t₂⟧                 =  μα.⟨⟦t₁⟧ | ap(⟦t₂⟧; α)⟩
⟦label α {t}⟧           =  μα.⟨⟦t⟧ | α⟩
⟦goto(t; α)⟧            =  μβ.⟨⟦t⟧ | α⟩  (β fresh)

IR Reduction Rules

The reduction relation ⊲ defines the evaluation semantics:

⟨μα.s | c̄⟩    ⊲  s[c̄/α]     (μ-reduction)
⟨v̄ | μ̃x.s⟩    ⊲  s[v̄/x]     (μ̃-reduction, v is value)

Implementation Mapping

Key Concepts

• Producer: Values/terms that produce results (variables, literals, μ-abstractions)
• Consumer: Contexts that consume results (continuations, destructors)
• Cut ⟨p | c⟩: Connects a producer p with a consumer c
• μα.s: Captures current continuation as α
• μ̃x.s: Binds received value as x

Further Reading

• [docs/research/grokking-the-sequent-calculus.md](../../docs/research/grokking-the-sequent-calculus.md) - Full research notes
• Downen & Ariola, "Compiling with Classical Connectives"