去年の四月あたりにもやってたんですけどね。その時は、Graph にCCCの要素(直積とカーリー化とか)を入れて、射のリストで圏を作って、それから Sets への関手を作る方式だった。
まあ、それでSetsはCCCなんでそれで良かったんですが...
でも、これが直接に Functional Completeness に関係するらしく、しかも、Graph から Sets に map する時に仮定した Graphに集合と関数を割り当てるのが邪魔。
なので、直接、証明する気になった。なのだが、さすがに卒論修論でできなかったんですが、3月結構やってたんだが、
風邪気味なのか、頭が廻らん
で、ぜんぜんできず。いや、そんなに難しくないはずなんだが。なにせ、ネタ本(Higher order categorical logic)では一段落でさらった書いてあるだけ。
Graph にCCCの要素を入れて、射の同値類を作ればできる
あぁ、そうですか。なんですが、最近だいぶ蘇ってきたので進んできました。
Graph から圏を作る時には射のリストを作るのだが、CCCの要素を入れる時にリスト側にいくつか入れると良いらしい。
T への射 ○ a はリスト側
二つの射をまとめる < f , g > はリスト側
これで、なんとなくできそうな気がしてきた。 あとは結合律だな。
まぁ、でも数学できる人は、この手のものは瞬時に理解できるんだろうなぁ。
下の case が演繹定理の場合分けに対応していて、演繹定理が Functiona Completeness ってことになるらしいです。
data Objs : Set (c₁ ⊔ c₂) where
atom : (vertex G) → Objs
⊤ : Objs
_∧_ : Objs → Objs → Objs
_<=_ : Objs → Objs → Objs
data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i
arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b)
π : {a b : Objs } → Arrow ( a ∧ b ) a
π' : {a b : Objs } → Arrow ( a ∧ b ) b
ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
_* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b ) --- case v
data Arrows : (b c : Objs ) → Set ( c₁ ⊔ c₂ ) where
id : ( a : Objs ) → Arrows a a --- case i
○ : ( a : Objs ) → Arrows a ⊤ --- case i
<_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) --- case iii
iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv
_・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
id a ・ g = g
○ a ・ g = ○ _
< f , g > ・ h = < f ・ h , g ・ h >
f ・ id b = f
iv f (id _) ・ h = iv f h
iv π < g , g₁ > ・ h = g ・ h
iv π' < g , g₁ > ・ h = g₁ ・ h
iv ε < g , g₁ > ・ h = iv ε < g ・ h , g₁ ・ h >
iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h >
iv f ( (○ a)) ・ g = iv f ( ○ _ )
iv f (iv f₁ g) ・ h = iv f ( (iv f₁ g) ・ h )
http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/tip/CCCGraph1.agda
No comments:
Post a Comment