『定理証明手習い』の読み方（私論）

本記事は、ラムダノートで発売している『定理証明手習い』を買っていただいた方に「読んで」とお願いするための「私家版、読み方のおすすめ」です。そもそも定理証明とか自分には関係ないしっていう人も多いと思うので、「気になるけど買ってない」という方に興味を持ってもらうことも目的としています。

「ラムダノートの本の読み方（私論）」シリーズはこれで第3回なのですが、前回からは丸1年も空いてしまいました。この間に『実践プロパティベーステスト』を出版し、プログラムの挙動を検証する本について語れることが増えたので、そのあたりの世界観自体から話を始めていきたいと思います。

テストケースを手作りして挙動を確かめる
性質からテストケースを自動生成するプロパティベーステスト
プログラムの性質を値によらず「証明」する
証明してみよう
続きは『定理証明手習い』で
現実的な効能？

テストケースを手作りして挙動を確かめる

配列を逆順にしたものが欲しいとします。

たとえばPythonであれば、配列aryを逆順にしたものはary.reverse()で得られます。スライスを使ってary[::-1]としてもいいでしょう。 reversed(ary)を使うことも考えられます。

普段、私たちがこうした便利な機能を使っているときは、単純に言語処理系の実装を信じています。そんな基本的な機能を開発している人たちがミスに気づかないとも思えないし、世界中のみんなが使っている機能で実際にこれまでバグが出ていないのだから、きっと今もこれからも正しく動作するでしょう。

しかし、もし自分の手で関数を実装するしかないとしたら、その挙動が正しいことを無邪気に信じるわけにもいきません。

ここでは例として、自然数からなる配列を逆順にする関数を次のようにして再帰的に定義したとしましょう。

def reverse(xs):
    if not xs:
        return []
    else:
        return reverse(xs[1:]) + [xs[0]]

この関数の挙動について確信するための最初の一歩は、テストケースをいくつか書いてユニットテストしてみることかもしれません。

assert reverse([]) == []
assert reverse([1]) == [1]
assert reverse([1, 2, 3, 4, 5]) == [5, 4, 3, 2, 1]

とはいえ、これっぽっちの単純な値に対する挙動を確かめるだけでは、想像もつかないような値でもこの関数が正しいかどうかは確信できませんよね。もっともっとテストケースを増やす必要があります。

しかも、できるだけ「思いもよらない値」に対するテストケースがほしい。定義した関数が、自分の想像力を越える値に対しても意図した動作をするかどうかを調べるには、自分の頭で考えたテストケースを追加していくだけではきりがなさそうです。

性質からテストケースを自動生成するプロパティベーステスト

そこでプロパティベーステストです。プロパティベーステストでは、人間はプログラムが満たすべき値ではなく性質のほうを考えて、その性質を確かめられるような値をフレームワークで機械的に大量に生成させます。性質から値を生成するのに疑似乱数を使って、十分に大量の値を生成すれば、自分の頭では想像できなかった値が含まれる可能性も高いでしょう。それらの値を使ってテストを実行することで、微妙なコーナーケースも勝手に網羅されるようにしようというわけです。

PythonにもHypothesisというプロパティベーステストのためのフレームワークがあるようなので、これを使ったプロパティベーステストの例をChatGPTに書いてもらいました。

from hypothesis import given, settings
from hypothesis.strategies import lists, integers

@given(lists(integers()))
@settings(max_examples=1000)
def test_reverse_property(xs):
    reversed_xs = reverse(xs)
    # リストが逆順になっているか？
    for i in range(len(xs)):
        print(xs)
        assert reversed_xs[i] == xs[len(xs) - i - 1]

test_reverse_property()

上記の例では、自分が定義した再帰的なreverseで試しに使ってみる値として、自然数からなるリストを生成させています。そして、生成された値を使ってみた結果が本当に逆順になっているかどうかをfor文で確認するというプログラムのようです。

これをpytestで試してみたところ、下記のような結果になりました。 pytestでは--hypothesis-show-statisticsオプションを明示しないと統計情報が出ないようなのと、Hypothesisによって生成された事例を標準出力に見るには-sオプションが必須という点でちょっとはまりましたが、とりあえず1000の値を無作為に生成することによるプロパティベーステストはできているようです。

$ pytest --hypothesis-show-statistics -s
（中略）
============================ Hypothesis Statistics =============================

