このブログは、論理プログラミングを無限に実行する場合、実行順序を指定する機能を追加することを目的としています。現在は「無限の項書き換え」のような方法で記述する方法を検討しています。
エレファントな群とリー代数
項書き換えと同様の方法で群やリー代数で成り立つ関係を示すということをやっています。現在はマグマとモノイドで成り立つ関係について書いています。項書き換えの標準的な記述方法は『Universal Algebra for Computer Scientists (Monographs in Theoretical Computer Science. An EATCS Series, 25)』または『計算論理に基づく推論ソフトウェア論』に書かれていると思われますが、まだ全部読んでいないのでよくわかりません。また、項書き換えを無限に繰り返したものを扱うには「多項式の代入」の記述方法の方が良いのではないかと思われるため、現在はそのような記述方法になっています。この方法が有効かどうかはまだわかりません。
現在は環で成り立つ関係を示すということをやっています。この内容は『環の演算』で書いたものです。ここでは書き換え規則を合成するということをやっています。これを説明するために、現在は単一化について説明しています。単一化については『計算論理に基づく推論ソフトウェア論』に書かれているようなのでこの本を見ています。
今後は合成を無限に繰り返したものを記述する方法について考えていきます。このような記述方法があれば、数学の理論でプログラムとして記述することができるものがあると考えられます。このような記述方法がないために記述する方法がないという誤解があるという気がするので、それを解消したいと考えています。
代数的構造による圏論
現在は『圏論の道案内 ～矢印でえがく数学の世界～ 数学への招待』という本を随伴の項目まで読んでいます。「項書き換え」のような方法で随伴を記述するということが目標ですが、現在はまだ随伴のことがよくわかっていないので本の引用だけになっています。
数学的帰納法、可換モノイド、連立一次方程式については、残念ながらこの本にはこの後とくに記述がありませんでした。
前回の中間報告以降更新していない項目
エレファントな整数論
この項目も「項書き換え」のような方法で
- 数学的帰納法
- 割り算の定義 → ユークリッドの互除法
- 素数の定義 → エラトステネスのふるい
- 素因数分解の(可換モノイドとしての)一意性
の記述ができないか、今後考えていきます。
エレファントな線形代数
この項目も「項書き換え」のような方法で、連立一次方程式の解法や行列のランクなどを、行列を使わずに記述できるかを今後考えていきます。
エレファントな関数論
この項目も「項書き換え」のような方法で、コーシーの積分定理の証明について記述できないか、今後考えていきます。
今後の予定
現在は「無限の項書き換え」のような方法で数学の問題を記述する方法を検討しています。今後は他の方法も検討していき、プログラミング言語で表すことを目標としています。
