ガロア理論一段落

一段落詐欺はいろいろあるわけですけどね。プロシンのネタので、締切前に終わっていたはずなんだが、まぁ、良くある。

残ってたのは順列の数え上げと交換子の数え上げがちゃんとできてるどうか調べるだけなので簡単だったはずなんだが....

順列の数え上げ自体は簡単で高校生でも書けるプログラムなわけなんですが、結構、難航。Fresh List の慣れもあるかな。

普通プログラムって何通りも書き方があって、まぁ、だいたいどれでも動くわけ。ところが、Agda だと

　　停止性とか、順序の正しさ、そして、全部入っていることを確認する方法

とかが全部つながってないとダメ。つまり、かなり特定の方法、再帰に特化した方法で書くことが必要らしい。

結局、三四回書き直す羽目に。でも、図書いて、ちゃんと再帰になるように書いたら、ぐっと短くなった。で、できあがり。長かった。

交換子の数え上げの方は任意のFresh List二つの組み合せに抽象化できるらしいんですが、ちょっと書き方がわからなくてやってません。

ガロア理論と言っても正規拡大体とかやってないけど、Agdaはむしろそっちの方が得意かもな。圏論に近いから。

来年は、チコノフの定理やろうかな。集合論あるし。Filter で圏論的にやるなんて言う手もあるらしい。

そんなわけで、詳細は、オンラインで開催されるプロシンで話します。

https://github.com/shinji-kono/Galois