前に「週刊 代数的実数を作る」という一連の記事を書きました。
あれの続きじゃないですが、また計算機代数周りの記事を書きたいなあと最近思っています。
せっかく書くなら、今度は構成的数学の視点を取り入れたいです。
構成的数学についてWeb検索したらこういうサーベイが見つかりました：
- 石原 哉、構成的数学とその動向
構成的数学にもいくつか流派があり、直観主義論理を生むことになったBrouwerの直観主義、Markovの構成的数学（このMarkovさんはMarkov過程の人の息子らしいです）、そしてBishopの構成的数学などが挙げられるようです。
直観主義論理は排中律を採用しないことで有名かと思いますが、Brouwerの直観主義やMarkovの構成的数学はさらに過激で、古典数学と矛盾する原理 (principle) を認めているらしいです。Bishopの構成的数学はそれらよりも穏健で、「直観主義論理に基づくが、古典数学と矛盾する原理は採用しない」立場を取ります。そのため、Bishop流で成り立つ結果はBrouwer流、Markov流、古典数学のいずれでも成り立ちます。
Bishop流の構成的数学のスタートは1967年の
- E. Bishop, Foundations of Constructive Analysis, McGraw-Hill, 1967
という本で、解析学を構成的にやっています。この本は一旦絶版になり、改訂版みたいなものが
として出ています（Bishopはこの本が出る前に亡くなったようですが）。最近になって別の出版社が1967年の本を復刊（？）したようです。
他の分野については、Bishop流の代数学が
で行われています。私の当面の興味は代数学なので、この本で勉強しています。
Bishop流では非構成的な原理・公理は採用しないということでフルの選択公理も採用しませんが、従属選択公理は採用するようです。
排中律やフルの選択公理の他には、principle of omniscience（訳すなら「全知の原理」とかですかね）と呼ばれる原理が除外されます。具体的には、
- the limited principle of omniscience (LPO): \({0,1}\)からなる列\(a_n\)について、「全ての\(n\)について\(a_n=0\)」または「ある\(n\)について\(a_n=1\)」が成り立つ
という原理で、古典数学ならこれは排中律を使って証明できます。ですが構成的数学では排中律がないので別途検討が必要で、この原理は構成的とは見做されません。
構成的数学では集合の取り扱いも独特なようで、Bishop流では「集合は要素を構成する方法（？）によって定義され、同値関係\(=\)を備えたもの」という風になっています。どことなく型理論っぽさがあります。同値関係を備えた集合はsetoidと呼ばれることもあるみたいです。
古典数学では同値関係があったら同値類を作って商集合を構成するところですが、おそらく「有限とは限らない集合からなる集合」をまともに取り扱いたくないからこうしているのだと思います。計算機の上で商空間みたいなのを扱う場合は、同値類なんて使わずに、イコール演算子をオーバーロードしたり、完全代表系を取ったりすると思いますが、構成的数学もそんな感じなのかもしれません。
（ちなみに、構成的な集合論では冪集合公理も制限の対象になるらしいです。）
構成的代数ですが、無限集合を第一級の対象として扱うことに難があるので、イデアルなんかは有限生成なものしかまともに取り扱えなさそうです。
古典数学ではNoether環なら任意のイデアルが有限生成ですが、「任意のイデアルが有限生成」という主張は非常に強く、構成的な観点からは零環以外の環についてNoether性を証明できないという風なことがどこかに書かれていました。
古典数学では複数の条件が同値であることを示してその条件を満たすものに名前をつけるということがよくありますが、公理を減らした数学では条件の同値性が示せなかったりします。なので数学的対象の定義が古典数学でお馴染みのものとは違っていたりします。
例えば、古典数学では単項イデアル整域の定義は「任意のイデアルが単項イデアルであるような整域」ですが、「任意のイデアル」について主張するのは構成的には扱いづらいのか、構成的代数では「任意の有限生成なイデアルが単項イデアルであって（つまりBézout整域）、単項イデアルについての昇鎖条件が成り立つ整域」という定義を採用するみたいです。この条件は古典数学の元では古典数学での定義と同値です。
また、一意分解整域（UFD）の概念も4個くらいに分裂するようです。
構成的数学については、今度Handbook of Constructive Mathematicsという本が出るようです。いいお値段がしますが、是非読みたいです。
計算機代数の方は、「代数的実数を作る」でやり残したこと、LLLとか、代数体とか、p進数とかをやりたいです。それから、さっき有限生成イデアルに言及しましたが、Gröbner基底もちゃんと勉強したいと思って何年も経ちました。
「記事を書きたいなあ」と最初に書きましたが、まだ勉強中の身で記事を書きたいとか烏滸がましいですね。まずは勉強して自分用のノートを作りつつ、理解が深まれば公開等を考える、という形にしようと思います。
【追記】構成的数学について色々調べていた時のメモを貼っておきます。
↑Constructive Mathematicsで検索すると上の方に出てくるやつ。とりあえず読んどけ。
そういえば、構成的数学の教科書は Beeson と Troelstra & van Dalen しか知りません。他にお勧めはあります？
— Hiroyasu Kamo (@kamo_hiroyasu) January 28, 2019
↑↓挙げられているのは以下の2つ：
- Michael J. Beeson, Foundations of Constructive Mathematics: Metamathematical Studies
- A.S. Troelstra, D. van Dalen, Constructivism in Mathematics, Vol 1, Volume 121 – 1st Edition
↑Beesonの方は（Springerの電子版セールで）既に私の手元にあった。
#こんなの読んだ
— Jun Inoue (@jun0inoue) May 17, 2021
https://t.co/fraFznjSNt
理解度80%
完全にタイトルの出落ち感で読んだ論説。タイトル通り、構成主義懐疑派にありがちな誤解を five stages of grief に擬え、説教していく宗教勧誘広告。 1/18
- Andrej Bauer, Five stages of accepting constructive mathematics
↑読み物。
- Henri Lombardi, [1903.04200] Algebra in Bishop’s style: some major features of the book “A Course in Constructive Algebra” by Mines, Richman, and Ruitenburg
↑A Course in Constructive Algebraの紹介っぽい
- Henri Lombardi, Claude Quitté, Commutative Algebra: Constructive Methods: Finite Projective Modules Finite Projective Modules
- [1605.04832v3] Commutative algebra: Constructive methods. Finite projective modules
↑これも構成的代数の本っぽい。元々フランス語で書かれたのが英訳された感じ。
- Ihsen Yengui, Constructive Commutative Algebra: Projective Modules Over Polynomial Rings and Dynamical Gröbner Bases
↑これも構成的代数の本っぽい。
【追記2】A Course in Constructive Algebraに載っている一意分解整域 (UFD) の定義ではGCDの存在が言えない気がしてきて、調べたらこんなのが見つかりました：
- ac.commutative algebra – Constructively correct notion of unique factorization domain – MathOverflow
定義に同伴（あるいは整除）が識別可能であることか、GCD整域に条件を追加する形で定義を書き直すか、ということになりそうです。
ピンバック: やりたいことリスト | 雑記帳