logic - 論理とカリー・ハワード対応についての質問

Question

論理プログラミングの基礎と、型システムと従来の論理との構文的類似性の現象との基本的な関係について教えてください。

Answer 1

カリーハワード同盟は、論理プログラミングではなく、関数型プログラミングに関するものです。Prologの基本的なメカニズムは、ホーン節として表現された論理式が充足可能であるかどうか、つまり、それらは本当です。

したがって、論理プログラミングは、プログラムを論理式として指定することであり、プログラムの計算は、私が言ったように、Prologreolutionにおける何らかの形の証明推論です。対照的に、カリー・ハワード対応は、自然演繹と呼ばれる特別な論理式の証明がラムダ計算のプログラムにどのように対応するかを示し、プログラムのタイプは証明が証明する式に対応します。ラムダ計算での計算は、正規化と呼ばれる証明論の重要な現象に対応します。これは、証明を新しい、より直接的な証明に変換します。したがって、論理プログラミングと関数型プログラミングは、これらの論理のさまざまなレベルに対応します。論理プログラムは論理の式に一致し、関数型プログラムは式の証明に一致します。

別の違いがあります。使用されるロジックは一般的に異なります。論理プログラミングは一般的に単純な論理を使用します—私が言ったように、Prologはホーン節に基づいています。ホーン節は、含意がネストされない可能性のある非常に制限されたクラスの式であり、論理和はありませんが、Prologはルールをカットします。対照的に、Haskellのような関数型プログラミング言語は、型がネストされた意味を持つプログラムを多用し、あらゆる種類のポリモーフィズムによって装飾されています。それらはまた、ロビンソンの計算メカニズムが基づいている排中律の原理の使用を禁止する論理のクラスである直観主義論理に基づいています。

他のいくつかのポイント：

1. ホーン節よりも洗練されたロジックに基づいてロジックプログラミングを行うことができます。たとえば、Lambda-prologは直観主義論理に基づいており、解像度とは異なる計算メカニズムを備えています。
2. Dale Millerは、カリーハワード同盟に使用される別の用語であるプログラムメタファーとしての証明とは対照的に、論理プログラミングの背後にある証明理論パラダイムをプログラミングメタファーとしての証明検索と呼んでいます。

Answer 2

論理プログラミングは、基本的に、証明の検索に向けられた目標に関するものです。型付き言語と論理の間の構造的関係には、一般に関数型言語が含まれますが、命令型言語や他の言語が含まれることもありますが、論理プログラミング言語は直接関係しません。この関係は、証明をプログラムに関連付けます。

したがって、論理プログラミングの証明検索を使用して、関数型プログラムとして解釈される証明を見つけることができます。これは（あなたが求めたように）2つの間の最も直接的な関係のようです。

この方法でプログラム全体を構築することは実用的ではありませんが、プログラムに面倒な詳細を入力するのに役立つ場合があり、実際にはこれのいくつかの重要な例があります。この基本的な例は、構造的サブタイピングです。これは、単純な含意証明を介していくつかの証明ステップを入力することに対応します。より洗練された例は、Haskellの型クラスシステムです。これには、特定の種類の目標指向検索が含まれます。極端な場合、これには、コンパイル時にチューリング完全形式の論理プログラミングが含まれます。