■

突然いろいろやる気を失なった。

Coqむず杉。関数型言語ってよく知らんからその勉強がてら読みはじめたのが去年の今ごろだった。SoftwareFoundations

そもそも読み初めようと思ったのは、SICP読んでて、4章でprologっぽいものが出てきて、ここで扱われてる論理は、現実の論理と同じものであるか？みたいなの(4.4.3)を見て、ついていけなくなった。(分からなさすぎて)

そもそも論理ってなんや？
論理学ってのもあまり分かってないし。Bool値の計算とはちょっと違うらしい。

コンピュータで記号論理を扱うのはどうすればいいのか？ということをつらつら探すと、Coqというものがあり、その入門として、SoftwareFoundationsが優れているらしいので、読みはじめたんだった。

ついでに関数型言語の勉強にもなると書いてあったし。(女子高校生が書いたhttp://www.iij-ii.co.jp/lab/techdoc/coqt/ は、関数型言語の知識が前提だったのでパス)

中高で殆どが意味不明だった数学の証明がコンピュータ上で表すことが出来るとは!ということで、すごく面白かった。かったんだけども。本当に欲しかったのは、中学校のとき殆どが超意味不明でついていけなかった幾何の証明だ。あれが、Coqみたいな感じでコンピュータ上で実行出来るなら完全に数学をやりなおせるんじゃないかと。でも残念ながらそうゆうのはまだ無いらしい。ユークリッド幾何学が形式化されてないからか？情報幾何というのがあったけど全然関係なさそうだ。いつか偉い人が幾何学の証明オブジェクトをコンピュータ上に構築してくれることを期待します。

しかし、なんでも最初は簡単で面白いんだけど、ちょっと進むと途端に難しくなるよな。