停止性問題から「バグのないプログラムは存在しない」（あるいは「プログラムにバグの無いことは証明できない」）と良く言われますが、
Coqによる証明駆動開発
http://d.hatena.ne.jp/mzp/20110228/ruby
ではプログラムを証明できるみたいですが、これは冒頭の１文が可能ということでしょうか？
あと、
「カリー･ハワード同型対応」
について教えて下さい。
興味を持っていただけたようで、とても嬉しいです。
具体的な例で説明しますと、ソクラテスさんを殺すことで有名な三段論法を命題論理で書くと
(A->B) -> (B -> C) -> A -> C
となります。
で、これが真であることを証明するには、
の2つの方法があります。
このように、推論規則を用いた証明と関数の実装が対応するのがカリー・ハワード同型です。
ただ、「だからどうした?」と言われるとボクにはうまく答えれません。せいぜい「型チェックモジュールを再利用して証明チェックもできて嬉しいよね」ぐらいしか答えれません。
Coqというのは仕様の記述もできて、プログラムも組める言語なのでしょうか？
についてですが、簡単に答えるとyesです。
ボクの認識では仕様は「どのような性質を持つか」を記述したもので、プログラムは「どのようにそれを実現するか」を記述したものです。
http://d.hatena.ne.jp/yoshihiro503/20090923/p1 の例だと、「mergesortの結果はソートされている」という仕様を表現するためにSortedという述語を使っています。 Sortedはどのような性質をもつべきかは定義されていますが、どのようにそれを実現するかは定義されていません。
一方、プログラムはmergesort関数ですが、こちらは「どのように実行するか」は定義されていますが、どのような性質を満すかは定義されていません。
最後に、mergesort_sorted定理を証明することで、プログラムが仕様を満すことを証明しています。
このようにCoqでは仕様とプログラムの両方を記述して、プログラムが仕様を満すことを証明できます。
無理だと思うな。
一般的に、仕様を出す側と実装する側が分かれているとして、バグ（仕様を出す側の期待通りに動いてくれない）の原因として、以下のようになると思う。
「Coqによる証明駆動開発」は、面白いと思うけど、仕様から「証明」を正しく導き出せている、という証明ができない。
従来の「仕様の誤解」によるバグと同列。
また、「その他」の中には、コンパイラやスクリプトエンジンのバグによる、というものもあるので、それも、証明駆動では解決できない。
「証明が正しいとしたら」という前提を置くなら、従来の手法でも、「テストケースが正しいとしたら」という前提を置くのと、何ら変わりが無いので、証明駆動だからどうだか、ということにはならない。
テスト駆動との比較も、多分に、恣意的な感じが否めない。
テスト駆動を正しく理解している人が、BASE64 の実装をするときに、ランダムに抽出したデータの確認だけで済ませるはずがない。
実装しようとしている対象の領域によっては、テスト駆動に比べて、楽に必要十分なテストができます、というふうに読むなら、同意できるかな、という感じ。
仮に、「ひとつでもバグが無いプログラムを作成できるなら、バグが無いプログラムを作ることは可能である」として、コンパイラのバグも考えないとしたなら、
「Hello world」級のプログラムなら、従来の手法でも、バグが無いプログラムを作れることになりますよね。
「カリー･ハワード同型対応」については、「論理の哲学」って本を読んでみたことはあるんだけど、僕には難し過ぎて、よく分からない。
他の人に解説を譲ります :-)
ありがとうございます。
「カリー･ハワード同型対応」は
http://www.at-akada.org/blog/2008/12/post-275.html
「論理学の証明と関数型言語のプログラムが一対一対応する」
これにより、論理学の方で証明しておけば、必然的にプログラムの方も証明されるということらしいですが、今ひとつどう対応するのか良くわからないので、どなたか教えていただきたいです。
リンク先の以下の話も面白いです。
関数型言語にcall/ccを加えると古典論理になるらしい。call/ccって背理法だったらしいぞ！なんだってー！！
(ちょっと調べるとcall/ccの方が広いみたいだけど)。
つまりあれだ、二重否定除去とか背理法とかうさんくさいから止めて直観主義論理でいこうというのは「call/ccとか黒魔術だから使うのやめよう」というのに相当する(たぶん)。
無理
http://d.hatena.ne.jp/yoshihiro503/20090923/p1
この例だと、証明の仕方が正しいかどうかの検証はしてない。
カリー・ハワードの対応（Curry-Howard correspondence）に関しては以下が簡潔に説明してます。
ありがとうございます。
２番目のリンク先分かりやすいです。
ただ、やはり
型が論理式（命題）にあたるとすれば，その型を持つ式（プログラム）は何にあたるのだろうか？ 実は，「式」は「型」が表す命題の証明とみなすことができる
というあたりから分からなくなってきます。
例えばCoqが有名で，グラフ理論の四色定理やCコンパイラの正しさなど，様々な性質が厳密に検証されている。
「Cコンパイラの正しさ」の確認と「バグの有無」はどういう関係にあるのかと、定理証明器でなぜプログラムが正しいことが証明できるのかがよく分からないです。(Coqでやる証明とプログラムの関係？）
リンク先の人間です。
「証明駆動でバグがなくせる!」はわりとFUDで、実際はある種のバグを潰せるだけです。
証明駆動でやっているのは
の3つです。
2.のおかげで仕様同士の矛盾を排除でき、3.のおかげで仕様と実装の食い違いを排除できます。ですので、Coqを使うことで「矛盾する仕様に起因するバグ」と「仕様と実装の食い違いによるバグ」を排除できます。もちろん仕様の誤解や、要件と仕様の食い違いなどには太刀打ちできません。
あと、Coq自体にバグが含まれる可能性は否定できませんが、小さくて枯れたコア部分 + その上に構築された便利な機能という構成なっているので、致命的なバグが含まれる可能性は低いはずです。
mzpさん、こんにちは。
「Coq to Rubyで初める証明駆動開発」の記事興味深く拝見させて頂きました。
全てのバグを無くすことが不可能だとしても、
「ある条件(前提下)の元で○○のバグを無くすことができる」
というのはとても興味があったので、質問してみました。
質問自体は「（全ての）バグの無いプログラムを作ることは可能ですか？」と読めて、
「無理」という回答が多いと思いますが、
実際にはCoqによる証明駆動開発というのはどんなのだろうと思い質問してみました。
良くわからないのは「論理学の証明と関数型言語のプログラムが一対一対応する」
というイメージと、
>仕様と実装をCoqで記述する
>仕様が満すべき性質を証明する
>実装が仕様を満すことを証明する
上記がどのように行われるのかです。
Coqというのは仕様の記述もできて、プログラムも組める言語なのでしょうか？
宜しければまた教えてください。
興味を持っていただけたようで、とても嬉しいです。
具体的な例で説明しますと、ソクラテスさんを殺すことで有名な三段論法を命題論理で書くと
(A->B) -> (B -> C) -> A -> C
となります。
で、これが真であることを証明するには、
の2つの方法があります。
このように、推論規則を用いた証明と関数の実装が対応するのがカリー・ハワード同型です。
ただ、「だからどうした?」と言われるとボクにはうまく答えれません。せいぜい「型チェックモジュールを再利用して証明チェックもできて嬉しいよね」ぐらいしか答えれません。
Coqというのは仕様の記述もできて、プログラムも組める言語なのでしょうか？
についてですが、簡単に答えるとyesです。
ボクの認識では仕様は「どのような性質を持つか」を記述したもので、プログラムは「どのようにそれを実現するか」を記述したものです。
http://d.hatena.ne.jp/yoshihiro503/20090923/p1 の例だと、「mergesortの結果はソートされている」という仕様を表現するためにSortedという述語を使っています。 Sortedはどのような性質をもつべきかは定義されていますが、どのようにそれを実現するかは定義されていません。
一方、プログラムはmergesort関数ですが、こちらは「どのように実行するか」は定義されていますが、どのような性質を満すかは定義されていません。
最後に、mergesort_sorted定理を証明することで、プログラムが仕様を満すことを証明しています。
このようにCoqでは仕様とプログラムの両方を記述して、プログラムが仕様を満すことを証明できます。
mzpさん、こんにちは。ありがとうございます。
('a -> 'b) -> ('b -> 'c) -> 'a -> 'cという型を持つ関数が存在することを示す(= 実装してみる)
->が関数だとすると
f(a)=b
g(b)=c
h(f(a))=g(b)=c
合成関数が存在することと三段論法は同じことでしょうか？
関数がカリー化されている言語なら理論上は可能です。
カリー化を利用すると、複数の引数をとる関数を、一つの引数のみを取る複数の関数のラムダ計算などの単純な理論的モデルと見なして研究できるようになる
http://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%E5%8C%9...
ありがとうございます。
そのバグをチェックするためのプログラムでさえバグが無いという保障はないので、完全にバグのないプログラムはできません。世界中に存在するウィルスと同じように、誰しもが完全に「存在しない」「撲滅した」とは言い切れないのです。あくまでも「発見されなくなった」程度のことしか言えないものです。
プログラムならば、簡単にアラートメッセージくらいの内容を一文(JavaScriptで言えば「alert("文")」)。というくらいのプログラムなら「ミスはない」などと言えるでしょう。しかし、何行、何十行、何百行となるとたとえ一行一行チェックしたとしても、完全な意味で「バグはない」とは言えません(細部の不具合はほとんどコンピュータ画面上にエラーを出さないほど無視されるものです)。何十年以上かけてデバッグしたとしても完全にバグは取り除かれたという保障は存在しません。
「カリー･ハワード同型対応」やCoqに関してもリンク先を参照の上でご回答願いたく。
それははっきり言って無理。
wikipediaにも書いてあるよ
不適切な解答にチェックを入れました。
「カリー･ハワード同型対応」やCoqに関してもリンク先を参照の上でご回答願いたく
mzpさん、こんにちは。ありがとうございます。
->が関数だとすると
f(a)=b
g(b)=c
h(f(a))=g(b)=c
合成関数が存在することと三段論法は同じことでしょうか？