https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf の P.3 の11個の規則
- IDENTITY
- WEAKENING
- CONTRACTION
- EXCHANGE
- MULTI-COMPOSITION （もとは無名）
- PAIRING
- PROJ-1
- PROJ-2
- ABS
- APP
- UNIT（むしろTERMINALだろうが）
使う文は以下。
確認と取得
- we have σ
- we take σ at location L
- we possess M:Γ → τ named f
- we possess Γ → τ due-to M named f
新規導入
- we get σ
- we assert σ → τ due-to M named f
操作
- we use post-compose g
- we use pre-compose f
- we use make-id
- we use 操作 インデックス〈パラメータ〉
IDENTITY
象形文字 I
from wire-palette we get σ we use make-id we assert σ → σ
WEAKENING
象形文字 !
we possess M:Γ → τ we use pre-compose id[Γ], Delete[σ] we assert Γ, σ → τ
CONTRACTION
象形文字 Δ
we possess M:Γ, σ, σ → τ we use pre-compose id[Γ], Copy[σ] we assert Γ, σ → τ
EXCHANGE
象形文字 X
we possess M:Γ, σ, σ' → τ we use pre-compose id[Γ], Swap[σ, σ'] we assert Γ, σ', σ → τ
MULTI-COMPOSITION
記号 -(-, ..., -)
from node-palette we assert F:τ_1, ‥‥, τ_n → τ' we possess F:τ_1, ‥‥, τ_n → τ' we possess M_1:Γ → τ_1 ‥‥ ‥‥ we possess M_n:Γ → τ_n we use left multi-composition we assert Γ → τ' due-to F(M_1, ..., M_n)
PAIRING
記号 < -, - >
we possess M:Γ → τ we possess N:Γ → σ we use pairing[Γ, τ, σ] we aasert Γ → τ×σ du-to <M, N>
PROJ-1
記号 π^1
we possess M:Γ → τ×σ we use post-compose proj-1[τ, σ] we assert Γ → τ
PROJ-2
記号 π^2
we possess M:Γ → τ×σ we use post-compose proj-2[τ, σ] we assert Γ → σ
ABS
仮想ベンディング象形文字 ∩
we possess M:Γ, σ → τ we use curry[Γ, σ, τ] we assert Γ → [σ, τ]
APP
仮想ベンディング象形文字 ∪
we possess M:Γ → [τ, σ] we possess N:Γ → τ we use left uncurry[Γ, σ, τ] we assert Γ → σ
UNIT
象形文字 !
we have Γ we use make-terminal[Γ] we assert Γ → 1
