このブログは、論理プログラミングに実行順序を指定する機能を追加するため、現在は主に数学的帰納法や可換モノイドについてプログラミング言語で記述する方法を調査しています。
前回の中間報告以降更新したもの
代数的構造による圏論 ← 斜めの線を使わない圏論
このブログでは普通の圏論の本に載っているような図式を書くことができないらしいので、「斜めの線を使わない圏論」では、自由生成モノイド、自由生成可換モノイド、自由生成半環などを構成するような方法で、極限、随伴などを説明することができないか検討していました。圏論の本に載っているような説明は私にはわかりにくいので、別の説明の方法があるかどうか考えていましたが、特に進展はありませんでした。
このシリーズでは、「圏論の道案内」を読みながら上記のような問題を考えていきます。
「圏論の道案内」では自然変換を中心に説明されています。「第4章 自然変換」、その前の「第3章 関手」ではたぶん自然変換に関連した例が書かれていています。その前に「前順序」の説明があります。このあたりは何かの説明に使えるかもしれません。
続いて、この本では「コンマ圏」を使って「第5章 普遍性 ⑥射圏，そして一般射圏」で極限が説明されています。この本では「コンマ圏」のことを「一般射圏」と呼んでいます。
「エレファントな整数論」で写像から作られる前順序集合について調べているのですが、そのような議論をするには「第7章 圏論的集合論」の「①トポス（topos）」、「②圏論的集合論」まで読んだほうが良いようなので、そこまでは読みました。
今の段階で
を結合律を使った書き方で書く方法を考えることができると思われます。しかし、トポスの定義がまだよくわかっていないので、他の本も参考にして調べています。「直観主義論理」や「型理論」に関する本もあったので読んでみることにします。これは無限に動くプログラムの連携に使えるのではないかと思っています。
「論理プログラミングとしての半環の標準化」というのは論理プログラミングの実行を「選言標準形」のような形に変形することと考えた場合どうなるかというものです。結合律のような法則により自然数より少し一般的な全順序集合の合成と考えることができます。これはモナドが関連するかもしれないのでモナドのところまで読んでみます。今のところこの「変形」を説明する言葉がないので、まずそれを考えた後で次に進もうと思います。
前回の中間報告以降更新していないもの
エレファントな線形代数
連立一次方程式の解法や行列のランクなどを、行列を使わずに説明することを引き続き考えていきます。
エレファントな関数論
コーシーの積分定理の証明について調査中です。
保留中のシリーズ
以下の記事のシリーズは、他の案件で進展があるまで保留中です。
今後の予定
まだどのような形で数式の「変形」を書けば良いのかわかっていないので、まずそこから考えていきます。その後いろいろな数学の問題について考えて、プログラミング言語で表すことができるのかどうか考えていきます。