test_reverse.py::test_reverse_property:

  - during reuse phase (0.00 seconds):
    - Typical runtimes: < 1ms, of which < 1ms in data generation
    - 2 passing examples, 0 failing examples, 0 invalid examples

  - during generate phase (2.73 seconds):
    - Typical runtimes: ~ 0-2 ms, of which ~ 0-2 ms in data generation
    - 998 passing examples, 0 failing examples, 24 invalid examples

  - Stopped because settings.max_examples=1000

これで自作のreverseの定義にもだいぶ確信がもてるようになりました！

さらにプロパティベーステストでは、値ではなく性質のほうを考えるという特性から、「人間がプログラムの仕様について勘違いをしてないかがわかる」という強みもあります。そうしたプロパティベーステストの発展的話題については、『実践プロパティベーステスト』という書籍でさらに高度な手法がいろいろ紹介されているので、興味がある方はそちらをぜひお求めください。いまのところ最強のプロパティベーステストフレームワークがErlang/Elixir向けのものなので、それらの言語による解説ではありますが、他の言語でもかなりのところまで実践できるようです。

プログラムの性質を値によらず「証明」する

いったん別の本の宣伝を挟んだところで、ここまでの話の要点を書き出しておきます。

ユニットテストでは、プログラムが満たすべき値を考えて、それらの値を使った結果を確認する
プロパティベーステストでは、プログラムが満たすべき性質を考えて、それに見合った値を無作為に生成し、それらの値を使った結果を確認する

このように並べて見ると、ユニットテストとプロパティベーステストでは「人間が何を考えるか」は違いますが、「値を使ってみて確かめる」という観点ではよく似ています。プログラムの挙動を確認したいのだから、いずれにしても何らかの値を使ってみて確かめることになるでしょう。

しかしプログラムによっては、値を実際に使って確認してみなくても、その性質を形式的に確信できるはずであるようなものがあります。たとえば、配列を反転させる関数であれば、値によらず「2回使うと元に戻る」という性質が満たされているべきでしょう。「2回使うと元に戻る」関数のすべてが「配列を反転させる」という動作を実現するものかどうかは別の話ですが、そのつもりで書いた関数について「2回使うと元に戻る」という事実を値によらず証明できるなら、その性質を具体的な値を使ってみることで確認するよりも、かなり強力に正しいプログラムであることが確信できます。

現物をたくさん調べて確かめるのではなく、そうした性質を数学の定理のように「証明」しようというわけです。

というわけで、ここから今日の本題である定理証明です。残念ながらPythonでは現実的にそのような芸当は（たぶん）できないので、ここからは例としてLisp系の架空のプログラミング言語を使います。

このLisp系の架空の言語では、冒頭に挙げたPythonによるreverseの再帰的な実装をそのまま引き写して、次のような関数としてリストに対するreverseが定義できるとします。

(defun reverse (xs)
  (if (atom xs)
      xs
      (cons (reverse (cdr xs)) (car xs))))

そして「任意のリストxsに対してreverseを2回使うと元に戻る」という性質は、次のような式として書けるとします。

(equal 
  (reverse (reverse xs))
  xs)

もし上式を評価した結果が、xsの値によらず't、つまり真になるなら、「任意のリストxsに対してreverseを2回使うと元に戻る」という性質が確かに検証できたことになるでしょう。これが定理証明です！

証明してみよう

前項では都合よくでっちあげた架空のLisp系言語の例を持ち出して「これが定理証明です！」と言いましたが、「そんなん言われても単なる机上の空論じゃんよ」という感じですよね。

実を言うと、前項の例ではいろいろ大事なところをごまかしています。まず、atomやcons、carやcdrといった「組み込み関数」について、何も具体的な挙動を明記していません。証明というからには、そうした細部の意味をしっかり固める必要があります。

たとえば、そうした組み込み関数にはあらゆる値に対して必ず何らかの値を返して停止するという性質（「全域性」とか「停止性」などと呼ばれます）が必要です。ふつうのLispの実装におけるcarやcdrにはこの性質がないので、SchemeやCommon Lispをそのまま使って前項のノリで定理証明をすることは実はできません。

また、reverseは再帰的に定義されているので、その性質を証明するには帰納法が必要になります。したがって、(equal (reverse (reverse xs)) xs)という単一の式によって表される性質ではなく、次のような「帰納法の主張」に変形して、この評価結果を'tにすることが証明になります。

