数学的証明とコンピュータ プログラムを同一視するディープ リンク | クアンタマガジン

一部の科学的発見は、DNA の二重らせん構造やブラック ホールの存在など、何か新しいことを明らかにするために重要です。 しかし、いくつかの啓示は、かつては別個であると考えられていた XNUMX つの古い概念が実際には同じであることを示すため、深遠です。 電気と磁気が XNUMX つの現象の XNUMX つの側面であることを示すジェームス クラーク マクスウェルの方程式、または一般相対性理論による重力と湾曲した時空の結びつきを考えてみましょう。

カリーとハワードの対応も同様ですが、より大規模であり、XNUMX つの分野内の個別の概念だけでなく、専門分野全体を結び付けています。 コンピュータサイエンス および 数理論理学。 カリー・ハワード同型性 (XNUMX つの物事の間にある種の XNUMX 対 XNUMX の対応関係が存在することを意味する用語) としても知られ、数学的証明とコンピューター プログラムとの間に関連性を確立します。

簡単に言えば、カリーとハワードの対応は、コンピュータ サイエンスの XNUMX つの概念 (タイプとプログラム) がそれぞれ命題と証明、つまり論理の概念と同等であると仮定しています。

この対応の波及効果の XNUMX つは、プログラミング (多くの場合、個人的な工芸とみなされます) が数学の理想的なレベルにまで高められるということです。 プログラムを書くことは単なる「コーディング」ではなく、定理を証明する行為になります。 これにより、プログラミングという行為が形式化され、プログラムの正しさを数学的に推論する方法が提供されます。

この通信は、それを独立して発見した 1934 人の研究者にちなんで命名されました。 XNUMX 年、数学者で論理学者のハスケル カリーは、数学の関数と、XNUMX つの命題間の「if-then」ステートメントの形式をとる論理の含意関係との類似性に気づきました。

カリーの観察に触発されて、数理論理学者のウィリアム アルビン ハワードは 1969 年に計算と論理の間の深いつながりを発見し、コンピューター プログラムの実行が論理証明の単純化によく似ていることを示しました。 コンピューター プログラムが実行されると、各行が「評価」されて XNUMX つの出力が生成されます。 同様に、証明では、(たとえば、冗長な手順を削除するか、複雑な式をより単純なものに置き換えることによって) 簡略化できる複雑なステートメントから始めて、結論 (多くの中間ステートメントから派生した、より凝縮された簡潔なステートメント) に到達します。 。

この説明は対応関係の一般的な意味を伝えていますが、それを完全に理解するには、コンピュータ科学者が「型理論」と呼ぶものについてもう少し学ぶ必要があります。

有名な逆説から始めましょう。ある村に、自分で毛を剃らない男性全員の毛を剃る理容師が住んでいます。 床屋さんは自分で髭を剃りますか？ 答えが「はい」の場合、彼は自分自身の毛を剃ってはなりません（なぜなら、彼は自分の毛を剃らない男性だけを剃るからです）。 答えが「いいえ」の場合、彼は自分自身の毛を剃らなければなりません（なぜなら、彼は自分で毛を剃らない男性全員の毛を剃るからです）。 これは、バートランド ラッセルが集合と呼ばれる概念を使用して数学の基礎を確立しようとして発見した逆説の非公式バージョンです。 つまり、矛盾が発生せずに、それ自体を含まないすべてのセットを含むセットを定義することは不可能です。

この矛盾を避けるために、「タイプ」を使用できることをラッセル氏は示しました。 大まかに言えば、これらはオブジェクトと呼ばれる特定の値を持つカテゴリです。 たとえば、自然数を意味する「Nat」という型がある場合、そのオブジェクトは 1、2、3 などになります。 研究者は通常、オブジェクトの種類を示すためにコロンを使用します。 整数型の数字 7 は、「7: Integer」と書くことができます。 型 A のオブジェクトを取得して型 B のオブジェクトを吐き出す関数、または型 A と型 B のオブジェクトのペアを結合して「A × B」と呼ばれる新しい型を作成する関数を使用できます。

したがって、このパラドックスを解決する XNUMX つの方法は、これらの型を階層に配置して、それらの型がそれ自体よりも「下位レベル」の要素のみを含むことができるようにすることです。 そうすれば、型はそれ自体を含むことができなくなり、パラドックスを生み出す自己参照性が回避されます。

型理論の世界では、ステートメントが真であることを証明することは、私たちが慣れ親しんでいるものとは異なるものになる可能性があります。 整数 8 が偶数であることを証明したい場合は、8 が実際に「偶数」と呼ばれる特定の型のオブジェクトであることを示す必要があります。この場合、メンバーシップの規則は 2 で割り切れます。8 が割り切れることを確認した後、 2 により、8 は確かに Even タイプの「住民」であると結論付けることができます。

カリーとハワードは、型が基本的に論理命題と同等であることを示しました。 関数が型に「生息」しているとき、つまり、その型のオブジェクトである関数を正常に定義できるときは、対応する命題が真であることを効果的に示していることになります。 したがって、型 A の入力を受け取り、型 B の出力を与える関数 (型 A → B で示される) は、「A であれば B」という含意に対応する必要があります。 たとえば、「雨が降っているなら、地面は濡れている」という命題を考えてみましょう。 型理論では、この命題は「Raining → GroundIsWet」型の関数によってモデル化されます。 異なって見える公式は、実際には数学的には同じです。

この関連性は抽象的に聞こえるかもしれませんが、数学とコンピューター サイエンスの実践者が自分たちの仕事についてどのように考えるかを変えただけでなく、両方の分野でいくつかの実際的な応用にもつながりました。 コンピューター サイエンスにとって、ソフトウェアの正確性を保証するプロセスであるソフトウェア検証の理論的基盤を提供します。 論理命題の観点から望ましい動作を組み立てることにより、プログラマはプログラムが期待どおりに動作することを数学的に証明できます。 また、より強力な関数型プログラミング言語を設計するための強力な理論的基盤も提供します。

そして数学に関しては、この対応が誕生につながりました。 証明アシスタント、インタラクティブな定理証明者とも呼ばれます。 これらは、Coq や Lean などの正式な証明の構築を支援するソフトウェア ツールです。 Coq では、証明の各ステップは本質的にプログラムであり、証明の有効性は型チェック アルゴリズムでチェックされます。 数学者も証明アシスタントを使用しています。特に、 無駄のない定理証明者 — 数学を形式化すること。これには、数学的な概念、定理、証明を厳密なコンピューター検証可能な形式で表現することが含まれます。 これにより、数学の非公式な言語をコンピューターでチェックできるようになります。

研究者たちは、数学とプログラミングの間のこのつながりがもたらす影響をまだ調査中です。 元のカリーとハワードの対応では、プログラミングと直観主義的論理と呼ばれる一種の論理が融合されていますが、より多くの種類の論理もそのような統合に適していることが判明しました。

「カリーの洞察からXNUMX世紀の間に何が起こったかというと、『論理システムXが計算システムYに対応する』という事例がますます発見され続けているということだ」と述べた。 マイケル・クラークソン、コーネル大学のコンピューター科学者。 研究者らはすでに、プログラミングを、「リソース」の概念を含む線形ロジックや、可能性と必要性​​の概念を扱うモーダル ロジックなど、他のタイプのロジックに関連付けています。

そして、この通信にはカリーとハワードの名前が記されているが、それを発見したのは決して彼らだけではない。 これは、通信の基本的な性質を証明しています。人々は何度も何度もそれに気づき続けます。 「計算とロジックの間に深いつながりがあるのは偶然ではないようです」とクラークソン氏は言う。