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

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

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

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

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

直觉逻辑只是普通函数式语言所对应的某种逻辑。重要的是，它是建设性的：基本上，证明a -> b给你一个算法来计算b，a这在常规经典逻辑中是不正确的（因为排中律，它会告诉你某事是真或假，但不是为什么）。

尽管 like 函数不像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可以很容易地具有 type Int -> Int。同样，Haskell 不能这样做。你需要依赖类型来做这样的事情。

典型的函数式语言并不是很适合编写证明，不仅因为它们缺少依赖类型，还因为 ⊥ 具有a所有类型a，可以作为任何命题的证明。但是像Coq和Agda这样的全部语言都利用对应关系来充当证明系统以及依赖类型的编程语言。

于 2012-04-18T15:33:28.973 回答
2

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

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

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

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

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

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

它是一种类型，或者是一个命题。在f :: Int -> Int中，(+1)将“程序”命名为“程序”（在特定意义上，将函数和常量都称为“程序”，或者作为证明。语言的语义必须提供f作为推理的原始规则，或者证明证明f如何可以从这样的规则和前提构建。

这些规则通常根据定义类型的基本成员的等式公理和允许您证明其他程序包含该类型的规则来指定。例如，从Intto 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 回答
2

也许理解其含义的最好方法是开始（或尝试）使用类型作为命题和程序作为证明。最好学习一种具有依赖类型的语言，例如Agda（它是用 Haskell 编写的，类似于 Haskell）。有各种关于该语言的文章和课程。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)命题视为类型，将其证明视为功能。此类证明有更先进的技术（例如，前序推理，Agda 中的组合器就像 Coq 中的策略）。

还有什么可以证明的：

  • head ∘ init ≡ head对于向量，在这里。

  • 您的编译器生成一个程序，该程序的执行给出的值与解释相同（主机）程序（此处为 Coq）中获得的值相同。这本书也是关于语言建模和程序验证主题的好读物。

  • 任何其他可以在建设性数学中证明的东西，因为 Martin-Löf 的类型论在其表达能力上等同于 ZFC。事实上，Curry-Howard 同构可以扩展到物理和拓扑以及代数拓扑。

于 2012-04-18T18:08:51.090 回答