(if (atom xs)
    (equal (reverse (reverse xs)) xs)
    (if (equal (reverse (reverse (cdr xs))) (cdr xs))
        (equal (reverse (reverse xs)) xs)
        't))

ためしに(atom xs)の場合を証明してみましょう。高校数学で数学的帰納法をやったときに「基底部」と「帰納部」に分けて証明したのを覚えている人も多いと思いますが、これはその「基底部」の証明に相当します。

上式でいうと2行めが基底部なので、見やすいようにそこだけを取り出します。これを変形していって、結果的に'tにできれば、基底部の証明完了です。

(equal (reverse (reverse xs)) xs)

まずは内側のreverseを定義で置き換えます。

(equal (reverse 
         (if (atom xs)
             xs
             (cons (reverse (cdr xs)) (cons (car xs) '()))))
       xs)

いま調べているのは基底部で、つまり(atom xs)なので、2行めのif式の条件は真です。したがってこうなります。

(equal (reverse xs) xs)

再びreverseを定義で置き換えます。

(equal (if (atom xs)
           xs
           (cons (reverse (cdr xs)) (cons (car xs) '())))
       xs)

やはり(atom xs)なので、if式の条件は真ですから、こうなります。

(equal xs xs)

これは'tなので、この場合についての証明はこれで完了です！

続きは『定理証明手習い』で

前項では、いかにも簡単そうに式変形を進めましたが、これは簡単な例だから簡単というだけで、実際にはこんな簡単にはいきません。 reverseの性質についての証明も、前項で終わりではなく、まだ「帰納部」に対する証明が残っています（前述したように、本当はさらに全域性についても証明が必要）。

改めて帰納部だけを取り出すとこんな式になっていて、いかにも手を動かして式変形するのは面倒そうですね。ミスも起きそう。

    (if (equal (reverse (reverse (cdr xs))) (cdr xs))
        (equal (reverse (reverse xs)) xs)
        't))

そこで、こうした「そこそこ複雑な主張を式変形していって'tにする」という形での証明の流れを、先生と生徒の対話を通して一歩ずつ学べる本があります。それが『定理証明手習い』です。同書では、さらに証明における式変形を機械的に支援してくれる仕組みも用意されていて、それも利用できるようになっています。いわゆる「定理証明支援系」です。定理証明支援系の実装で何が考慮されているのかを含めて、値ではなく証明によってプログラムの確からしさを検証するとはどういうことなのかを体験できるのが『定理証明手習い』が本としておもしろいところです。

現実的な効能？

証明によるプログラムの検証という、まだなじみがない人が多いであろう考え方に触れる第一歩として手に取ってほしい『定理証明手習い』ですが、これ一冊で実務に定理証明を導入できるという本でないのも事実です。ただ、それでも本書で触れられる考え方を知ることには、少なからず効能があると思います。具体的には、「証明（のようなこと）をしてみる」という選択肢を手に入れてもらうのが、本書の役割としてあるのかなと考えています。

たとえば、本記事で定義した架空のLisp系言語におけるreverseには実は重大な欠陥があって、どんなにがんばっても帰納部に対する証明が得られません。実際、ふつうのLispではこのように定義してreverseだと「2回使うと元に戻る」という性質を満たせないのです。そのため、ちゃぶ台をひっくり返すようですが、実際に手を動かしてみると証明に行き詰まります。

しかし、やはり実際に手を動かしてみるとわかりますが、証明に行き詰まる過程で「その定義のどこに問題があるか」に気が付けます。「何かが決定的におかしい」と気づけることで、より正しい実装へと舵を切れるかもしれません。本記事のreverseにおける問題は、consにより「本物のリスト」が作られるような書き方をしてしまっていることです。 Lispにおけるconsで作られるのは「本物のリスト」ではなく、コンスペアなどと呼ばれるちょっと癖のあるデータ構造なので、Pythonの配列と同じ要領でリストの再帰的な定義を雑に書くとはまるのです。

「下位の詳細がどうなっていれば証明が通るだろうか？」という観点で実装を検証すること自体が、問題を理解するうえで役に立つことはあると思っていて、そのようなアプローチのひとつとして定理証明という方法の存在を知っていることに価値があるような気がしています。個人的に『定理証明手習い』は、そのためのさらにきっかけになるような本だと考えています。

ちなみに、「正しいreverseを2回すると元に戻る」をちゃんと証明するには何が必要か気になる人は、以下の記事で今井宜洋さんによるCoqでの解説が読めます。