計算機言語で定理証明#1

さる10月24日　土曜日に大久保で次のようなイベントがありました。

http://atnd.org/events/1507

ありましたもといやりましたもとい出来ました。

何度かこのブログでも人が少ない困ったみたいな事を書いたのですが、当日は最終的に9人の参加になりました。すごい。こんな意味不明な集いに9人...　ありがとうございました。

当日の流れは、twitter検索で#proofpartyとかやってもらえれば、ほんの少し分かると思います。

http://search.twitter.com/search?q=%23proofparty

スライド

私が発表で使ったスライドは次です。発表という程でもなくてオープニングで使ったのですが。

にゅもんあぐだ

View more documents from ranha.

これは何かというと、Agda2を飛び出して他に行こうというスライドです。

感想

AgdaとCoq

何も考えないでAgda2で証明を書くとこうなる、という良いお手本があるのでそれは後で上げるとして。

私のスタンスとしてはAgda2を使うって言うのは証明を書くというよりも、依存型を持ったマゾい言語でプログラム書いてという感じなので定理証明器を使っているという感じはしてませんでした。し、今もあんまりしてません。

所がどっこいで、当日kikxさんのCoqを使ったLive-Proofingがエキサイティング過ぎたのでこれはボクの知ってる定理証明器と違う！！そういう気分がふつふつと沸き上がったのです。

CoqのLive-Proofing見ていて思った事は
1.証明をちゃんとモジュール化している
2.ライブラリの証明を使い易い(しかもHoogle、とは違いますが証明検索も付いてる)
3.本当に証明しているという感じ
4.Agda2のココは気が利かないよなぁという所も実は考えられている感
で偉い子過ぎるなぁと・・・。

Coqは多分ああいう「証明本気モード」とは別に、Agda2でやってるような「依存型付き関数型言語」っぽい使い方も出来るのでどう見てもCoqですありがとうございましたという感じでした。みんなCoqをやろう。

それと関連して面白かったことは、確かいけがみさんが「なぜAgdaをあえて使うんですか?」ということを尋ねられて。
私はまぁ最初見つけたものがたまたまAgda2で、見た目がHaskellっぽかったのと割と書ける(使えるという意味では無いです)のでだらだらとやってるとかそんなんかなぁみたいだったのですが、さかいさんもたまたまAgdaで早くどうこうしたいという事を言っていてお互い運が悪いと深く悲しみました。

いけがみさんのスライドは、Webで見てもしょうがないよなぁと思うんですが、不味い部分を削って上げてもらえれば楽しいかと思うので期待が届けばきっと上がるんでしょう！

お題について

「すうがく(実数ですけど...)」と「ハノイの塔の 2^n - 1の動かし方が最小になる」以外は片付いてました。
まぁそれは簡単なので良かったとしてこの残った連中がどうしてやろうという感じですねハイ・・・。

IVT(中間値の定理)については、kikxさんがCoqの実数ライブラリ辺りを使って駆逐。
ただ、結局Coqはどういう実数の構成にしているんだろう・・・。

