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
| Concept |
File |
Function/Type |
| Translation ⟦−⟧ |
Ziku/Translate.lean |
translate |
| μ-reduction |
Ziku/IR/Eval.lean |
eval |
| μ̃-reduction |
Ziku/IR/Eval.lean |
eval |
| Producer |
Ziku/IR/Syntax.lean |
Producer |
| Consumer |
Ziku/IR/Syntax.lean |
Consumer |
| Statement |
Ziku/IR/Syntax.lean |
Statement |
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
