トップ «前の日記(2007-12-11) 最新 次の日記(2007-12-13)» 月表示 編集

日々の流転


2007-12-12 [長年日記]

λ. 「Coqで“無限オブ無限”」のyoshihiroさんによる証明

先日のCoqで“無限オブ無限”で書いたCoqのコードが題意を満たすことを、にわとり小屋でのプログラミング日記のyoshihiro503さんが証明してくれました。ありがとうございます。
Coqで”無限オブ無限”(証明部分)

これは圧巻。面倒そうだとは思っていたものの、なんと500行もの証明に。 ……自分でやらなくて正解だったかも(苦笑

Coqを知らない人はこれを見て何が何だか分からないと思うけど、CoqIDEに読み込ませてステップ実行*1させていくと、ゴールがどう変形されていくかが分かって、何をやってるかが分るはず。といっても、僕もまだ全部はとても理解できていないけど。

Tags: coq

*1 Coqは手続き型言語です;-)