YouTubeで3*3魔方陣は1種類しか存在しないことをやっていた。
これをプログラムでやったらどうなるだろう。
最初はEgisonでやっていたけれど、計算が終わらないのでやめた。
ソースだけ貼っておきます。
第一段階
Haskellでやることにする。
リスト[1..9]に対して順列を出力する関数permutationsをかまして、
後は縦・横・斜めの和が15になるものをフィルタリングすれば良いだろう。
（一列の和が15というのは分かっているものとします）
*MagicSquare> answer1 [[2,9,4,7,5,3,6,1,8],[2,7,6,9,5,1,4,3,8],[8,3,4,1,5,9,6,7,2],[8,1,6,3,5,7,4,9,2],[4,9,2,3,5,7,8,1,6],[4,3,8,9,5,1,2,7,6],[6,7,2,1,5,9,8,3,4],[6,1,8,7,5,3,2,9,4]]
8個出力された。
第二段階
魔方陣の回転と鏡映を同一視する。
これは二面体群D4になるのかな？ 位数が8なので計算結果とも一致している。
9要素タプルをnewtypeする。
回転と鏡映を考慮した、Eqクラスのインスタンスにする。
そして、先頭要素D4 (2, 9, 4, 7, 5, 3, 6, 1, 8)と残りを比較する。
*MagicSquare> answer2 [True,True,True,True,True,True,True]
これで、3*3魔方陣は1種類しか存在しないことが証明できた。
.
.
Idrisでもやってみたいが、どうやるのだろう。
ラムゼーの時もそうだったけれど、
組み合わせ系は、定理証明支援系は苦手なのかもしれない。
IdrisでもHaskellと同じように「計算」すればいいかな、とも思ったけど、
それでは意味がないな、と考える。
.
.
