保証と要求：カリー／ハワード対応も添えて - 檜山正幸のキマイラ飼育記 (はてなBlog)

$\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\Imp}{\Rightarrow } \require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } }% \newcommand{\When}{\Keyword{When } } \newcommand{\Holds}{\Keyword{Holds } } \newcommand{\DoesHold}{\Keyword{DoesHold? } } \newcommand{\Proof}{\Keyword{Proof } }$ 文の種類に、平叙文〈declarative sentence〉や疑問文〈interrogative sentence〉などがあります。論理式で書かれるような命題は平叙文だと考えられるでしょう。では、論理式で書かれる“疑問文”はないのでしょうか？不要なのでしょうか？

命題をめぐる対話の場面では、疑問文、あるいは命令文〈imperative sentence〉に近い疑問文が必要になります。僕が実際に使っている形式的疑問文*1の書き方を紹介します。ついでに、カリー／ハワード対応で型の世界に移ったときの形式的疑問文の話もします。

この記事で述べた“疑問文”の具体的・現実的な使い方は次の記事にあります。

証明の“お膳立て”のやり方

内容：

疑問符と感嘆符
保証と要求
保証と要求の形式化
保証と要求を細かく分類する
カリー／ハワード対応と型推論

疑問符と感嘆符

AさんとBさんがいて、目の前のお皿によくわからない黒い塊がのっているとします。

Aさん「これ食べられる」
Bさん「これ食べられる」

字面の上では、二人はまったく同じことを言っています。が、二人の発言の意図は違います。末尾に一文字加えると、違いがハッキリします。

Aさん「これ食べられる?」
Bさん「これ食べられる!」

Bさんの言うことが信用できるならば、「これ食べられる!」は黒い塊が食品であることを保証しています。保証している文の末尾に感嘆符を付けることにします。この感嘆符の意味は、驚きや強調ではなくて「間違いなく食べられるぞ、安心しろ」です。保証の感嘆符が付いた文をここでは保証文〈warranty sentence〉と呼ぶことにします。

文末の疑問符は通常どおりの用法で、疑問文を表します。上のAさん／Bさんの会話は、疑問文で問いかけて保証文でこたえた*2ことになります。

保証と要求

AさんとBさんがいて、目の前に命題があるとします。

Aさん「この命題正しい?」
Bさん「この命題正しい!」

これは、前節同様、疑問文と保証文による会話です。Bさんの保証を信じてオシマイにすることもできますが、命題の正しさはその根拠を問うことができます。

Aさん「この命題正しい? 証明をみせて」

こうなると、単なる疑問文ではなくて、命令文っぽくなります。もちろん、命令調ではなくて丁寧にお願いする言い回しでもいいですよ。

Aさん「この命題正しい? 証明をみせていただけますでしょうか？」

丁寧にお願いするとやっぱり末尾に疑問符が付きますね。

いずれにしても、根拠の提示まで求める文をここでは要求文〈requirement sentence〉と呼びましょう。

Aさんの要求文に対して、Bさんは「これは証明なしに仮定する公理だから正しいんだよ！」とこたえることもできます。現実的には、次のような応答も許容しないと辛いですね。

Bさん「証明はあるんだけど長くてめんどくさいんだよなー、今はとりあえず俺の言うこと信じてくれよ、この命題正しい！」

保証と要求の形式化

$P$ が何らかの命題（を表す論理式）だとして、「 $P$ は正しい!」という保証文を次の形で書くことにします。

$\quad \vdash!\, P$

一方、「 $P$ の証明をみせていただけますでしょうか？」という要求文は次のように書きます。

$\quad \vdash?\, P$

例えば、ゴールドバッハ予想（「4以上の全ての偶数は、二つの素数の和で表すことができる。」）は次の要求文で書けます。

$\quad \vdash?\; \forall n\in {\bf N}.\,n \ge 4 \land \mrm{isEven}(n) \Imp (\exists p, q\in {\bf N}. \mrm{isPrime}(p) \land \mrm{isPrime}(q) \land p +q = n)$

これに対する保証文 $\vdash!\, \cdots$ は、今のところ誰も主張することができません。

さて、単一の命題だけでなく、幾つかの仮定のもとで成立する／しない命題も考えましょう。「仮定付きで正しい!」という保証文は次の形にします。

$\quad A_1, \cdots, A_n \vdash!\, P$

そして、「仮定付きの証明をみせていただけますでしょうか？」という要求文は次の形です。

$\quad A_1, \cdots, A_n \vdash?\, P$

実際の命題に関する保証文／要求文を書くとき、横一行に書くのは書きにくく／読みにくいので、僕は次のように書いています。

