前回の記事「近未来の証明ソフトウェアは‥‥」で、次のように書きました。
もう楽観的な気分にはなりにくいのですが、自然言語で対話できるAIが評判になっているご時世だし、「2年後にはグランディ／センタのサンプルをそのまま理解する証明ソフトウェアが実現する」と予測しておきましょう。まー、予測っつうより“願い”ですけど。
2年後にはこうなっているといいな、という僕の“願い”をもう少し具体的に書いておきます。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\calc}{\Keyword{calc } }
\newcommand{\endcalc}{\Keyword{end } }
\newcommand{\theorem}{\Keyword{theorem } }
\newcommand{\context}{\Keyword{context } }
\newcommand{\par}{\Keyword{par } }
\newcommand{\endpar}{\Keyword{end } }
\newcommand{\curs}{ \textcolor{orange}{\blacksquare} }
`$
内容：
タクティクから人間可読証明へ
現在主流のタクティク証明（「タクティク」と呼ばれる独特なコマンドを駆使する）は、機械〈ソフトウェア〉には向いてますが、人間が読めないので、人間に対するプレゼンテーションには使えません。人間可読な形式として、「近未来の証明ソフトウェアは‥‥」で紹介した運算的証明フォーマットは有望な選択肢です。どんな証明でも運算的に書けるわけではないですが、守備範囲はけっこう広そうです。
現在の証明支援系ソフトウェアは、タクティク証明は支援してくれますが、タクティク以外の証明は支援してくれません。シンタックスハイライトやインテリセンス〈コンプリーション〉はありますが、それはコーディング全般に対する一般的支援で、証明特有の支援ではありません。
タクティク証明はバックワード・リーズニング（「フォワード・リーズニングとバックワード・リーズニング」参照）であり、バックワード・リーズニングであることがソフトウェアによる支援を容易にしています。しかしだからと言って：
- バックワード・リーズニングがタクティクでしか書けないわけではない。
- フォワード・リーズニングだからといってソフトウェア支援ができないわけではない。
実際、運算的証明フォーマットでバックワード・リーズニングも書けます。フォワード・リーズニングの際にもソフトウェアに助けて欲しいことは色々あります。
運算的証明フォーマットとソフトウェア支援
「近未来の証明ソフトウェアは‥‥」で引用したグランディ／センタのサンプルを再掲します。
$`\theorem \text{sample } (k : \mrm{Nat}) : \mrm{even}\; ( k^3 + k) :=\\
\calc \\
\mrm{even} ( k^3 + k)\\
\updownarrow //\text{ Extract the common factor.}\\
\mrm{even} (k\cdot (k^2 + 1) ) \\
\updownarrow //\text{ Distribute even over }\cdot \text{ .}\\
\mrm{even}(k) \lor \mrm{even}(k^2 + 1) \\
\updownarrow //\text{ Simplify the right disjunct.}\\
\quad \calc \\
\quad \text{... 省略}\\
\quad \endcalc\\
\mrm{even}(k) \lor \lnot\mrm{even}(k)\\
\updownarrow //\text{ The law of the excluded middle.}\\
\top\\
\endcalc`$
運算的証明の書き方を少し変更します。
$`\calc`$の横に、証明すべきステートメントを書いてしまうことにします。証明の前提となるコンテキストは別に書きます。
$`\context (k : \mrm{Nat})\\
\calc \mrm{even}( k^3 + k) \leftrightarrow \top \\
\text{... 省略}
`$
グランディ／センタのサンプルは両方向の〈bidirectional〉リーズニングだったので $`\leftrightarrow`$ を使いましたが、バックワード・リーズニングなら $`\leftarrow`$、フォワード・リーズニングなら $`\rightarrow`$ で書くことにします。
自然言語による証明のヒントはコメントとして書きましたが、近未来の証明ソフトウェアは統制・制限された自然言語〈controlled natural language〉は理解できるはずなので、自然言語によるヒントはコメントではなくて証明ソースコードの一部とします。ソフトウェアに無視して欲しい文言だけをコメントとします。
$`\context (k : \mrm{Nat})\\
\calc \mrm{even}( k^3 + k) \leftrightarrow \top \\
\text{// calculational proof start.}\\
\updownarrow \text{ Extract the common factor.}\\
\mrm{even} (k\cdot (k^2 + 1) ) \text{ // (1) }\\
\text{... 省略}
`$
ソフトウェアは、"Extract the common factor." という自然言語とその他の記述を理解して、次の2つの証明要求〈証明責務 | ゴール〉を裏側で生成します。
- $`(k : \mrm{Nat}), \mrm{even}( k^3 + k) \vdash?\: \mrm{even} (k\cdot (k^2 + 1) )`$
- $`(k : \mrm{Nat}), \mrm{even} (k\cdot (k^2 + 1) ) \vdash?\: \mrm{even}( k^3 + k)`$
これらの証明要求はユーザーの手を煩わせずに解決して、$`\text{ // (1) }`$ の行まで書いた段階で、次の2つの証明判断（証明可能性を主張するメタ命題）が成立している状態になります。
- $`(k : \mrm{Nat}), \mrm{even}( k^3 + k) \vdash \mrm{even} (k\cdot (k^2 + 1) )`$
- $`(k : \mrm{Nat}), \mrm{even} (k\cdot (k^2 + 1) ) \vdash \mrm{even}( k^3 + k)`$
ユーザーから要求があれば、内部的に自動生成した証明の説明〈explanation〉を人間可読形式で表示します。ときにはユーザーが「おまえ、何したの？」と訝しく思うでしょうから。
証明のお膳立てのソフトウェア支援
「証明の“お膳立て”のやり方」シリーズで述べた“証明のお膳立て”をソフトウェアがどのように支援できるかを考えてみます。
$`\Gamma`$ はコンテキスト、$`A, B`$ は命題（を表す論理式）とします。$`\curs`$ はエディタのカーソル位置を表します。エディタが次の状況だとしましょう。
$`\context \Gamma\\
\calc A \land B \leftarrow\\
\uparrow \text{ 論理アンドを分解する}\curs
`$
$`\leftarrow`$ や $`\uparrow`$ から、ユーザーがバックワード・リーズニングをしようとしているのは読み取れます。この状態で[Enter]キーを押すと、エディタとバックエンドの証明支援サーバーは次の状態を作ります。
$`\context \Gamma\\
\calc A \land B \leftarrow\\
\uparrow \text{ 論理アンドを分解する}\\
\par \\
\quad \calc A \leftarrow\\
\quad \curs\\
\quad \endcalc\\
\quad \calc B \leftarrow\\
\quad \endcalc\\
\endpar \text{ // par の終わり}\\
\endcalc \text{ // calc の終わり}
`$
ソフトウェアは、自然言語「論理アンドを分解する」を理解して、すぐ下に証明のテンプレート〈スニペット〉を挿入して、カーソルを適切な位置まで移動します。ここで、$`\par`$ は"parallel"の略記で、複数のサブ証明が並行した構造を表します。
全称命題の証明の場合も同様な支援ができます。$`P`$ は述語（を表す論理式）だとします。
$`\context \Gamma\\
\calc \forall x\in X. P(x) \leftarrow\\
\uparrow \text{ 全称記号を外す}\curs
`$
[Enter]キーで次の状態になります。
$`\context \Gamma\\
\calc \forall x\in X. P(x) \leftarrow\\
\uparrow \text{ 全称記号を外す}\\
\quad \context (x\in X)\\
\quad \calc P(x) \leftarrow\\
\quad \curs\\
\quad \endcalc\\
\endcalc
`$
ユーザーとソフトウェアが協力して $`P(x)`$ の証明を書けば、次の証明判断が成立している状態になります。
- $`\Gamma, (x\in X) \vdash P(x)`$
全称導入の推論規則は自動的に適用されて、次が得られます。
- $`\Gamma \vdash \forall x\in X.P(x)`$
人間にとって何が負担なのか
タクティク証明では、独特なコマンド達とその使い方を憶えて慣れる必要があります。しかし、頑張ってタクティク証明を書いても他の人が読めるものではありません。リーズニングの方法（バックワードのみ）も記述（コマンド・スクリプト）も、教科書や論文にある証明とはまったく違うものです。
タクティクであれ直接証明であれ、証明で使う定理をライブラリやパッケージから探すのはホントに大変です。定理検索こそ、チャット方式AIに代行して欲しい作業です。
定理、公理、定義、関数などの、証明ソースコード内での正確な名前（例えば、自然数の掛け算の結合法則ならNat.mul_assoc）をすべて憶えるなんてことは人間には不可能です。人間には当たり前だと思える命題（例えば、k^2 = k*k）の詳細な証明を強いられるのは苦痛以外のなにものでもありません。
タクティク証明以外では、ありきたりのコーディング・サポートしか提供されてないのはときに腹立たしくなります。「もう少し手伝ってくれよぉ」と。
2年後には、これらの負担とストレスが解消されることを願っています。
