「証明支援系がダメだった理由と、AIでブーストする理由 // 人間可読証明」において次のように書きました。
人類がテキスト言語から絵図言語に乗り換えられないのは、文字・活字・組版文化の歴史的惰性だと思いますが、このような歴史的惰性を変化させるのは5年10年では無理でしょう。絵図的には簡単なことを、テキストに引き写しては難読化させるという不毛な作業を、まだしばらくは続けることになりそうです
多次元的な構造を潰して1次元の文字列にしては人々に困惑と苦痛を与えるって、ほんとに不毛で無意味で莫大な損失をもたらすわけだけど、現状においては、絵図〈ダイアグラム | ピクチャー〉を生成・交換・共有・保存するツール・環境が整備されてないので、いかんともし難いです。
せめて、紙と鉛筆を使う場合、あるいは頭のなかに形式証明を思い描くときは絵図が使えるように、説明を加えます。$`\newcommand{\Imp}{ \Rightarrow }
\newcommand{\hyp}{ \text{-} }
\newcommand{\ent}{ \mathrel{\triangleright\!\!\longrightarrow} } % entails
`$
内容:
- 追記・補足の記事: 自然言語混じり形式証明の意味論
シリーズ・ハブ記事:
カリー/ハワード/ランベック対応と複圏・多圏
我々がバックボーンとする考え方はカリー/ハワード/ランベック対応〈Curry-Howard-Lambek correspondence〉です。つまり、型付きラムダ計算と論理とモノイド閉圏(特にデカルト閉圏)は同じものだという発想・観点です。カリー/ハワード/ランベック対応については次の過去記事とそこから参照されている記事群を見てください。
概念的には同じことを、分野ごとに違う言葉/違う書き方で表現しているだけなのです。とはいえ、「違う言葉/違う書き方で表現している」ことを相互翻訳するのは至難のワザです。「「プログラミング = 証明」のはずだが」より引用:
関数型プログラミングと形式的証明では、記述言語や背景理論で使っている用語や記号があまりにも違うので、翻訳が難しい。
分野・コミュニティ間の文化・言語・習慣・関心ごと・視点の違いが、高い壁となって立ちはだかります。この壁は、僕は無意味でロクデモナイものだとみなしていますが、なかなか打ち崩せない。
例えば、論理では、「関数、定理、推論規則」は別ものとして教わりますが、証明支援系付きプログラミング言語Lean 4では、「関数、定理、推論規則」は同じものです。シンタックスシュガーや別名として異なるキーワード(例えば def
とtheorem
)も使えますが、意味論と実装メカニズムからは同じものです。
このような、「別ものか同じものか?」のような食い違いも実は表層的なもので、違う言葉/違う書き方を使っていることに起因します。抽象化・概念化すれば、食い違いは解消します。
証明や計算はテキストにエンコードされますが、分野ごとのテキスト・エンコード法の大きな違いが、“高い壁”をもたらしています。共通の絵図〈ダイアグラム | ピクチャー〉で描くことは、壁を崩す一手段となります。図示法としてはストリング図が標準的であり、ストリング図は(単なる圏よりむしろ)複圏〈multicategory〉/多圏〈polycategory〉の射の視覚的表現です。複圏/多圏については、次の記事に(述語論理との関係から)まとめてあります。
次節で具体例を出して説明を続けます。
形式証明のストリング図
次の図は、「証明支援系がダメだった理由と、AIでブーストする理由 // 人間可読証明」で出した、形式証明を表すストリング図です。
この図をテキストにエンコードするときや、地の文で説明するときは矢印記号を使います。そのとき、「何をどの矢印記号で表すか」が分野ごと・コミュニティごとに違っていてシンドイ。以下の記事に嘆きや対処法があります。
「そんな他愛もないことで」と思われるかも知れませんが、いやいやいや、深刻! 伝達やコミュニケーションにおいて行き違い・誤解・困惑・混乱が頻繁に発生して、ほとほと困っています。
この記事では、圏/複圏/多圏のプロファイル記述(後述)に、「自然言語前提の証明記述でも形式的枠組みは必要」で出した特殊な矢印 $`\mathrel{\triangleright\!\!\longrightarrow}`$ を使います。以下の表の折衷案を使う、ということです。
$`\text{型理論}`$ | $`\text{論理}`$ | $`\text{圏論}`$ | $`\text{折衷案}`$ |
$`\to`$ | $`\Rightarrow`$ | $`[\hyp, \hyp]`$ | $`\to, \Imp`$ |
$`\vdash`$ | $`\to`$ | $`\to`$ | $`\ent`$ |
$`\vdash`$ | $`\vdash`$ |
さて、本節冒頭のストリング図は、全体として多射(多圏の射)*1を表します。多射は、複数の入力と複数の出力を持つ“関数のようなもの”と思ってください。「複数」のなかには「一つだけ」も「何もない」も含まれることに注意してください。多射のプロファイルとは、複数かもしれない入出力の型の仕様です。上の事例のプロファイルは次のように書けます。
$`\quad (P, Q) \ent (P\land (Q \land P))`$
混乱の心配がなければ外側の括弧は省略してもかまいません。
$`\quad P, Q \ent P\land (Q \land P)`$
水色で描いたマルもそれぞれが多射で次のようなプロファイルを持ちます。
- $`\text{copy} : P, Q \ent P, Q, P, Q`$
- $`\text{proj1} : P, Q \ent P`$
- $`\text{swap} : P, Q \ent Q, P`$
- $`\text{AND} : Q, P \ent Q\land P`$
- $`\text{AND} : P, Q\land P \ent P\land (Q\land P)`$
ここで、$`\text{AND}`$ が二箇所で出てきますが、実は違うものです。定理や推論規則は“関数のようなもの”ですが、より正確に言えば“総称関数のようなもの”です。そして、命題は“型のようなもの”なので、総称関数のようなものである推論規則は、命題パラメータ(総称の型パラメータ相当)を持つのです。命題パラメータを下付きで表すと:
- $`\text{copy}_{P, Q} : P, Q \ent P, Q, P, Q`$
- $`\text{proj1}_{P, Q} : P, Q \ent P`$
- $`\text{swap}_{P, Q} : P, Q \ent Q, P`$
- $`\text{AND}_{Q, P} : Q, P \ent Q\land P`$
- $`\text{AND}_{P, Q\land P} : P, Q\land P \ent P\land (Q\land P)`$
水色のマルである基本関数(のようなもの)をポイントフリースタイルで組み合わせて全体を構成すれば:
$`\quad \text{copy}_{P, Q} \,;
(\text{proj1}_{P, Q} \otimes \text{swap}_{P, Q}) \,;
(\mathrm{id}_P \otimes \text{AND}_{Q, P}) \, ;
\text{AND}_{P, Q\land P}`$
ここで、セミコロンは図における縦方向のワイヤー接続で、テンソル積記号(otimes)は図における横方向の併置です。組み合わせた結果である多射のプロファイルが、
$`\quad P, Q \ent P\land (Q \land P)`$
だったのです。
変数名・ラベルの利用
前節で、「定理や推論規則は“関数のようなもの”」「命題は“型のようなもの”」と言いましたが、もっと端的に言えば、定理や推論規則は関数で、命題は型です。カリー/ハワード/ランベック対応から言えば、関数を「定理、推論規則」と呼び、型を「命題」と呼ぶのは、単に論理の習慣に過ぎないのです。他の分野・他のコミュニティはまた別な呼び方をするでしょう(同じものを)。
多射を描いたストリング図のテキスト・エンコードとして、前節ではポイントフリースタイルを使いました。ポイントフリースタイルとは、変数を使わない表現スタイルです。が、変数を使った式のほうがよく使われていますから、変数使用スタイルのエンコードもやっておきましょう。
命題は型なので、$`x: P`$ のようなラベル付き命題は、変数の型宣言 $`x: {\bf R}`$ と同じです。変数名・ラベルの絵図的解釈は二種類準備しておくといいでしょう。
1つ目の解釈は、変数名・ラベルはノードのポート(詳細は「ストリング図のテキスト化: ボックス&ポート方式」参照)の場所を識別する目印です。
2つ目の解釈は、入力を持たないノードの名前です。入力を持たないノード(三角で描いている)は、集合・型なら要素、命題なら証拠(仮定を持たない証明)と解釈できます。
これら2つの解釈は、状況に応じて使い分けてください。
ラベルを型〈命題〉の別名と解釈しがちですが、それは違います。例えば、2変数関数の記述
$`\quad x:{\bf R}, y:{\bf R} \mapsto x^2 + y^2 \;: {\bf R}`$
に出現するラベル(変数名)$`x, y`$ が実数型(実数全体の集合)の別名とは思わないですよね。変数名・ラベルは型(命題も型)の別名ではないです。
変数名・ラベルの現実的な用途は、ワイヤーを繋ぐときに、どことどこを繋ぐかを指示するための参照名としてです。ゆびさしで「こことあそこを繋ぐ」とはやれないので、場所の名前が必要になります。
変数使用スタイルは、ポイントフリースタイルに比べて便利な面があります。より具体的であり、コピー、スワップ、破棄などを明示する必要がなくなります。次節で具体的にやってみます。
ラベル利用の事例
先程のストリング図のワイヤー(あるいはポート)にオレンジ色のラベルを付けると以下の図になります。本来、すべての場所に異なるラベルを付けるべきですが、一部は重複した名前を使用しています。
水色のマルのプロファイルをラベル付きで書くと次のようになります。
- $`\text{copy} : (x:P, y:Q) \ent (x:P, y: Q, x': P, y': Q)`$
- $`\text{proj1} : (x: P, y: Q) \ent x: P`$
- $`\text{swap} : (x':P, y':Q ) \ent (y':Q, x':P)`$
- $`\text{AND} : (y':Q, x':P ) \ent z: Q\land P`$
- $`\text{AND} : (x: P, z: Q\land P) \ent P\land (Q\land P)`$
これらを律儀に代入文にエンコードすると:
$`\quad\text{let } (x, y, x', y') := \text{copy}( x, y)\\
\quad\text{let } x := \text{proj1}( x, y)\\
\quad\text{let } (y', x') := \text{swap}( x', y')\\
\quad\text{let } z := \text{AND}(y', x')\\
\quad\text{in } \text{AND}(x, z)`$
もちろん、これは簡略化できて:
$`\quad \text{AND}(x, \text{AND}(y, x) )`$
コピー、スワップ、破棄は、明示的に呼び出さなくてもラベル〈変数名〉の出現パターンで表現できます。
前節で「定理や推論規則は関数、命題は型」と言いました。また、最初の節で「共通の絵図〈ダイアグラム | ピクチャー〉で描くことは、壁を崩す一手段」とも言いました。これがどういうことか具定例で説明しましょう。
命題 $`P, Q`$ を実数型 $`{\bf R}`$ に、論理And $`\land`$ を直積 $`\times`$ に、推論規則 $`\text{AND}`$ をペアを作る関数 $`\text{pair}`$ に置き換えてみます。ペアは $`\langle\,,\,\rangle`$ で示します。
$`\quad \text{pair}_{X, Y} : (s: X, t:Y) \ent \langle s, t \rangle : X\times Y`$
基本関数のプロファイルは次のようになります。
- $`\text{copy} : (x:{\bf R}, y:{\bf R}) \ent (x:{\bf R}, y: {\bf R}, x': {\bf R}, y': {\bf R})`$
- $`\text{proj1} : (x: {\bf R}, y: {\bf R}) \ent x: {\bf R}`$
- $`\text{swap} : (x':{\bf R}, y':{\bf R} )\ent (y':{\bf R}, x':{\bf R})`$
- $`\text{pair} : (y':{\bf R}, x':{\bf R}) \ent z: {\bf R}\times {\bf R}`$
- $`\text{pair} : (x: {\bf R}, z: {\bf R}\times {\bf R} ) \ent {\bf R}\times ({\bf R}\times {\bf R})`$
これらを律儀に代入文にエンコードすると:
$`\quad\text{let } (x, y, x', y') := \text{copy}( x, y)\\
\quad\text{let } x := \text{proj1}( x, y)\\
\quad\text{let } (y', x') := \text{swap}( x', y')\\
\quad\text{let } z := \text{pair}(y', x')\\
\quad\text{in } \text{pair}(x, z)`$
もちろん、これは簡略化できて:
$`\quad \text{pair}(x, \text{pair}(y, x) ) = \langle x, \langle y, x\rangle \rangle`$
証明と計算で同じことしてます。概念的には同じことを、分野ごとに違う言葉/違う書き方で表現しているだけなのです。
ノードとコネクター
最後に、表題にあるノードとコネクターについて説明します。
圏(普通の圏)/複圏/多圏の射をストリング図に描くと、それはノードになります。ノードは単なる点ではなくて、ワイヤーを繋ぐポートを持ったデバイスだと思ってください。変数名・ラベルは、ポートまたはポートにつながったワイヤーに付けられた目印です。変数名・ラベルは場所の識別が目的であり、ワイヤーの型とは全然違います。型は、圏/複圏/多圏の対象です。
ノード達はワイヤーで繋がれるのですが、コピー、スワップ、破棄とワイヤリングのひとまとまりをコネクター〈connector〉と呼ぶことにします。次の図を例に説明します。
ノード=射 のプロファイルは:
- $`f:A \ent B`$
- $`g: B, C \ent D`$
これらを組み合わせて青いノードが作られ、青いノードのプロファイルは:
$`\quad A, C \ent B, D`$
組み合わせ方をポイントフリースタイルで書けば:
$`\quad (f \,; \Delta_B) \,{_2;_1}\, g`$
ここで、$`\Delta_B`$ はコピーで、$`{_2;_1}`$ は多射の結合演算で「2番目の出力ワイヤーを1番目の入力ワイヤーに繋ぐ」ことです。
この組み合わせ方における $`;\Delta_B \,{_2;_1}`$ の部分をオレンジ色で描いています。オレンジ色の部分を実体的な部品と考えてコネクターと呼ぼう、ということです。コネクターを実体的に扱うことにより、複雑なワイヤリング作業をモジュラー化〈modularization〉できます。
自然言語証明や、半形式証明の自然言語ヒント/キューを形式化してみると、コネクターの情報が省略・暗黙化されている場合が多いのが分かります。逆に言えば、自然言語証明や半形式証明から形式証明へのコンパイル〈トランスパイル〉では、省略・暗黙化されたコネクターの再現が肝になります。
- 追記・補足の記事: 自然言語混じり形式証明の意味論
*1:多射は、polycategory の morphism なので polymorphism ですが、多相の意味のポリモーフィズムとかぶってしまうので、polyarrow とか polymap とか呼びます。日本語なら「多相」とのコンフリクトは起きないので「多射」を使います。