60

インターネットで調べてみたところ、論理理論の講義にどんどん退化していないCHIの説明が頭に浮かびました。（これらの人々は、「直感的な命題論理」が実際に普通の人間にとって何かを意味するフレーズであるかのように話します！）

大まかに言えば、CHIは、タイプは定理であり、プログラムはそれらの定理の証明であると言います。しかし、それは一体何を意味するのでしょうか？

これまでのところ、私はこれを理解しました：

  • 考えてみてくださいid :: x -> x。そのタイプは、「Xが真であるとすると、Xが真であると結論付けることができます」と言います。私には合理的な定理のように思えます。

  • ここで考えてみましょうfoo :: x -> y。Haskellプログラマーなら誰でも言うように、これは不可能です。この関数を書くことはできません。（まあ、とにかく騙さずに。）定理として読むと、「Xが真であるとすれば、Yは真であると結論付けることができます」と書かれています。これは明らかにナンセンスです。そして、確かに、この関数を書くことはできません。

  • より一般的には、関数の引数は「これが真であると見なされる」と見なすことができ、結果タイプは「他のすべてが真であると仮定して真である」と見なすことができます。たとえば、関数の引数がx -> yある場合、Xが真であるということは、Yが真でなければならないことを意味すると仮定することができます。

  • たとえば、(.) :: (y -> z) -> (x -> y) -> x -> z「YがZを含意し、XがYを含意し、Xが真であると仮定すると、Zが真であると結論付けることができます」と見なすことができます。これは私には論理的に理にかなっているようです。

さて、一体どういうInt -> Int意味ですか？o_O

私が思いつくことができる唯一の賢明な答えはこれです：関数X-> Y-> Zがある場合、型シグネチャは「タイプXの値とタイプYの値を作成できると仮定すると、タイプZ"の値を作成することができます。そして、関数本体は、これをどのように行うかを正確に記述します。

それは理にかなっているようですが、あまり面白くありません。だから明らかにこれ以上のものがあるに違いない...

4

3 に答える 3

52

カリーハワード同形性は、型が命題に対応し、値が証明に対応することを単純に述べています。

Int -> Int論理的な命題としてはあまり興味深いことではありません。何かを論理的な命題として解釈するときは、その型に人が住んでいる（値がある）かどうかだけに関心があります。つまり、Int -> Int「与えられたInt、私はあなたに与えることができる」という意味Intであり、もちろんそれは真実です。それには多くの異なる証明があります（そのタイプのさまざまな異なる機能に対応します）が、それを論理的な命題としてとらえるとき、あなたは本当に気にしません。

それは、興味深い命題がそのような機能を含むことができないという意味ではありません。命題として、その特定のタイプは非常に退屈です。

完全にポリモーフィックではなく、論理的な意味を持つ関数型のインスタンスについては、p -> Void（いくつかのpについて）、Void無人型：値のない型（Haskellでは⊥を除くが、それは後で）。タイプの値を取得する唯一の方法Voidは、矛盾を証明できる場合（もちろん、不可能です）でありVoid、矛盾を証明したことを意味するため、そこから任意の値を取得できます（つまり、関数が存在しますabsurd :: Void -> a） 。 。したがって、p -> Void¬pに対応します。これは「pは虚偽を意味する」という意味です。

直観主義論理は、一般的な関数型言語が対応する特定の種類の論理です。重要なのは、それが建設的であるということです。基本的に、の証明は、から計算するアルゴリズムa -> bを提供します。これは、通常の古典論理では当てはまりません（排中律の法則のため、何かが真か偽かを教えてくれますが、そうではありません）なぜ）。ba

のような機能Int -> Intは命題ほど意味がありませんが、他の命題でそれらについてステートメントを作成することができます。たとえば、（GADTを使用して） 2つのタイプの等価のタイプを宣言できます。

data Equal a b where
    Refl :: Equal a a

タイプの値がある場合Equal a b、a同じタイプのb：Equal a bは命題a = bに対応します。問題は、この方法でしか型の平等について話すことができないということです。しかし、依存型がある場合は、この定義を簡単に一般化して任意の値で機能させることができるため、値aとbが同一であるEqual a bという命題に対応します。したがって、たとえば、次のように書くことができます。 

type IsBijection (f :: a -> b) (g :: b -> a) =
    forall x. Equal (f (g x)) (g (f x))

ここで、fとgは通常の関数であるため、fは簡単にタイプを持つことができますInt -> Int。繰り返しますが、Haskellはこれを行うことができません。このようなことを行うには、依存型が必要です。

典型的な関数型言語は、依存型がないだけでなく、aすべてaの型を持つ⊥が命題の証明として機能するため、証明を書くのにあまり適していません。しかし、 CoqやAgdaのようなトータル言語は、対応を利用して、依存型のプログラミング言語としてだけでなく、証明システムとしても機能します。

于 2012-04-18T15:33:28.973 に答える
2

おそらく、それが何を意味するのかを理解するための最良の方法は、型を命題として使用し、プログラムを証明として使用することから始める（または試す）ことです。Agda（Haskellで書かれており、Haskellに似ています）などの依存型の言語を学ぶことをお勧めします。その言語に関するさまざまな記事やコースがあります。Agdaは不完全ですが、LYAHFGGの本のように、物事を単純化しようとしています。

簡単な証明の例を次に示します。

