| name | sequent-calculus |
| description | Surface → IR translation rules and IR reduction semantics for Ziku's λμμ̃-calculus based intermediate representation. Use when implementing translation, IR evaluation, or understanding the core semantics. |
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
