菜单
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.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
| 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. |
Translation rules and reduction semantics for Ziku's IR based on the λμμ̃-calculus.
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)
The reduction relation ⊲ defines the evaluation semantics:
⟨μα.s | c̄⟩ ⊲ s[c̄/α] (μ-reduction)
⟨v̄ | μ̃x.s⟩ ⊲ s[v̄/x] (μ̃-reduction, v is value)
| 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 |
⟨p | c⟩: Connects a producer p with a consumer c