{-# OPTIONS --without-K #-} -- we are consistent

module Equality where

-- Peano arithmetic.
-- 
--   ℕ-formation:     ℕ is set.
-- 
--   ℕ-introduction:  o ∈ ℕ,
--                    a ∈ ℕ | (1 + a) ∈ ℕ.
-- 
data ℕ : Set where
  o : ℕ
  1+ : ℕ → ℕ

-- Axiom for _+_.
-- 
--   Form of ℕ-elimination.
-- 
infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
o + m = m
1+ n + m = 1+ (n + m)

-- The identity type for ℕ.
-- 
infix 4 _≡_
data _≡_ (m : ℕ) : ℕ → Set where
  refl : m ≡ m

-- Usefull property.
-- 
cong : {m n : ℕ} → m ≡ n → 1+ m ≡ 1+ n
cong refl = refl

-- Proof _of_ mathematical induction:
-- 
--   P 0, ∀ x. P x → P (1 + x) | ∀ x. P x.
-- 
ind : (P : ℕ → Set) → P o → (∀ n → P n → P (1+ n)) → ∀ n → P n
ind P P₀ _ o = P₀
ind P P₀ next (1+ n) = next n (ind P P₀ next n)

-- Associativity of addition using mathematical induction.
-- 
+-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative m n p = ind P P₀ is m
  where
    P : ℕ → Set
    P i = (i + n) + p ≡ i + (n + p)
    P₀ : P o
    P₀ = refl
    is : ∀ i → P i → P (1+ i)
    is i Pi = cong Pi

-- Associativity of addition using (dependent) pattern matching.
-- 
+-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative′ o _ _ = refl
+-associative′ (1+ m) n p = cong (+-associative′ m n p)

(m + n) + p ≡ m + (n + p)そこでは、命題をタイプとして、その証明を関数として見ることができます。このような証明には、より高度な手法があります（たとえば、事前注文の推論、AgdaのコンビネータはCoqの戦術のようなものです）。

他に証明できること：

  • head ∘ init ≡ headベクトルについては、ここで。

  • コンパイラは、同じ（ホスト）プログラムの解釈で得られた値と同じ値を実行するプログラムを生成します。ここでは、Coqの場合です。この本は、言語モデリングとプログラム検証のトピックについてもよく読んでいます。

  • マーティン・レーフの表現力の型理論はZFCと同等であるため、構成主義数学で証明できるものは他にあります。実際、カリー・ハワード同形性は、物理学とトポロジー、および代数トポロジーに拡張できます。

于 2012-04-18T18:08:51.090 に答える
2

私が思いつくことができる唯一の賢明な答えはこれです：関数X-> Y-> Zがある場合、型シグネチャは「タイプXの値とタイプYの値を作成できると仮定すると、タイプZ"の値を作成することができます。そして、関数本体は、これをどのように行うかを正確に記述します。それは理にかなっているようですが、あまり面白くありません。だから明らかにこれ以上のものがあるに違いない...

ええ、そうです、それは多くの意味を持ち、多くの質問を開くので、かなり多くのことがあります。

まず第一に、CHIについてのあなたの議論は、含意/関数型（->）の観点からのみ組み立てられています。これについては話しませんが、接続詞と論理和がそれぞれ積型と和型にどのように対応するかを見たことがあるでしょう。しかし、否定、全称記号、存在記号などの他の論理演算子についてはどうでしょうか。これらを含む論理的証明をプログラムにどのように変換しますか？おおまかに次のようになります。

  • 否定は、ファーストクラスの継続に対応します。これを説明するように私に頼まないでください。
  • 命題（個々ではない）変数の全称記号は、パラメトリック多型に対応します。したがって、たとえば、ポリモーフィック関数idは実際には次のタイプを持ちますforall a. a -> a
  • 命題変数の存在記号は、データまたは実装の非表示に関係するいくつかのことに対応します。抽象データ型、モジュールシステム 、および動的ディスパッチです。GHCの実存的なタイプはこれに関連しています。
  • 個々の変数に対する普遍的かつ存在記号化は、依存型システムにつながります。

それ以外に、論理に関するあらゆる種類の証明がプログラミング言語に関する証明に即座に変換されることも意味します。たとえば、直観主義論理の決定可能性は、単純型付きラムダ計算のすべてのプログラムの終了を意味します。

さて、Int-> Intはどういう意味ですか？o_O

それはタイプ、あるいは命題です。で、「プログラム」f :: Int -> Intに(+1)名前を付けます（特定の意味で、関数と定数の両方を「プログラム」または代わりに証明として認めます。言語のセマンティクスは、f推論の原始的な規則として提供するかf、証明がどのように行われるかを示す必要があります。そのようなルールと前提から構築することができます。

これらのルールは、タイプの基本メンバーを定義する等式公理と、他のどのプログラムがそのタイプに存在するかを証明できるルールの観点から指定されることがよくあります。たとえば、IntからNat（0から先の自然数）に切り替えると、次のルールが得られます。

  • 公理:(0 :: Natの0原始的な証明ですNat）
  • ルール：x :: Nat ==> Succ x :: Nat
  • ルール：x :: Nat, y :: Nat ==> x + y :: Nat
  • ルール：x + Zero :: Nat ==> x :: Nat
  • ルール：Succ x + y ==> Succ (x + y)

これらの規則は、自然数の加算に関する多くの定理を証明するのに十分です。これらの証明もプログラムになります。

于 2012-04-18T18:47:29.793 に答える