数学的言説とアルゴリズムに落とせるということについて、ぼんやり考えたこと

自分は放言癖があるというか、思いついたことをよく吟味もせずにテキストにしてしまうことが多い。自分が書くコードもそのスタイルを反映して、思いついたpathをトレースして、それで書きっぱなしで終わることが多い。

ぼんやりとした思い付きと、(自然｜人工、programming)言語で記述された命題との間にはギャップがある。とはいえ、命題にもさまざまなクラスがある。

• 古典的な論理の世界だと、アルゴリズムを構成不能な命題というのは存在する。プログラムの停止性とか。
• 直観論理の世界ならば、だいたいアルゴリズムに乗るだろう。というか、構成的でないものを扱ってないわけだ。
• アルゴリズムが存在しても、有限の資源を持った計算機でできることはもっとかぎられる

こういう包含関係を集合論で記述するとき、集合論そのものはどのレベルなのか、みたいなジレンマは有名らしい。
圏論は、カテゴリーといいながら、こういう究極の包含関係をとりあえず棚上げしてすすむ。というか、有限の立場で、構造を保存しつつどこまでいけるか、という奥床しさを感じる。では、圏論では超越的な構造は扱えないのか？というあたりが自分にとってはまだまだよく理解できない。

inspired by

ブルバキとグロタンディーク

数学 その形式と機能