Categorical Programming(2) -

http://d.hatena.ne.jp/m-a-o/20091020#p3
の続き。

ここらへんの話
http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf

よく考えたら直和を持つcartesian closed categoryは、distributiveになる。証明は、

$Hom(A \times (B+C),X) = Hom(B+C , X^A) = Hom(B,X^A) \times Hom(C,X^B)=\\Hom(A \times B ,X) \times Hom(A \times C, X) = Hom((A \times B) + (A \times C),X)$

なので、あとは米田の補題。

てことで、CPLもCHARITYもdistributiveになって、多分この二つは等価なんでしょう

それから論文の定理で

Proposition 3.3.2: If a cartesian closed category C has the natural number object,
it has all the primitive recursive morphisms.

というのが面白かった。まあ、CCCは単純型付ラムダ計算のモデルなので、当然と言えば当然なのかもしれない。でも、原始帰納関数を含んでいることは言ってるけど、それ以外にどれくらいの関数を含んでるんだろうか？
・CHARITYのサイトには、CHARITYで書けるコードは全部停止することが保証されると書いてある
・原始帰納的じゃないけどAckermann関数は書けるらしい
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20030114#p01
高階原始帰納関数ってなに？

さて。
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20050215#p02
によると、不動点と有限直和を持つcartesian closed categoryは自明なものに限るらしい。

圏論的に破綻してても気にしないというのでもいいけど、それだと話が終わってしまうので、よい計算モデルにはよい圏が対応していると信じて、なんか条件を緩めたい。諦める方向性としては4つくらい思いつく。

1)不動点を諦める
と、CPL/CHARITYとかになる。これはこれでいいけどTuring completeになってほしい

2)直和を諦める
Categorical Abstract Machineとかの方向性がこれなんだと思う。一応、Fixとかあるっぽいけど、代わりに直和がない。

3)exponentialを諦める
cartesianだけど、cartesian closedでない。という設定だとどうなるんだろう。

4)直積を諦める(モノイダル積にする)
cartesian closedだと、自然な(文字通り、自然変換になってる)対角射と射影が存在して、上の定理の証明でも本質的に効いてる。逆に、「自然な」対角射と射影が存在するようなmonoidal categoryは、cartesianになりそうな(要証明)。

monoidal categoryだと、そもそもnatural number objectの定義自体が不明だけど、適当なcomonoid objectが存在して、natural number object相当のものは定義できそうな気もする。ついでに、不動点の定義も曖昧だけど、cartesian monoidal categoryで不動点とtraceが等価なので、考える圏としてはtraced symmetric monoidal closed categoryあたり？ついでに、直和というより、加法圏とかにするのが自然な気もする。こういう圏で自明でないものはいくらでもある(例えば、有限次元ベクトル空間の圏)

考えてる圏としては、linear lambda calculusのそれに近い気がするけど、線形論理の方には、linear exponential comonadとかが必要らしいが、こいつが何なのかよく分からない(定義は理解できるけども、何で必要なのかとか、そのへん。。)

ただまあ、丁度CCCからCAMが出るように、symmetric monoidal closed categoryからLinear Abstract Machineというのを定義できるらしい(が、元論文はopenでないので未確認)

5)その他
あとは、locally cartesian closedだと、依存型に対応する(らしい)とか。でも、依存型ってあまり好きでないので、興味なかったり