計算機言語を使った定理証明の会
10月24日 東京は大久保です。
人が7人ぐらい居ないとちょっと広いなーという部屋を借りてしまっているので、俺はやるぞ！！って人はなんとしても来てください。
全く宣伝になってないなー。
「当日までにやってくるべきお題」がまだfixされていないですが、今は案を出している感じなのでこれはやってみたいかも、というものが在れば書き込んでください。
これはどういう会なの?
ちゃんと明文化していなかったのでここで書いておきます。
最近は、定理証明器という単語を割と耳にする機会が増えた気がしますがそれは間違いなく気のせいです。
で、ただAgda2とかIsabelle/HOLとかCoqとかで定理を証明するよーっていうのは、割と調べれば出ます。っていうかそもそも定理を証明する事を目標にしているので調べれば色々と出て来ます。まぁ日本語リソースは少ないですが。
ただ、ライブでいんたらくちぶに、それらの使い方を日本語で見せてもらうというのは今の所は貴重な機会だと思います。ので参加しましょう！
それから今回は、そもそも定理を証明する方向の言語を使うだけでなくて、普通のプログラミング言語(C++,Haskell,Prolog[なんか偏ってるかなぁ...],Ruby??)でそういう「定理を証明する」ような事をやってのけるとすると、どういうテクニックが要るだろうかという所にも注目したいと思います。
ので、今回はじっくり味わいながら議論して1,2個の大きな定理を証明するというよりは、小さいヤツを幾つか証明しつつテクニックを蓄えよう(参加者は頭良い人ばっかりなので私は蓄えさせてもらうだけですけど)という趣きです。
そういう感じですから、今ATNDに入れてるお題(当日までにやってくるべきものです！)は簡単なモノが多いです。証明を頑張るというよりは、自分の言語でどうすれば出来るかという部分に時間が掛かると思っているので。
今の所は極端に難しい定理は無いですから、馴染みの無い方も是非参加してください。
