Curry-Howard 同构

Question

我在互联网上进行了搜索，但我找不到任何关于 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 类型的值”。函数体准确地描述了你将如何做到这一点。

这似乎有道理，但不是很有趣。很明显，它肯定比这更多......

Answer 1

Curry-Howard 同构只是说明类型对应于命题，值对应于证明。

Int -> Int 作为一个逻辑命题并不真正意味着有趣。在将某事解释为逻辑命题时，您只关心该类型是否inhabited（具有任何值）。所以，Int -> Int 只是意味着“给定一个Int，我可以给你一个Int”，这当然是真的。它有许多不同的证明（对应于该类型的各种不同函数），但是当把它作为一个逻辑命题时，你并不在乎。

这并不意味着有趣的命题不能涉及这样的功能；只是那个特定的类型很无聊，作为一个命题。

对于不完全多态且具有逻辑意义的函数类型的实例，请考虑p -> Void（对于某些p），其中Void 是无人居住的类型：类型没有值（Haskell 中的 ⊥ 除外，但我稍后会谈到）。获得Void 类型值的唯一方法是，如果你能证明矛盾（这当然是不可能的），并且由于Void 意味着你已经证明了矛盾，你可以从中获得任何价值（即存在一个函数absurd :: Void -> a)。因此，p -> Void 对应于 ¬p：它的意思是“p 意味着虚假”。

Intuitionistic logic只是普通函数式语言对应的某种逻辑。重要的是，它是建设性的：基本上，a -> b 的证明为您提供了一个算法来从 a 计算 b，这在常规经典逻辑中是不正确的（因为law of excluded middle，它会告诉你某事是真还是假，但不是为什么）。

尽管像Int -> Int 这样的函数作为命题的意义不大，但我们可以用其他命题来陈述它们。例如，我们可以声明两种类型的相等类型（使用GADT）：

data Equal a b where
    Refl :: Equal a a

如果我们有一个Equal a b类型的值，那么a与b的类型相同：Equal a b对应命题a = b。问题是我们只能这样谈论类型的相等性。但是如果我们有dependent types，我们可以很容易地将这个定义推广到与任何值一起工作，所以Equal a b将对应于值 的命题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，可以作为任何命题的证明.但是total 语言，如Coq 和Agda，利用这种对应来充当证明系统以及依赖类型的编程语言。

Answer 2

也许理解它的最佳方式意味着是开始（或尝试）使用类型作为命题和程序作为证明。最好学习一种具有依赖类型的语言，例如Agda（它是用 Haskell 编写的，类似于 Haskell）。该语言有各种articles and courses。 Learn you an 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) 命题是类型，它的证明是函数。此类证明有更高级的技术（例如，preorder reasoning，Agda 中的组合器就像 Coq 中的策略）。

还有什么可以证明的：

• head ∘ init ≡ head 用于向量，here。

• 您的编译器生成一个程序，该程序的执行给出的值与在解释 Coq 的同一（主机）程序 here 中获得的值相同。 This book 也是语言建模和程序验证主题的好读物。

• 任何其他可以在构造数学中证明的东西，因为 Martin-Löf 的类型理论在其表达能力上等同于 ZFC。事实上，Curry-Howard 同构可以扩展到physics and topology 和algebraic topology。

Answer 3

我能想出的唯一明智的答案是：如果你有一个函数 X -> Y -> Z，那么类型签名会说“假设可以构造一个 X 类型的值，另一个类型Y，那么就可以构造一个 Z 类型的值”。函数体准确地描述了你将如何做到这一点。这似乎是有道理的，但它不是很有趣。很明显，它肯定比这更多......

嗯，是的，还有很多，因为它有很多含义并提出了很多问题。

首先，您对 CHI 的讨论完全是根据含义/功能类型 (->)。您没有谈论这个，但您可能也已经看到合取和析取分别对应于乘积和求和类型。但是其他逻辑运算符，如否定、全称量化和存在量化呢？我们如何将涉及这些的逻辑证明转化为程序？原来大致是这样的：

• 否定对应于一等延续。不要让我解释这个。
• 对命题（而非单个）变量的通用量化对应于参数多态性。例如，多态函数id 确实具有forall a. a -> a 类型
• 对命题变量的存在量化对应于一些与数据或实现隐藏有关的事情：抽象数据类型、模块系统和动态调度。 GHC 的存在类型与此有关。
• 对单个变量的普遍和存在量化导致依赖类型系统。

除此之外，这还意味着各种关于逻辑的证明会立即转化为关于编程语言的证明。例如，直觉命题逻辑的可判定性意味着在简单类型的 lambda 演算中终止所有程序。

现在，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)

这些规则足以证明许多关于自然数加法的定理。这些证明也将是程序。