日記 (2020 年 4 月 18 日)
4 月 18 日の続き。
前回は、 アローを Freyd 圏上で解釈し、 アロー則が Freyd 圏の射としても成り立つことを示した。
今回はその逆で、 任意の Freyd 圏の射として等しいなら、 アローの型システムの項として等しくなることを示す。
まず準備として、 型システム Arrow に関する性質を 1 つ証明する。
Arrow には、 与えられた計算を左側の成分にのみ適用する直積の間の計算を作る first がプリミティブな演算として定まっていた。
ここで当然、 与えられた計算を右側の成分に適用する計算を作る演算は定めないのかという疑問が生じるが、 これは実は first を用いて作ることができる。
命題 4.1.
Arrow において、 型多相な閉じた項 second を、
second : [A,B]⇀[C×A,B×A] ≡ λf.arrswap⋙firstf⋙arrswap
と定めと、
second(arrM) = arr(id×M) secondF⋙arr(M×id) = arr(M×id)⋙secondF second(F⋙G) = secondF⋙secondG secondF⋙arrsnd = arrsnd⋙F second(secondF)⋙arrassoc = arrassoc⋙secondF
が成り立つ。
ここで、
swap : A×B⇀B×A ≡ λp.⟨sndp,fstp⟩ snd : A×B⇀B ≡ λp.sndp
と定めている。
すなわち順に、 直積の左右を入れ替える関数, 直積から第 2 成分への射影関数である。
この逆に、 Arrow のプリミティブな項として first の代わりに上記の 5 つの等式を満たす second を導入した場合でも、 同様の方法で first を定義することができ、 それは 定義 1.4 中の後半 5 つの等式を満たす。
したがって、 Arrow を定義するときに、 first のみをプリミティブな項として入れるか、 second のみをプリミティブな項として入れるか、 もしくは両方とも入れるかは、 単に慣習の問題であって、 どれを採用しても結局同値な体系になる。
これ以降では、 利便性のため second もプリミティブに入っていたものとして議論する。
さて、 以上の準備のもと、 前回の結果の逆が示せる。
これを証明するにあたっての核となる箇所は、 Arrow において特定の等式が成立することを確かめるところであるが、 これはただ計算すれば良いだけので、 示すべき等式を挙げるだけに留めて計算の過程は省略する。
命題 4.2.
Arrow における型割り当て Γ⊢M:A および Γ⊢N:A に対し、 任意の豊穣 Freyd 圏で M=N が成り立つならば、 Arrow で M=N が成り立つ。
証明.
圏 を以下のように定める。
- の対象は、 Arrow の型全体とする。
- の対象 A,B の間の射は、 Arrow の型割り当て a:A⊢M:B の等号 (および自由変項 a の名前の変更) による同値類全体とする。
この同値類は {a:A⊢M:B} もしくはより簡潔に {M} で表す。
- の対象 A 上の恒等射は、 {a:A⊢a:A} とする。
- の射 {a:A⊢M:B} および {b:B⊢N:C} の合成は、 {a:A⊢N[b:=M]:C} とする。
よく知られているように、 このように定めると実際に圏を成し、 いわゆる Arrow の構文圏と呼ばれるものになる。
さらに、 Arrow は λ1× を部分システムとして含むので、 これはカルテシアン閉圏になっている。
続いて、 -豊穣圏 を以下のように定める。
- の対象は、 の対象全体とする。
すなわち、 Arrow の型全体である。
- の対象 A,B に対し、 その間の射対象を [A,B]=[A,B] で定める。
- の対象 A に対し、 恒等射を定める射を、
jA={u:1⊢arrid:[A,A]}
とする。
- の対象 A,B,C に対し、 合成を定める射を、
cABC={p:[A,B]×[B,C]⊢fstp⋙sndp:[A,C]}
とする。
これが実際に -豊穣圏を定めるためには、 3 つの等式
arrid⋙F = F F⋙arrid = F (F⋙G)⋙H = F⋙(G⋙H)
が成り立つ必要があるが、 これはまさに Arrow の公理の一部そのものであるから成り立つ。
次に、 にバイノイダル圏の構造を定める。
の対象 A,B に対して A⋉B=A⋊B=A×B とし、 さらに の対象 A,B に対して、
(-⋉B)AA = {f:[A,A]⊢firstf:[A×B,A×B]} (A⋊-)BB = {f:[B,B]⊢secondf:[A×B,A×B]}
と定める。
これが関手 -⋉B と A⋊- を定めるための条件は、 4 つの等式
first(arrid) = arrid second(arrid) = arrid first(F⋙G) = firstF⋙firstG second(F⋙G) = secondF⋙secondG
に帰着されるが、 最初の 2 つの式は明らかに成り立ち、 残りの 2 つの式は Arrow の公理と命題 4.1 の一部そのものである。
さらに、 に前モノイダル圏の構造を定める。
まず、 ⊤=1 とおく。
さらに、 前モノイダル圏に必要な 4 種類の構造射を、 の対象 A,B,C に対し、
αABC = {u:1⊢arrassoc:[(A×B)×C,A×(B×C)]} λA = {u:1⊢arr(λa.⟨⋆,a⟩):[A,1×A]} ρA = {u:1⊢arr(λa.⟨a,⋆⟩):[A,A×1]} σAB = {u:1⊢arrswap:[A×B,B×A]}
で定める。
これらがそれぞれ各変数について自然であることは、 7 つの等式
first(firstF)⋙arrassoc = arrassoc⋙firstF second(firstF)⋙arrassoc = arrassoc⋙first(secondF) second(secondF)⋙arrassoc = arrassoc⋙secondF F⋙arr(λa.⟨⋆,a⟩) = arr(λa.⟨⋆,a⟩)⋙secondF F⋙arr(λa.⟨a,⋆⟩) = arr(λa.⟨a,⋆⟩)⋙firstF firstF⋙arrswap = arrswap⋙secondF secondF⋙arrswap = arrswap⋙firstF
に帰着され、 さらに、 これらがそれぞれ中心的であることは、 8 つの等式
first(arrassoc)⋙secondF = secondF⋙first(arrassoc) second(arrassoc)⋙firstF = firstF⋙second(arrassoc) first(arr(λa.⟨⋆,a⟩))⋙secondF = secondF⋙first(arr(λa.⟨⋆,a⟩)) second(arr(λa.⟨⋆,a⟩))⋙firstF = firstF⋙second(arr(λa.⟨⋆,a⟩)) first(arr(λa.⟨a,⋆⟩))⋙secondF = secondF⋙first(arr(λa.⟨a,⋆⟩)) second(arr(λa.⟨a,⋆⟩))⋙firstF = firstF⋙second(arr(λa.⟨a,⋆⟩)) first(arrswap)⋙secondF = secondF⋙first(arrswap) second(arrswap)⋙firstF = firstF⋙second(arrswap)
に帰着される。
これらの等式は全て簡単な計算によって導かれる。
最後に、 Freyd 圏の構造を定める。
の対象 A,B に対して、
JAB={m:A⇀B⊢arrm:[A,B]}
と定める。
これが対象上恒等的であるための条件は、 2 つの等式
arrid = arrid arr(M⊳N) = arrM⋙arrN
に帰着される。
また、 これが前モノイダル圏の構造を保つことは、 2 つの等式
arr(M×id) = first(arrM) arr(id×M) = second(arrM)
に帰着され、 さらに、 これが中心的であることは、 2 つの等式
first(arrM)⋙secondF = secondF⋙first(arrM) second(arrM)⋙firstF = firstF⋙second(arrM)
に帰着される。
これらの等式も全て簡単な計算によって導かれる。
以上により、 豊穣 Freyd 圏 (;,J) が得られ、 定義によって Arrow のこの圏への解釈はほぼ恒等写像になっていることが分かる。
したがって、 型割り当て Γ⊢M:A および Γ⊢N:A に対し、 任意の豊穣 Freyd 圏で M=N が成り立つとすると、 特に今定義した (;,J) においても M=N となり、 それはすなわち Arrow で M=N が成り立つということである。
以上で、 圏論側で等式が成り立てば型システム側でも成り立つこと (完全性) も示されたことになる。
前回の結果と合わせれば、 以下が得られる。
定理 4.3.
Arrow における型割り当て Γ⊢M:A および Γ⊢N:A に対し、 任意の豊穣 Freyd 圏で M=N が成り立つための必要十分条件は、 Arrow で M=N が成り立つことである。
これで、 アローの圏論的対応物を見つけるという当初の目標が達成されたことになる。
次回以降は、 アローに付加的な構造を加えたものについて、 同様に圏論的対応物を探す話をしていきたいと思う。