ranha https://blog.hatena.ne.jp/ranha/ Yet Another Ranha https://ranha.hatenadiary.org/ http://atnd.org/events/29893/13日にProofPartyの第2回目がありました。今回の内容は、 「ハノイの塔では最短手数が(2^n)-1となることを証明する」 「例の採用問題でLv4になる」 の2つがメインでした。結果としては、前者がまだ書けていない、後者は既にyoshihiro503さんがCoqで証明(http://d.hatena.ne.jp/yoshihiro503/20100119)を書かれているのですが、私が今回Agda2でyoshihiro503さんの証明で言う所のSoundnessまでが書けたのでそこからは自明かなーという。個人的には、当日ついにCo… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Franha.hatenadiary.org%2Fentry%2F20100314%2F1268574468" title="ProofParty第2回目の話 - Yet Another Ranha" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2010-03-14 22:47:48 rich https://ranha.hatenadiary.org/entry/20100314/1268574468 1.0 100%