私は取りあえずAgda2で妥協した証明(postulateを使う)をするならどの辺で妥協しようかなぁという点を探ってましたが良いのが思いつかず。
難しそうなのは賢い人に任せてまたC++でやろうかなーと思って取りあえずtemplateの所にintは書けるけどdouble書けなくて計算機εとかでεを誤摩化してベターっと証明書けないやんけ！！なんでですか?という事を質問してしまった。でまぁでもほんと何でだろうと思っていた所、kinabaさんからそれD( http://twitter.com/kinaba/status/5119588120 )が飛んで来たので流石C++の来世の姿であると思うなど。

でも結局色々考えたけどそれ在った所でどうにもっていうか・・・。

すうがくは頭の悪い私には適当に数学の実数の辺りのソレらしい所を公理として入れちゃってまぁソレで良いんじゃないかなぁという。あんまり計算しない人間が沢山計算を頑張る計算機のそのあたりの事で文句を言う筋合いは無いと思うしでも個々を生かせって事もあるので結局分からないです。

ハノイの塔は、手数が最小になるという証明を人間に対してやる時は簡単なんですけれども、それをどう表現してやるかとかで大変だなぁと思っていて結局最後まで出来ませんでした。

構造を数学的に表して(どう表すかを考えるのが...)、かつその数学的構造上の何ソレが定理証明器で表現出来るんだったら出来るだろうしうーん。

いやまぁ証明自体は出来てるくさいんだけどこのギャップが結構楽しいかなーっていう気がします。もっというと、私は機械に教えてあげられる程には証明そのものを理解出来てないんでしょうね。

こういうのは勿論苛ついたりしますけどそれなりに楽しいです。

その他1

shelarcyさんのNot 98 Haskell for Proofが出てこなかった残念過ぎた・・・。

あとGHCは今の所としてはtypesさんがtermsさんを馬鹿にしてる感じ(ここの説明は凄くイカしてると思います => http://strictlypositive.org/winging-jpgs/)でダメだと言っていたのですが、sheというプリプロセッサ(http://personal.cis.strath.ac.uk/~conor/pub/she/)があるらしいので、Conorさんは分かっている凄い人だと思いました。

GHCにはAlgebraic Kindも入るとかで(いつかは知りませんけど)後3年後ぐらいに期待出来ると良いんじゃないかと思いますハイ。

その他2

pirapirapiraさんの運んで来たドミノ DE 自然演繹(http://www.winterdrache.de/freeware/domino/index.html)が酷過ぎて酷かった。これは本当に酷いです。

その他3

m0h1canさんに、Prologでも「すうがく」周りはどうにも成りませんかね、という無茶ぶりをした所、取りあえず実数をGray Codeにencodingしてみたけど結局なぁーという話を出してくれてそれがとても面白かったです。

(参考 : http://www.i.h.kyoto-u.ac.jp/~tsuiki/bit/gray.html)

カタン

カタンは今度眠く無い時にまたやりたい・・・。

あのゲームは、他の人がどういうカードを取って行ったのかとかちゃんと覚えとけば大分面白そうだなぁとかは。
結局2つのサイコロの目の和の出易さとかあるしフムフムだし、謎カードを私は一度も使わなかったので謎カードの効果は結局どんなんがあるだろうとか。

まぁルールが分からないのに一応出来たのは、徹底的にゲームの補助に回ってくれたいけがみさんのお陰という事に尽きます・・・。

肉、肉を食べる

その前に。建物を出て懇親会場に向かう時に、関東ITソフトウェア健保会館(今回集った場所)には中華レストランがあるのですが、眼鏡をかけたミニのチャイナドレスを着た人が給仕をしていて。
その雰囲気が凄く様になってるというか、かなり美人でふぇろもんでこれは良いものを見たなーとか一人で思っていました。いやあれは凄かった。リアルも捨てたもんじゃない・・・。

懇親会があれば、その時に第2回をやるかやるならどういうネタでやるかという話をしようと思ってたので、まぁしてみました。

結果としては、

圏論
グラフ理論
メイド喫茶(メイド喫茶行きたい過ぎる...)
証明器は投げ捨てるものなので計算可能な○○主義から攻める?

とかその辺が出ました。

それらは後でWiki(http://ranha.kerox.info/proofparty/)に書いておきます。
=> 第2回のページ

4色定理は個人的に凄くやりたいんだけど、一方その場でのウケは非常に良く無かった。いや確かに大変そうだなーと思うけどうーん・・・。

まとめ

Coqを使おう。

m0h1canさんのお陰で今回も場所が確保出来ました。いつもありがとうございます。

更にその他

帰りに電車の中で、pirapirapiraさんと"The Definition of Standard ML"を使ってなんかしたいよねしたい！！という話をしていたけど、適当にやるとSMLのType Checkerを実装とかになるのみだよなぁしかしソレは適当に出来るのであってもうちょっと固まったらなんとか。

年末年始つくばに来ても良いとか言ってらっしゃっていて、まぁ私は年末年始もつくばに居るのでカモンカモン！！とか言っておいたけど多分そんな時にやっても誰も来ないでおじゃる・・・。