証明するということ[数学][言語]

http://labs.timedia.co.jp/2013/08/post-22.html

ゲーデルの証明を一つずつプログラム言語で記述してしまえばいい！
そういうことならHaskellでしょう。だってHaskellのプログラムってそのまま数学の証明みたいだもんね！
まあそんな野望を抱いて最初の1章を読み終え、さてそろそろプログラムを書くか...
とHaskellに詳しい同僚に相談してみました

「無理っすよ、Haskellは述語論理（∀とか∃とか）を表現できないですから！
Haskellに述語論理をのっけたAgdaってのがあります」

これか↓

Wikipedia - Agda

The Agda Wiki
http://wiki.portal.chalmers.se/agda/pmwiki.php

チュートリアルは、PDFで論文ちっくに書かれてある。
ざっと見た感じ、わけわからん。


定理を証明するだけなら、そういう言語がいろいろあったよな、、、、

Wikipedia - 自動定理証明

これとか。
あと、証明プログラミングっていうのも面白いネタよね。
Coqなんかはちゃんと使えると楽しいのかなあ。

それはともかく、KOMMYとは同じ会社で背中合わせの席だったことがある。
どんな言語も3日あれば使いこなせるよ、と豪語しつつ、
実際に使いこなしていた。

すげぇと感心しつつ、Haskellさえちゃんとやったことのない身としては恐怖を覚えたのでした。

嘘は良くないなあ。
Haskellいじりもしてたような記憶があるんだがw

permlink