C++ × 定理証明 - squirrel_code @ ウィキ

C++ × 定理証明

last update: 2012/09/09 (Sun)

世の中には酔狂な人がいるもので，プログラミングと定理の証明が等価だと言った人がいるそうな．これを「カリー・ハワード対応」と言うらしい．カリー・ハワードさんが言ったのか，カリーさんとハワードさんが共同で発表したのか，カリーさんとハワードさんが独立に発見したけどたまたま時期が同じだったのか，詳しいことは知らないので調べておくように．

で，気になった．我等が C++ も定理証明と等価なのだろうか．等価だとしたら，我々がプログラムを作るとき，それはどのような定理を証明していることになるのだろうか．

やってみる．

まず，定理証明といったとき，これは論理学で言う形式的証明のことである．形式的証明にはいくつかの流儀があるが，そのうちの１つにヒルベルト流の形式化というのがある．ヒルベルト流の形式化では，全ての命題を「A ならば B」（これを「含意」と言う）と「A でない」（これを「否定」と言う）で表す．これを以下のように書こう．

A -> B // A ならば B
!A // A でない

さて，これに対応する C++ プログラムを考える．カリー・ハワード対応では，命題は型と対応する． 「含意」は A という型と B という型から新たな型「A -> B」を作り出す操作となる．これは C++ では template で実装できる．同様に「否定」も template で実装できる．

template <typename A, typename B>
struct then {};
template <typename A>
struct negate {};

「ならば」は英語で「then」である． 「A ならば B」は英語で「A then B」であり，C++言語で「then<A, B>」である．「でない」は英語で「not」だが，not は識別子としていろいろ問題があるので「negate」を使った．次に，ヒルベルト流の定式化では，推論規則として「A -> B であり，かつ A ならば B」を用いる．俗に言う（正しくは言わない）３段論法，ちょっとかっこよく言うと「モーダスポネンス」である．ちなみに推論規則には他に「モーダストレンス」とか「モーダスポネンストレンス」とかがある．興味があれば Go Wikipedia．

さて，カリー・ハワード対応において推論規則はプログラムに対応する．簡単には関数だと思えばよい．引数が前提条件で，返り値が結論である．つまり，モーダスポネンスは，then<A, B> と A を引数に取り，B を返す関数である．

template <typename A, typename B>
B mp(then<A, B> t, A) {}

ここで３段論法は以下のプログラムで表現される．

struct X{}
struct Y{}

int main(int argc, char * argv[])
{
    X
        p1; // 前提 X
    then<X, Y>
        p2; // 前提 X -> Y
    Y
        p3 = mp(p2, p1); // 結論 Y
}

ここでは前提を無理やり書いたため，何を証明したのか分かり難くなっているが，最後の行の p3 = ... がすなわち p3 の証明である．この証明が正しいかどうかは，コンパイルしてみればよい．コンパイラの型チェッカを通過すれば，証明は妥当である．

形式的証明では，前提をいろいろ書けばなんでも証明できてしまうが，一応「正しい」命題を「全て」生成することができる「前提」が知られている．「正しい」と「全て」を括弧でくくったあたりはいろいろとややこしいので説明は省略する．いずれにせよ，これらの前提は「公理」と呼ばれる．

// 公理1
// A -> (B -> A)
template <typename A, typename B>
then<A, then<B, A> > axiom1() {}

// 公理2
// (A -> (B -> C)) -> (A -> B) -> (A -> C)
template <typename A, typename B, typename C>
then<then<A, then<B, C> >, then<then<A, B>, then<A, C> > > axiom2() {}

// 公理3
// (!A -> !B) -> (B -> A)
template <typename A, typename B>
then<then<negate<A>, negate<B> >, then<B, A> > axiom3() {}

さて以上を使えば，世の中のいろいろな定理が証明できるはずである．手始めとして，自明な命題「A ならば A である」を証明しよう．

struct X {};

int main(int argc, char * argv[])
{
    // P1: (X -> ((X -> X) -> X)) -> ((X -> (X -> X)) -> (X -> X))
    //     なぜなら公理2で A = X, B = (X -> X), C = X
    then<then<X, then<then<X, X>, X> >, then<then<X, then<X, X> >, then<X, X> > >
        p1 = axiom2<X, then<X, X>, X>();

    // P2: X -> ((X -> X) -> X)
    //     なぜなら公理1で A = X, B = (X -> X)
    then<X, then<then<X, X>, X> >
        p2 = axiom1<X, then<X, X> >();

    // P3: (X -> (X -> X)) -> (X -> X)
    //     なぜなら P1, P2 から MP
    then<then<X, then<X, X> >, then<X, X> >
        p3 = mp(p1, p2);

    // P4: X -> (X -> X)
    //     なぜなら公理1で A = X, B = X
    then<X, then<X, X> >
        p4 = axiom1<X, X>();
    
    // P5: X -> X
    // なぜなら P3, P4 から MP （結論）
    then<X, X>
        p5 = mp(p3, p4);
}

コンパイルちゃんと通るぜ．

&trackback()

---

参考

• C++でMix-inもどき

---

コメント

• コメントの投稿テスト -- (tossy_squirrel) 2010-12-29 03:35:18

---

関連ページ

• トップページ

---

関連ブログ

#blogsearch