2008-08-02 [長年日記]
λ. Categories with attributes (cwa)
依存型とcatamorphism の話を書くために、まずは依存型を持つ体系の圏論的なモデルとして Categories with attributes を導入する。
Categories with attributes
Category with attributes (cwa) は依存型を持つ計算体系の圏論的なモデルとしてよく使われる圏で、以下の構成要素と条件からなる。
- 圏 C
- 終対象 1∈|C|
- 前層 Fam : Cop → Set
- 射に対する作用については S[f] := Fam(f)(S) という記法を用いる。
- 任意の Γ∈|C| と S∈Fam(Γ) に対して、Γ・S ∈ |C| という対象と射 πS : Γ・S → Γ が存在する
- 記法を濫用して πS のことを、単に S と書くことがある。
- 任意の射 f : Δ → Γ と S∈Fam(Δ) に対して、射 f・S : Δ・S[f] → Γ・S が存在して、
![\xymatrix@+15pt{ \Delta\cdot S[f] \ar[r]^{f\cdot S} \ar[d]_{\pi_{S[f]}} & \Gamma\cdot S \ar[d]^{\pi_S} \\ \Delta \ar[r]_{f} & \Gamma }](tex/9872fd683cdeca608cfd2a568231f10c.png "\xymatrix@+15pt{ \Delta\cdot S[f] \ar[r]^{f\cdot S} \ar[d]_{\pi_{S[f]}} & \Gamma\cdot S \ar[d]^{\pi_S} \\ \Delta \ar[r]_{f} & \Gamma }")
がpullbackになっていて、さらに idΓ・S = idΓ・S と (f∘g)・S = (f・S)∘(g・S[f]) が成り立つ
依存型を持つ体系のcwaでの大雑把な解釈
まず、πS の section からなる集合を Tm(Γ, S) := {M: Γ→Γ・S | πS∘M = idΓ} と書くことにする。 そうすると、依存型を持つ体系はcwaに大雑把にはこんな感じで対応する。
- 文脈 Γ は Γ∈|C| に対応し
- 文脈 Γ での型 S 、すなわち Γ ├ S set であるような S は、S∈Fam(Γ) に対応
- 文脈 Γ での項 M 、すなわち Γ ├ M : S であるような M は、M∈Tm(Γ, S) に対応
これは一見すると奇妙な解釈に見えるけど、スライス C/Γ を考えると、普通の解釈を一般化したものになっている。
C/Γでの終対象は C の idΓ: Γ→Γ なので、C での πS : Γ・S → Γ を C/Γ では単にSと書くことにすると、M∈Tm(Γ, S) は C/Γ ではちゃんと点 1→S とみなすことが出来る。
![\xymatrix{ \Gamma \ar@{=}[dr] \ar[rr]^{M} & & \Gamma\cdot S \ar[dl]^{\pi_S} \\ & \Gamma }](tex/9290b2e4239bb1d1a496f2e193a437df.png "\xymatrix{ \Gamma \ar@{=}[dr] \ar[rr]^{M} & & \Gamma\cdot S \ar[dl]^{\pi_S} \\ & \Gamma }")
代入
それから、M∈Tm(Γ, S) と f : Δ→Γ に対して、M[f] ∈ Tm(Δ, S[f]) を、pullback の性質から以下の図のように定義する。
![\xymatrix@+15pt{ \Delta \ar@{=}@/_1pc/[ddr] \ar@/^1pc/[rrd]^{M\circ f} \ar@{.>}[dr]|{M[f]} \\ & \Delta\cdot S[f] \ar[r]_{f\cdot S} \ar[d]^{\pi_{S[f]}} & \Gamma\cdot S \ar[d]^{\pi_S} \\ & \Delta \ar[r]_{f} & \Gamma }](tex/bc33472fef904aae3e1c932788a73fed.png "\xymatrix@+15pt{ \Delta \ar@{=}@/_1pc/[ddr] \ar@/^1pc/[rrd]^{M\circ f} \ar@{.>}[dr]|{M[f]} \\ & \Delta\cdot S[f] \ar[r]_{f\cdot S} \ar[d]^{\pi_{S[f]}} & \Gamma\cdot S \ar[d]^{\pi_S} \\ & \Delta \ar[r]_{f} & \Gamma }")
S[f] や M[f] と書いたが、これらはもちろん代入(substitution)を表している。
例えば、Γ ├ N : T と Γ, x : T ├ M : S から Γ ├ M[x:=N] : S[x:=N] を得ることが、N ∈ Tm(Γ, T) と M ∈ Tm(Γ・T, S) から M[N] ∈ Tm(Γ, S[N]) を得ることに対応している。
![\xymatrix@+15pt{ \Gamma\cdot S[N] \ar[d]^{\pi_{S[N]}} \ar[r]^{N\cdot S} & \Gamma\cdot T\cdot S \ar[d]^{\pi_S} \\ \Gamma \ar[r]_{N} \ar@<1ex>[u]^{M[N]} & \Gamma\cdot T \ar@<1ex>[u]^{M} }](tex/3b0d4e5438f5326eead985369047b0ea.png "\xymatrix@+15pt{ \Gamma\cdot S[N] \ar[d]^{\pi_{S[N]}} \ar[r]^{N\cdot S} & \Gamma\cdot T\cdot S \ar[d]^{\pi_S} \\ \Gamma \ar[r]_{N} \ar@<1ex>[u]^{M[N]} & \Gamma\cdot T \ar@<1ex>[u]^{M} }")
このように、構文的な代入を意味論的な代入にうまく対応させられるのが、cwaの嬉しいところ。
ただ、ちょっと面倒なのは weakening をする際にも、型や項の側では要らない変数を捨てるような代入を明示的に適用しなくてはいけないところ。
例えば、Γ ├ S set と Γ ├ M : S から weakening で Γ, x : T ├ S set と Γ, x : T ├ M : S を得るのは、S∈Fam(Γ) と M∈Tm(Γ, S) から、πT : Γ・T → Γ を使って S[πT]∈Fam(Γ・T) と M[πT]∈Tm(Γ・T, S[πT]) を得ることに対応する。
![\xymatrix@+15pt{ \Gamma\cdot T\cdot S[\pi_T] \ar[d]^{\pi_{S[\pi_T]}} \ar[r]^{\pi_T\cdot S} & \Gamma\cdot S \ar[d]^{\pi_S} \\ \Gamma\cdot T \ar[r]_{\pi_T} \ar@<1ex>[u]^{M[\pi_T]} & \Gamma \ar@<1ex>[u]^{M} }](tex/134a576fd7c64d1e5c6a58cf99e0eb54.png "\xymatrix@+15pt{ \Gamma\cdot T\cdot S[\pi_T] \ar[d]^{\pi_{S[\pi_T]}} \ar[r]^{\pi_T\cdot S} & \Gamma\cdot S \ar[d]^{\pi_S} \\ \Gamma\cdot T \ar[r]_{\pi_T} \ar@<1ex>[u]^{M[\pi_T]} & \Gamma \ar@<1ex>[u]^{M} }")
これくらいの例なら問題ないのだけど、ちょっと複雑なものを書こうとすると、すぐ訳がわかんなくなってしまうよ……*1
*1 うまい絵算の方法でもあるといいんだけどねぇ
