一般のプログラマに向けて、プログラムでの定理証明について頑張って語ってみる

最近、私は、Coqなどの定理証明支援系を学び始めたりしています。

せっかく学んだので、プログラムで定理証明するというのがどういうことなのか、自分の言葉で語ってみます。
ここでは、知らない人に知ってもらうため、Coqのような定理証明用の言語ではなく、C++でやってみます。

はじめたばかりの者が書いてますので、間違いなどありましたら、コメント欄で優しく教えていただけますと幸いです。
また、今回、ボトム型と依存型については、C++で作れるのかをよく理解できていないため、触れていません。(依存積はテンプレートとdecltypeでできるのでしょうか? 依存和は? ボトム型は?)
証明ではボトム型は否定に、依存型「任意の〜」や「ある〜が存在する」に相当する重要な概念なので、心苦しいのですが、許してください。

これでC++を使って定理証明ができる、とはならないですが、雰囲気や気持ちだけでも分かってもらえればと思います。

プログラムと証明

数学の定理などを、プログラムの「型」を使って行う、という試みです。
型を使って行うというのが、どういうことかというと、

class A {
public:
    A() {}
};

class B {
public:
    A a;
    B(A a) : a(a) {}
};

class C {
public:
    B b;
    C(B b) : b(b) {}
};

ものすごく適当なコードですが。
これで、例えば、Cの型を持ったインスタンスを作るにはどうすればいいでしょうか。

• Cのインスタンスを作るには、Bのインスタンスが必要です。
• Bのインスタンスを作るには、Aのインスタンスが必要です。
• Aのインスタンスは何もなくても作ることが出来ます。

つまり、Aを作れて、AからBが作れて、BからCが作れます。
具体的には、このようにしたら作れます。

int main() {
    C c = C(B(A()));
}

ところで、数学の証明について考えてみましょう。

• Aである
• AならばBである
• BならばCである

この3つの前提が与えられているとき、Cであることを示すには、どうすればいいでしょう。

• Cであることを示すには、Bであることを示せばいいです。
• Bであることを示すには、Aであることを示せばいいです。
• Aであることは、前提として知っています。

つまり、Aが言えて、AからBが言えて、BからCが言えます。

なんとなく、上に書いたプログラムの話と似ている気がしませんか?

つまり、プログラムの型が、証明に出てくる「命題」に対応して、その型のインスタンスが、その命題の証明に対応しています。
このようにプログラムと証明とが対応する、ということが実際分かっていて、その対応を「カリー＝ハワード同型対応」といいます。
(ぐぐると、ちゃんとした定義が出てきますが、論理学に明るい人でないと、理解が難しいかと思われます。私もカリー＝ハワード同型対応をきちんと理解しているかというと、していませんが、とりあえず定理証明で遊べるレベルにはなりました)

どのような言語で定理証明ができるのか?

型を使うので、型がある言語の方がいいです。また「AならばB」は関数、といった具合に、関数を多用するので、関数をその場で作れたり引数に渡せる言語の方がいいです。
今回触れないのですが、依存型とよばれる型が重要になるため、それらをサポートしているものがいいです。

関数型言語に、そういった特徴を持ったものが多いようです。

Coqのような証明支援システムと呼ばれているものでは、証明(つまり、インスタンスを作る作業)を楽にするための工夫がいろいろとされているので、それらを使うと非常に便利です。

「かつ」、「または」

もう少しやってみましょう。
論理によく出てくる「かつ」、「または」はどのように作れるでしょう?

2つの命題、つまり2つの型の組み合わせなので、テンプレートを使います。
「AかつB」を証明するには、AとBの両方が必要なので、2変数の関数を考えます。
「AまたはB」を証明するには、AかBのどちらかがあればいいので、1変数関数を2つ用意します。

つまり、こうなります。

#include <optional>

template<class A, class B>
class And {
public:
    A a;
    B b;
    And(A a, B b) : a(a), b(b) {}
};

