型チェッカーは間違っている可能性がある – LeanとCurry-Howard対応

あなたの型チェッカーは間違っている可能性がある - 形式的証明検証とCurry-Howard対応の紹介 2026年7月25日 目次 コードを書くとき、多くの人が型チェッカーに何度も助けられてきました。これは、文字列と整数を足したり、所有値への参照ではなく値を返したりしていないことを保証してくれる便利なソフトウェアです。しかし、便利であると同時に、時には煩わしいこともありますが、謙虚な型チェッカーは、私たちの命を救うという高貴な仕事を超えて、能力が限られているようです… したがって、型チェッカーが証明支援システムのバックボーンを形成することに驚くかもしれません - LeanやCoqのような言語です。これらは、型から得られる構造を使用して、ある命題が他の命題から従うかどうか、またはより口語的には、数学的証明を検証するかどうかを確実にチェックします。 このブログでは、まずCurry-Howard対応のより基本的な要素を紹介し、次に証明支援システムでどのように使用されるか、そして最終的には、これがあなたの型チェッカーが間違っている（または単に、あなたが正しいことを知らない）可能性があることを意味する理由を説明したいと思います。 Curry-Howard対応 Curry-Howard（CH）対応の軽い定義は次のとおりです。 証明はプログラムとして表現できる （…） 証明は実行できる この定義はあまり多くを語りませんが、証明はプログラムとして表現できるとすれば、プログラムに証明を返させる方法が必要になるという考え方ができます。しかし、これはそもそも何を意味するのでしょうか？ 基本に戻ると、プログラムが整数を返すために、それは型 $ ext{int}$ を返すと私たちは言います。これは任意の整数であり得ます。したがって、$ ext{int}$ は整数の集合を表します。同様に、プログラムが $ ext{True}$ または $ ext{False}$ を返すために、それは型 $ ext{bool}$ を返すと私たちは言います。これは両方の可能性を含んでいます。型を集合として近似することは厳密には正しくありませんが、この投稿の目的には十分です。 証明にこれを拡張しようとすると、プログラムが何らかの事実の証明を返すと、それは型 $P(X)$ の要素を返すと人が言うかもしれません。ここで $P(X)$ は事実 $X$ のすべての証明の集合です。 新しい証明オブジェクトを真剣に扱うために、まず命題論理と述語論理のいくつかの論理演算を新しいパラダイムに翻訳する必要があります。最も簡単なものから始めます。 $$ X ext{ is true} $$ この場合、Xが真であるためには、Xの証明が必要になります。 $$ ext{証明 } p: p ext{ は } P(X) ext{ に属する} $$ 私たちはこれを次のように言います： $P(X)$ は満たされている3。例えば、$P(5=5)$ は満たされていますが、$P(5+2=6)$ は満たされていません（ペアノ算術ではこの証明が存在しないため、偽です）。 次に、「かつ」（$ ext{and}$、$ ext{∧}$）という論理演算子を表したいと思います。馴染みのない方のために、$X ext{ かつ } Y$ は、XとYの両方が真である場合にのみ真です。したがって、$P(X)$ と $P(Y)$ の両方が満たされている、つまり $ ext{証明 } p: p ext{ は } P(X) ext{ に属する}$ かつ $ ext{証明 } p ext{': } p ext{' は } P(Y) ext{ に属する}$ となります。これは、オブジェクト $(p, p ext{'})$ を構築できることを意味します。したがって、次のようになります。 $$ P(X) imes P(Y) $$ （ここで $ imes$ はデカルト積を表します）は満たされています（$(p, p ext{'}) ext{ は } P(X) imes P(Y) ext{ に属する}$）。 次に、含意演算子を表したいと思います。$X ext{ ならば } Y$ は、Xが偽であるか、またはXが真でYが真であるかのいずれかです。これは、$P(X)$ から $P(Y)$ への関数の存在として表されます。 $$ P(X) o P(Y) $$ この関数が存在する場合、Xの証明があるたびに、Yの証明を導き出すことができます。Xが偽の場合（したがって $P(X)$ が満たされていない場合）、関数には入力がないため、$P(Y)$ は真である場合も偽である場合もあります。 簡潔にするために、標準的な論理演算の残りの部分についての議論は省略します。それらは集合論に次のように翻訳されます（ただし、この投稿の残りの部分には関連がありません）。 論理演算子 | 集合論 ---|--- $X ext{ または } Y$ | $P(X) + P(Y)$ （ここで $+$ は非交和を表します） $(orall(n ext{ は } ext{N} ext{ に属する})X(n))$ | $(n: ext{N}) o P(X(n))$ $( ext{存在 } (n ext{ は } ext{N} ext{ に属する})X(N))$ | $(n: ext{N}) imes P(X(n))$ 4 証明支援システムはCH対応をどのように使用するか 証明支援システムは、この対応と型チェッカーを使用して証明を検証します。しかし、どのように行うのでしょうか？それを示すために、Leanの表記法を使用して簡単な定理を証明しましょう。 定理 以下の定理をブログ：1と名付けます theorem blog (X Y Z: Prop) (h_1: X) (h_2: Y) (h_3: Y → Z) : X ∧ Z これは、$X, Y, Z$ が論理命題である、つまり真であるか偽であるかのいずれかであると述べることから始まります。これは、集合 $P(X), P(Y), P(Z)$ を構築するようなものですが、まだ満たされているかどうかは述べていません。 次に、Xの証明である仮説 $h_1: X$ があります。以前の議論を思い出せば、Xの証明があることはXが真であることと同等であり、したがって $h_1: X$ は単にXが真であることを与えます。これは $h_2$ と同様ですが、$h_2$ はYの証明を与えます。 そして、最後の仮説があります。これは、無限の創造性と知性を使用して、私が $h_3$ と名付けたものです。これは型 $$ Y o Z $$ です。これは、Yの証明からZの証明を得ることができる関数があることを意味します。これは $Y ext{ ならば } Z$ と同等です（以前に議論したのと同じです）。 定理の最後の部分は、望ましい結果である $X ext{ かつ } Z$ です。これを証明するには、$P(X) imes P(Z)$ を満たすオブジェクトを構築する必要があります。これを行うには、XとZの両方の証明を構築する必要があります。 ふう、それは多くのことでしたが、定理のステートメントを理解するためだけでした😨。しかし、論理演算を集合論にマッピングするという以前の議論が、定理を型の言語から論理の世界に移すことを可能にしたことがお分かりいただけたと思います。 定理の証明 今、私たちは定理を証明するという課題に取り組んでいます…数学者には本当に休息がありません（悪魔のようです！）。 鋭い目を持つあなたは、すでに望ましい構成要素の1つを持っていることに気づいたかもしれません。私たちは、$P(X)$ と $P(Z)$ の両方を満たす要素を必要としており、$h_1$、つまりXの証明（したがって $P(X)$ を満たすのに適しています）を持っています。なんて素晴らしい成果でしょう。 次に、$P(Z)$ を示す必要があります。さて、$h_2: Y$ と、$Y$ の証明を受け取って $Z$ の証明を与える関数である $h_3$ を持っています。待ってください、それはちょうど機能します™。したがって、$Y$ の証明 ($h_2$) を $h_3$ に渡すことで、$P(Z)$ を満たす $Z$ の証明を得ることができます。 では、Leanでこれをどのように書くのでしょうか？多くの方法がありますが、その1つは次のとおりです（自分で別の方法を試して、コメントに残してください）。 私たちは、望ましい結果を、連続して埋める必要がある2つの部分に分解することから始めます。ステートメントコンストラクタを使用して、Leanに望ましい結果を達成するために何をする必要があるかを尋ねます。忠実に、Leanは2つの目標を出力します。1つは $X$ を埋めるため、もう1つは $Z$ を埋めるためです。 $X$ を埋めるために、単に $h_1$ であるとLeanに伝えることができます。正確に $h_1$ です。$Z$ を埋めるためには、$h_3$ を $h_2$ に適用する必要があります（覚えておいてください、$h_3$ は関数です）。Leanでこれを行うには、単に $h_3 h_2$ です（非関数型言語により似せるために $h_3 (h_2)$ と書くこともできます）。したがって、$z$ という変数を型 $Z$ のものとして定義します。 1 2 3 4 5 theorem blog (X Y Z: Prop) (h_1: X) (h_2: Y) (h_3: Y → Z) : X ∧ Z := by constructor exact h_1 have z: Z := h_3 (h_2) exact z Leanは「目標達成 🎉」というメッセージで私たちを祝福し、私たちは再び公の場に顔を出すことができます。完全なコードは次のとおりです。 1 2 3 4 5 theorem blog (X Y Z: Prop) (h_1: X) (h_2: Y) (h_3: Y → Z) : X ∧ Z := by constructor exact h_1 have z: Z := h_3 (h_2) exact z 型チェッカー 投稿の冒頭で、あなたの型チェッカーが間違っている可能性があると主張することを約束しました。そして今、それをします。前述のように、証明支援システムがあなたが望ましい結果を証明したことを検証するためには、あなたが提供した一連の式の各式で型を評価できる必要があります。この要件には問題があります。それは、すべての式が評価を完了することを必要とします。式が評価を完了しない方法は2つあります。 CやPythonのexit()のような、評価を完了するという要件を回避することによる、いくぶん空虚なケースですが、