$\When x\in {\bf R}\\ \When x \ge 0\\ \When y\in {\bf R}\\ \When y \ge 0\\ \Holds x + y \ge 0$

$x\in {\bf R}$ などは、真偽を判定すべき命題というより、変数の型宣言なので、 $\For$ というキーワードを使うことにします。また、適宜まとめて書いてもいいとすると：

$\For x, y\in {\bf R}\\ \When x \ge 0, y \ge 0\\ \Holds x + y \ge 0$

これは保証文で、要求文は $\Holds$ を $\DoesHold$ に替えることにします。ゴールドバッハ予想の要求文も、仮定と結論に分けて次のように見やすく書けます。

$\For n\in {\bf N}\\ \When n \ge 4, \mrm{isEven}(n)\\ \DoesHold\\ \quad \exists p, q\in {\bf N}. \mrm{isPrime}(p) \land \mrm{isPrime}(q) \land p +q = n$

保証と要求を細かく分類する

仮定のない保証文は、仮定が0個の仮定付き保証文とみなせるので、 $n = 0$ の場合も含めて $A_1, \cdots, A_n \vdash!\, P$ の形を使いましょう（要求文のときも同様）。命題（を表すメタ変数）にラテン大文字 $A, P$ などを使いましたが、証明（を表すメタ変数）にはラテン小文字 $p$ などを使うことにします。

$A_1, \cdots, A_n \vdash!\, P$ という保証文には証明が現れません。つまりこれは「とりあえず俺の言うこと信じてくれよ、この命題正しい！」という主張です。証明をちゃんと付けた保証文は次の形にします。

$\quad A_1, \cdots, A_n \vdash!\, p:P$

ここで $p$ は証明を表しています。我々がよく使う記述では証明をステートメントの後に書くので、例えば $A, B \vdash!\, p:P$ なら次のように書くのが見やすいでしょう。

$\When A\\ \When B\\ \Holds P\\ \Proof\\ \quad p$

要求文に証明を書いたらどうでしょう？

$\quad A_1, \cdots, A_n \vdash?\, p:P$

これは、 $p$ が $A, B \vdash?\, P$ に対する“正しい証明であるかどうか”を問うていると解釈しましょう。証明検証系〈proof verifier〉というソフトウェアがあります（例えば Mizar）。証明検証系は人間が書いた形式的証明の正しさをチェックしてくれます。証明付きの要求文は、証明検証系への入力と考えれば分かりやすいでしょう*3。

今まで出てきた保証文／要求文をまとめてみると：

$A_1, \cdots, A_n \vdash!\, P$
証明は書いてない保証文。結論が $P$ になる証明が存在すると言っている。発言者が信頼できるなら保証になっている。
$A_1, \cdots, A_n \vdash!\, p:P$
証明が書いてある保証文。証明が正しいなら保証になっている。
$A_1, \cdots, A_n \vdash?\, P$
結論が $P$ である証明を要求する要求文。
$A_1, \cdots, A_n \vdash?\, p:P$
証明の正しさの検証を要求する要求文。

カリー／ハワード対応と型推論

論理の概念と型理論の概念のあいだの対応としてカリー／ハワード対応があります。その対応を大雑把に表にまとめると：

論理の概念	型理論の概念
命題	型
名前付きの命題	変数の型宣言
ある命題の証明	ある型を持つ項

命題に名前〈ラベル〉を付けたものを $a:A$ のように書くことにすると、証明付きの保証文は次のように書けます。

$\quad a_1:A_1, \cdots, a_n:A_n \vdash!\, p:P$

証明 $p$ において仮定を参照するでしょうから、 $p$ のなかには名前〈ラベル〉 $a_1, \cdots, a_n$ が登場するでしょう。

さて、 $t$ が変数 $x_1, \cdots, x_n$ を含む（かも知れない）項（式と言っても同じ）だとします。変数の型が決まっているとき、項 $t$ の型を保証する主張を次のように書きます。これも保証文です。

$\quad x_1:X_1, \cdots, x_n:X_n \vdash!\, t:Y$

前節の保証文／要求文の分類を、型と項に関する保証文／要求文に対しても適用すると次のようになります。

$x_1:X_1, \cdots, x_n:X_n \vdash!\, Y$
項は書いてない保証文。型 $Y$ の項が存在すると言っている。発言者が信頼できるなら保証になっている。
$x_1:X_1, \cdots, x_n:X_n \vdash!\, t:Y$
項が書いてある保証文。項が正しいなら保証になっている。
$x_1:X_1, \cdots, x_n:X_n \vdash?\, Y$
型が $Y$ である項を要求する要求文。
$x_1:X_1, \cdots, x_n:X_n \vdash?\, t:Y$
項とその型付け〈typing〉の正しさの検証を要求する要求文。