bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

継続の圏 続き

前回の日記のあと、さかいさんから個人的に指摘もらいました。「この圏はCCCじゃないんじゃないか」と。

CCCに対応するのは直観主義論理なのですが、一方で継続 ~X が Xの双対なら、~~X が X と同型になりそうなのです。つまり、~X を「Xの否定」とみなすと、排中律が成り立っちゃうかもしれないと。

ありゃー、一から考え直さないといかんかなー。

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。