Curry-Howard同构

Question

Curry-Howard同构

haskelltypeslogiccurry-howard

61

我在互联网上搜索了一下，没有找到任何有关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 的值”。而函数体则描述了如何实现这一过程。

这似乎很有道理，但并不是非常有趣。所以显然这其中必须还有更多的东西……

- MathematicalOrchid

6

https://dev59.com/dHA85IYBdhLWcg3wCfBZ - Don Stewart

3

在我发布这个之前请阅读那个 - 结果很快就迷失了... :-S - MathematicalOrchid

30

公平起见，大多数“普通人”不会去查阅Curry-Howard同构。 - amindfv

2

@amindfv 嗯，我想这也算公平了。 :-) - MathematicalOrchid

3个回答

2

我唯一能想到的合理答案是这样的：如果有一个函数X -> Y -> Z，那么类型签名说明“假设可以构建一个类型为X的值和一个类型为Y的值，那么就可以构建一个类型为Z的值”，而函数体恰好描述了如何完成此操作。这似乎很有道理，但并不十分有趣。因此，显然必须有更多内容……

嗯，确实，因为它具有许多含义并引出了很多问题。

首先，你只讨论了条件/函数类型（->）在CHI中的情况。虽然你没有提到这一点，但你可能已经看到了连词和析词分别对应于积类型和和类型。但是其他逻辑运算符（如否定、全称量化和存在性量化）怎么办？我们如何将涉及这些逻辑证明转换为程序？大致上是这样的：

- 否定对应于first-class continuations（一等延续）。不要让我解释这个。 - 对命题变量（而不是个体变量）进行普遍量化对应于parametric polymorphism（参数多态性）。因此，多态函数id实际上具有类型forall a. a -> a - 对命题变量进行存在量化对应于与数据或实现隐藏相关的一些内容：抽象数据类型、模块系统和动态调度。 GHC的存在类型与此有关。 - 对个体变量进行全称和存在量化导致dependent type systems（依赖类型系统）。

除此之外，这也意味着各种逻辑证明立即转换为关于编程语言的证明。例如，直觉主义命题逻辑的可决定性意味着简单类型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)

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

- Luis Casillas

我没有提到，但是我认为类型的记录就像逻辑与，而类似于 Either 的东西则是逻辑或。 - MathematicalOrchid

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)”的命题以及其证明作为函数。有更高级的技术用于此类证明（例如 preorder reasoning，Agda中的组合子类似于Coq中的策略）。

还可以证明什么：

head ∘ init ≡ head 对于向量成立，在这里。
你的编译器生成的程序执行后得到的值与同样（主机）程序的解释得到的值相同，在这里，针对 Coq。这本书也是关于语言建模和程序验证方面的好读物。
任何其他可以在构造数学中证明的事情，因为 Martin-Löf 的类型理论在其表达能力上等价于 ZFC。实际上，Curry-Howard 同构可以扩展到物理和拓扑以及代数拓扑。

- JJJ

这当然是一个完全“另外”的问题，但有一次我尝试理解其中一种高级语言。（我忘记它是Agda、Coq、Epigram还是其他什么了。）文档随意地使用技术术语，其含义对我来说完全不透明，我很快就迷失了…… - MathematicalOrchid

1

@MathematicalOrchid CH是同构，它阐明了两个不同领域概念之间的关系。你可以对一个领域有所了解（比如简单类型λ演算或Per Martin-Löf的依赖类型理论），但为了构建同构，你也必须了解另一个领域（自然推导系统或直觉主义逻辑）。 - JJJ

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- ehird · Accepted Answer

Curry-Howard同构简单地说明类型对应于命题，值对应于证明。 Int -> Int作为逻辑命题并没有太多有趣的含义。当将某些东西解释为逻辑命题时，您只关心该类型是否有任何值（是否被占用）。因此，Int -> Int只是意味着“给定一个Int，我可以给你一个Int”，当然是真的。有许多不同的证明（对应于该类型的各种不同函数），但在将其视为逻辑命题时，您并不真正关心。

这并不意味着有趣的命题不能涉及这样的函数；只是说这个特定类型作为命题相当无聊。

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

直觉主义逻辑仅仅是一种与常见函数式语言对应的逻辑。重要的是，它是构造性的：基本上，一个证明a -> b会给你一个从a计算出b的算法，这在普通经典逻辑中并不成立（因为排中律会告诉你某个命题要么是真的，要么是假的，但不会告诉你为什么）。

即使像Int -> Int这样的函数作为命题并没有多大意义，我们可以用其他命题来陈述它们。例如，我们可以使用广义代数数据类型声明两个类型的相等性：

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，可以作为任何命题的证明。但是Coq和Agda等total语言利用对应关系来充当证明系统以及依赖类型编程语言。