template<class A, class B>
class Or {
public:
    std::optional<A> a;
    std::optional<B> b;
    Or(A a) : a(a), b() {}
    Or(B b) : a(), b(b) {}
};

Andはいいと思いますが、Orがちょっとややこしいです。
C++17の機能のoptionalを使ってるので気をつけてください。

以下、適当に例題をやっていきます。

「P」と「PならばQ」から「PかつQ」を証明する

class P {
public:
    P() {}
};

class Q {
public:
    P p;
    Q(P p) : p(p) {}
};

template<class A, class B>
class And {
public:
    A a;
    B b;
    And(A a, B b) : a(a), b(b) {}
};

int main() {
    And<P, Q>(P(), Q(P()));
}

比較的簡単です。Pと、Pから作ったQをAndのコンストラクタに渡しています。

「PかつQ」ならば「PまたはQ」を証明する

これまでmain関数にベタ書きでしたが、今回は別の関数を作ることでやってみます。

「PかつQ」ならば「PまたはQ」を示したいので、
And<P, Q>を引数に受け取って、Or<P, Q>を返す関数を作ればいいですね。
P(), Q()が直接呼べるようになっていますが、今回、前提に「Pである」や「Qである」は入っていないので、証明を書く関数からそれを呼び出すのは無しにします。

#include <optional>

class P {
public:
    P() {}
};

class Q {
public:
    Q() {}
};

template<class A, class B>
class And {
public:
    A a;
    B b;
    And(A a, B b) : a(a), b(b) {}
};

template<class A, class B>
class Or {
public:
    std::optional<A> a;
    std::optional<B> b;
    Or(A a) : a(a), b() {}
    Or(B b) : a(), b(b) {}
};


Or<P, Q> proof(And<P, Q> pq)
{
    return Or<P, Q>(pq.a);
}

int main() {
    proof(And<P, Q>(P(), Q()));
}

長いけど、証明自体は1行です。
ちなみに、return Or<P, Q>(pq.a);は、return Or<P, Q>(pq.b);としても証明できます。

「PならばR」、「QならばR」、「PまたはQ」ならば「Rである」を証明する

今度も関数を作ってやってみましょう。
「PまたはQ」を、Pの場合とQの場合で場合分けすることで証明ができます。

#include <optional>

class P {
public:
    P() {}
};

class Q {
public:
    Q() {}
};

class R {
public:
    R() {}
};

R p_implies_r (P p) {
    return R();
}

R q_implies_r (Q q) {
    return R();
}

template<class A, class B>
class And {
public:
    A a;
    B b;
    And(A a, B b) : a(a), b(b) {}
};

template<class A, class B>
class Or {
public:
    std::optional<A> a;
    std::optional<B> b;
    Or(A a) : a(a), b() {}
    Or(B b) : a(), b(b) {}
};

R proof(Or<P, Q> pq)
{
    if (pq.a.has_value()) {
        return p_implies_r(pq.a.value());
    }
    else {
        return q_implies_r(pq.b.value());
    }
}

int main() {
    proof(Or<P, Q>(P()));
    proof(Or<P, Q>(Q()));
}

一応、Pの場合の証明とQの場合の証明の両方を呼んでみています。

まとめ

今回、C++を使って、プログラムで数学の証明ができる、という気分を味わえる説明を試みました。
実際のところ、C++で証明を書くことはまずなく、Coqなどの証明支援システムを使いますが、一般のプログラマに分かるよう、あえてC++でやってみました。

このような証明の仕組みを使って、数学の証明だけではなく、プログラムが意図したとおりに動くかの証明も(もちろん、何らかの仮定は必要ですが)行うことができます。
実用的なプログラムの証明を書くのが非常に難しいため、現状は証明支援システムは実際のプログラムの品質保証目的では滅多に使われていませんが、従来の単体テストのように、プログラムの妥当性をテストケースごとに示すのではなく、より包括的に示すことができる可能性があり、非常にわくわくします。