数理論理学とコンピューター プログラム コードの深い関係: 互いの鏡像

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

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

簡単に言うと、カリー-ハワードは、コンピューター サイエンスの 2 つの概念 (型とプログラム) は、論理の 2 つの概念 (命題と証明) に相当すると信じています。)。

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

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

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

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

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

ラッセルの研究は、この矛盾を回避するために型を使用できることを示しています。大まかに言うと、型とは、その具体的な値がオブジェクトと呼ばれるカテゴリです。たとえば、自然数を表す型 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 では、各証明ステップは本質的にプログラムであり、証明の有効性は型チェック アルゴリズムを通じてチェックされます。数学者はまた、数学を形式化するために証明アシスタント (特にリーン定理証明者) を使用しています。これには、数学的な概念、定理、証明をコンピューターで検証できる厳密な形式で表現することが含まれます。これにより、場合によっては非公式な数学言語をコンピューターでテストできるようになります。

研究者たちは、数学とプログラミングの間のこの関係がもたらす潜在的な成果についても調査しています。オリジナルのカリーとハワードの対応では、プログラム開発を直観主義的論理と呼ばれる一種の論理で統合していましたが、統合できる論理の種類はさらにたくさんあることが判明しました。

コーネル大学のコンピュータ科学者マイケル・クラークソンは次のように述べています。「カリーが洞察を導き出してから一世紀の間、私たちはますます多くの『論理システム、つまりシステム Y のインスタンス』を発見し続けてきました。」また、「リソース」の概念を含む線形ロジックや、可能性と必要性​​の概念を含むモーダル ロジックなど、他のタイプのロジックにもプログラミングをリンクしました。

そして、この通信にはカリーとハワードの名前が付いていますが、この通信の発見者は決して彼らだけではありません。これは、この対応の基本的な性質を示しています。つまり、人々は何度もそれを認識します。クラークソン氏は、「コンピューティングとロジックの深いつながりは偶然ではないようです。」

以上が数理論理学とコンピューター プログラム コードの深い関係: 互いの鏡像の詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。