トポス(1) この段階で数学的帰納法を使うことによって図式を使わずに説明することができるようになったと思うのですが、簡単にはいかないのでトポスについてもう少し調べてみたいと思います。[4]、[5]、[6]、[7]の本を持っていたので少し読んでみようと思い…

このブログは、論理プログラミングに実行順序を指定する機能を追加するため、現在は主に数学的帰納法や可換モノイドについてプログラミング言語で記述する方法を調査しています。 前回の中間報告以降更新したもの 代数的構造による圏論 ← 斜めの線を使わない…

第5章まで読めばろいろできると思われるのですが、数学的帰納法について考えるには第7章まで読んだほうが良いようなのでさらに引用していきます。そこまでは少し図式を描いていきます。 第6章 冪：プログラムの本質 ①冪 定義 6.1 (冪) 積を持つ圏 の対象 に…

⑦極限，余極限の定義 続いて極限と積などの関係を見ていきます。 積・余積 圏 を対象が の二つで、射が恒等射だけの圏とします。 と書くことにします。 型の図式(圏 から圏 への関手) に対する極限( の終対象)が存在するとします。、 とおきます。「 を圏 (…

第5章 普遍性 最初の方は定義を引用するだけとします。 ①終対象と始対象 定義 5.1 圏 の対象 が、 の任意の対象 に対して から への射がただ一つ存在するとき、 を の終対象と呼びます。この一意的な射を と書きます。 の反対圏 の終対象を の始対象と呼びま…

自然変換については良い書き方が見つからないので、ほぼ「圏論の道案内 ～矢印でえがく数学の世界～」に従って書いていきます。 第4章 自然変換 ④自然変換の例2：hom 関手間の自然変換 まず「第3章 関手 ②関手の例1：順序を保つ写像，反変関手・双対圏」から…

このブログでは、通常の論理プログラミングでは無限に動くプログラムを書くことができないので「極限」の考え方でなんとかできないか、ということでやっています。ある種の射影的極限、帰納的極限は外積の定義を書いたところで書いたように、構成的に定義す…