A certified version of the Buchberger’s algorithm

http://citeseer.ist.psu.edu/321720.html
Buchbergerのアルゴリズム(Euclidのアルゴリズムが整数環のイデアルのよい生成元=最大公約数を求めるものであるのに対して、体係数の多項式環のイデアルのよい生成元=グレブナー基底を求めるアルゴリズム)をCoqで生成しましたよというお話らしい。すんげー。Coqのソースは
http://coq.inria.fr/contribs/Buchberger.html
で手に入る。かなり長大なので、読む気はしない。Coqは読みづらいよなー。

生成したOcamlのコードが600行で、それをきちんと動かすためのコードが+100行程度。証明には、一年の"part time activity"を要したとか書いてある。Buchbergerのアルゴリズム程度で、1年もかかってたらお話にならないんだけど、それでも、こういうことを実行したのは偉大だ。証明から正しいコードを自動生成するのもいいけど、逆に自分でコード書いてしまって、それが正しいことを示せないんだろうか。プログラムから証明を生成みたいな。現時点では、そっちの方が実用性はありそうだけど、プログラムの形を限定しないと無理そうだ。foldまみれで書くみたいな。と書いてて思ったけど、Buchbergerのアルゴリズムをfold尽くしで書くとどうなるんだろう。

ところで、任意のイデアルが"グレブナー基底"を持つようなネーター環の特徴づけみたいなのは存在しないのだろうか。整数環に対しては、Euclidのアルゴリズムが、体係数の多項式環に対しては、Buchbergerのアルゴリズム、それからWeyl代数に対しても、グレブナー基底を求めるアルゴリズムが存在する。けど、例えば、整数係数の多項式環については、そのようなアルゴリズムあ知られてないし(多分)、存在もしなそう。まあ、重要とは思えないから、誰も考えないだろうけど