sequent-calculus
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.
Installation
Details
Usage
After installing, this skill will be available to your AI coding assistant.
Verify installation:
npx agent-skills-cli listSkill Instructions
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
- docs/research/grokking-the-sequent-calculus.md - Full research notes
- Downen & Ariola, "Compiling with Classical Connectives"
More by takoeight0821
View allFind relevant research and guide implementation based on it. Use when implementing features, fixing bugs, or exploring techniques where existing research in docs/research/ may provide guidance. Trigger phrases include "apply research", "use research", "based on the research", "implement from paper", or "find relevant research for [task]".
Search for Lean 4 and Mathlib theorems, lemmas, and definitions by type signature, name, or subexpression pattern. Use when the user asks to find a theorem, look up a Lean definition, search for lemmas, or needs help discovering Mathlib functions.
This skill should be used when the user asks to "refactor", "extract function", "rename", "improve code quality", "reduce duplication", or "remove code smell". Supports Lean 4 and general refactoring patterns.
This skill should be used when the user asks to "create a commit", "commit changes", "write a commit message", "make a commit", needs help with "conventional commits", or wants to understand commit message format and best practices.