ProofParty第2回目の話
3/13日にProofPartyの第2回目がありました。
今回の内容は、
- 「ハノイの塔では最短手数が(2^n)-1となることを証明する」
- 「例の採用問題でLv4になる」
の2つがメインでした。
結果としては、前者がまだ書けていない、後者は既にyoshihiro503さんがCoqで証明(http://d.hatena.ne.jp/yoshihiro503/20100119)を書かれているのですが、私が今回Agda2でyoshihiro503さんの証明で言う所のSoundnessまでが書けたのでそこからは自明かなーという。
個人的には、当日ついにCoqをはじめる事になったのでそれはまぁ大変良かったです。rewriteとか単純に便利だよなーという。
Coqをはじめる原因としては・・・。実は私がやった証明がよしひろさんの証明とあんま変わんないんでねーか？みたいな質問があったので、Coq読めないけど読めないままではいかんでしょう！という事で、きくすさんやt_miyaさんやkencobaさんに教わりながら読んだ所同じような感じだった→けれどもよしひろさんのLOP(Line of Proof)の方が1/4か1/5程で大変な事に成ってるなーという。
当日解消出来なかった疑問としては
- CoqにおけるPropとSetの違いは何なんだろう
- Agda2におけるPropとSet0の違いは何なんだろう
- Agda2 2.2.6で入ったrewriteとかって具体的にどう便利なんだ・・・？ (Set Universe Polymorphismは($)を定義する時とか便利な気がしますネ)
懇親会
和民で懇親会もやったり。
懇親会で出た内容は
- Coq(やAgda2)で証明出来る範囲はどんぐらいなんだろう。多分どこかからは、自動定理証明系を使わざるを得ないと思うんだけど・・・。
- 我々は「証明を理解しなければいけない」のだろうか？果たして証明が理解出来るのはどの範囲までだろうか？
- Immutable Object(http://www.amazon.co.jp/dp/6130631111/)という本が最近まことしやかに囁かれているが絶対コレは酷い本に違いないので、読書会をしませんか? => 後述します
- Coqのライブラリには初等幾何をするためのものがある！
その他本当に色々
次回の内容について
Immutable Object読書会
Immutable Objectという本があります(http://www.amazon.co.jp/dp/6130631111/)
108ページで6273円(amazon.co.jp)では高過ぎるので、内容が気になるなーという人で読書会をしませんか？という話が突発的に出ました。
読書会と言っても、本を参加する人間が買う必要は無くて「1冊の本を集まって読んで、Immutable Objectについてあーだこーだ言う」という感じになっています。
ProofParty第2回に参加した人間でまず参加出来そうな人を集って、今現在
- 4/3(土曜日) 4人
- 4/10(土曜日) 5人
という事になっています。
ただ一冊の本を読む形になるので勿論少人数でなければならないわけなんですけれども、後3,4人ぐらい居てくれると楽しいんじゃないかなーというそんな感じです。
