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になる。証明は、 なので、あとは米田の補題。 てことで、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は単純型付ラムダ計算のモデルなので、当
