数学的論理とコンピュータプログラムコードの深いつながり：互いの鏡像

DNAの二重らせん構造やブラックホールの存在など、いくつかの科学的発見は何か新しいことを明らかにするため、大きな意義を与えられております。しかし、この啓示にはさらに深い意味がある。なぜなら、これまで非常に異なっているように思われた 2 つの古い概念が実際には同じであることを示しているからだ。たとえば、ジェームズ・クラーク・マクスウェルは、電気と磁気が同じ現象の 2 つの側面であることを示す方程式を開発し、一般相対性理論は重力を時空の曲率に関連付けました。

同じことはカリー・ハワード対応にも当てはまり、これは 1 つの分野における 2 つの異なる概念だけでなく、コンピューター サイエンスと数理論理学という 2 つの分野全体を関連付けます。この対応は、カリー・ハワード同型性（同型性とは、2 つのものの間に 1 対 1 の対応があることを意味します）としても知られ、数学的証明とコンピュータ プログラムの間のつながりを確立します。

簡単に言えば、カリー・ハワードは、コンピュータサイエンスの 2 つの概念 (型とプログラム) は、論理の 2 つの概念 (命題と証明) と同等であると主張しています。

この対応の結果、プログラム開発は、以前は一般的に職人技と考えられていましたが、理想的な数学的レベルにまで高められました。プログラム開発は単に「コードを書く」だけではなく、定理を証明する行為にもなっています。これにより、プログラム開発の動作が形式化され、プログラムの正確性について数学的に推論する方法が提供されます。

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

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

この説明では、この対応が何を意味するのか大まかに説明していますが、それを完全に理解するには、コンピューター科学者が「型理論」と呼ぶものについてもう少し知識が必要です。

有名なパラドックスから始めましょう。ある村に、自分で髭を剃らない人だけを髭を剃る床屋がいました。それで、この床屋さんは自分で髭を剃るんですか？答えが「はい」の場合、彼は自分自身を剃ってはいけません（彼は自分自身を剃らない人だけを剃るからです）。答えが「いいえ」の場合、彼は自分で髭を剃っているに違いありません（彼は自分で髭を剃らない人全員の髭を剃っているので）。これは、バートランド・ラッセルが集合と呼ばれる概念を使用して数学の基礎を築こうとしたときに発見したパラドックスの非公式バージョンです。言い換えれば、それ自身を含まないすべての集合を含む集合を定義することは不可能であり、このプロセスは必然的に矛盾につながります。

ラッセルの研究によると、このパラドックスを回避するには型を使用できるそうです。大まかに言えば、型とは具体的な値がオブジェクトと呼ばれるカテゴリです。たとえば、自然数を表す型 Nat がある場合、そのオブジェクトは 1、2、3 などになります。研究者はオブジェクトの種類を示すためにコロンをよく使用します。たとえば、整数値 7 の場合は、「7: Integer」と記述できます。関数を使用して、タイプ A のオブジェクトをタイプ B のオブジェクトに変換したり、関数を使用してタイプ A とタイプ B の 2 つのオブジェクトを新しいタイプ「A×B」のオブジェクトに結合したりできます。

したがって、このパラドックスを解決するための 1 つの方法は、これらのタイプを階層化して、それらのタイプ自体より 1 レベル下の要素のみが含まれるようにすることです。すると、型はそれ自身を含むことができなくなり、上記のパラドックスを引き起こす自己参照が回避されます。

型理論の世界では、ステートメントが真であることを証明するプロセスは、私たちが慣れているものと同じではない可能性があります。整数 8 が偶数であることを証明したい場合、鍵となるのは、8 が実際には「偶数」型のオブジェクトであり、この型を定義する規則はその要素が 2 で割り切れることであることを証明することです。 8 が 2 で割り切れることを確認した後、8 は「偶数」タイプの「居住者」であると結論付けることができます。

カリー氏とハワード氏は、型は基本的に論理命題と同等であることを証明しました。関数が型に「存在する」場合、つまり関数がその型のオブジェクトである場合、対応する命題が真であることを効果的に証明できます。したがって、入力としてタイプ A のオブジェクトを受け取り、出力としてタイプ B のオブジェクトを生成する関数 (タイプ A→B と表現) は、「A ならば B」という含意に対応している必要があります。たとえば、「雨が降れば、地面は濡れている」という命題があるとします。型理論では、この命題は「雨が降る→地面が濡れている」というタイプの関数としてモデル化されます。 2 つの表現は見た目は異なりますが、数学的には同じです。

このつながりは抽象的に思えるかもしれませんが、数学やコンピューターサイエンスの実践者が仕事について考える方法を変えるだけでなく、両方の分野に実用的な応用もあります。コンピュータ サイエンスでは、このつながりは、ソフトウェアが正しいことを確認するプロセスであるソフトウェア検証の理論的基礎を提供します。望ましい動作を論理命題の形式で記述することにより、プログラム開発者はプログラムが期待どおりに動作するかどうかを数学的に証明できます。そして、このつながりは、より強力な関数型プログラミング言語を設計するための強固な理論的基礎も提供します。

数学では、この対応により、インタラクティブな定理証明器としても知られる証明支援ツールが生まれました。これらのソフトウェア ツールは正式な証明の構築に役立ちます。具体的な例としては、Coq や Lean などがあります。 Coq では、証明の各ステップは本質的にプログラムであり、証明の妥当性は型チェック アルゴリズムによってチェックされます。数学者は、数学の概念、定理、証明をコンピューターで検証できる厳密な形式で表現する数学の形式化にも証明支援ツール (特に Lean 定理証明器) を使用しています。これにより、非公式な数学言語をコンピューターでテストできるようになります。

研究者たちは、数学とプログラミングのつながりがもたらす潜在的な成果についても研究しています。オリジナルの Curry-Howard 対応では、プログラミングと直観主義論理と呼ばれるものを組み合わせていましたが、統合できる論理の種類は他にもたくさんあることがわかりました。

「カリーが洞察を得てから1世紀が経ち、私たちは『論理システムXは計算システムYに対応する』という例をどんどん見つけてきました」とコーネル大学のコンピューター科学者マイケル・クラークソンは言う。研究者たちはまた、プログラミングを「リソース」の概念を含む線形論理や、可能性と必然性の概念を含む様相論理など他の種類の論理と関連付けている。

この書簡にはカリー氏とハワード氏の名前が記されているが、それを発見したのは決して彼らだけではない。これは、この対応の基本的な特性を示しています。つまり、人々はそれを何度も気づくのです。 「計算と論理が深く結びついているのは偶然ではないようです」とクラークソン氏は言う。