Curry-Howard同构

Question

我在网上搜索过，我找不到任何关于迟浩田的解释，这些解释不会很快退化成一堂关于逻辑理论的讲座，而逻辑理论在我的脑海里是一场彻底的讨论。(这些人说的好像“直觉命题演算”是一个短语，实际上对正常人来说意味着什么！)

粗略地说，齐说类型是定理，程序是这些定理的证明。但这到底是什么意思？

到目前为止，我已经搞清楚了：

• 考虑一下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同构简单地说类型对应于命题，而值对应于证明。

作为一个逻辑命题，Int -> Int并不意味着很有趣。当将某一项解释为逻辑命题时，您只对类型是否有人居住(是否有任何值)感兴趣。所以，Int -> Int的意思就是“给定一个Int，我可以给你一个Int"，这当然是真的。关于它有许多不同的证明(对应于这种类型的各种不同的功能)，但是当把它当作一个逻辑命题时，你并不在乎。

这并不意味着有趣的命题不能包含这样的功能；只是，作为一个命题，这种特定类型是相当无聊的。

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

直觉逻辑只是普通功能语言对应的一种逻辑。重要的是，这是建设性的:基本上，a -> b的证明给出了从a中计算b的算法，这在常规经典逻辑中是不正确的(因为排除中间定律会告诉您某些东西是对的还是错的，但不是为什么)。

尽管像Int -> Int这样的函数并不代表命题，但我们可以用其他命题来说明它们。例如，我们可以声明两种类型的相等类型(使用GADT)：

data Equal a b where
    Refl :: Equal a a

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

Answer 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。实际上，Curry同构可以扩展到物理与拓扑和代数拓扑.

Answer 3

我能给出的唯一明智的答案是:如果您有一个函数X -> Y -> Z，那么类型签名说“假设可以构造一个类型X的值，另一个类型是Y，那么就有可能构造一个类型Z的值”。函数体精确地描述了你将如何做到这一点。这似乎是有道理的，但并不是很有趣。所以很明显比这更重要的是。

嗯，是的，还有更多，因为它有很多的含义，并打开了许多问题。

首先，您对CHI的讨论是专门根据含义/函数类型(->)进行的。您没有谈到这一点，但是您可能已经看到了连接和不连接分别如何对应于乘积和和类型。但其他逻辑运算符如否定、普遍量化和存在量化又如何呢？我们如何将涉及这些的逻辑证明转换为程序？原来大概是这样的：

• 否定对应于一级延续.别让我解释这个。
• 对命题变量(非个体变量)的通用量化对应于参数多态性。例如，多态函数id实际上具有forall a. a -> a类型。
• 对命题变量的存在量化对应于一些与数据或实现隐藏有关的事情:抽象数据类型、模块系统和动态调度。GHC的存在类型与此有关。
• 个体变量的普遍存在量化导致了依赖型系统的产生。

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

现在，-> Int到底是什么意思？？o_O

它是一种类型，或者是一种命题。在f :: Int -> Int中，(+1)将一个“程序”命名为“程序”(在某种特定意义上，它同时承认函数和常量为“程序”，或者作为证明)。语言的语义必须提供f作为一个基本的推理规则，或者演示f是如何从这些规则和前提构建的证明。

这些规则通常是根据定义类型的基本成员的等式公理和允许您证明该类型中的其他程序的规则来指定的。例如，从Int切换到Nat (自然数从0向前)，我们可以有以下规则：

• Axiom：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)

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