8

当我问这个问题时，现在已删除的答案之一是暗示该类型Either对应于Curry-Howard 对应关系中的 XOR，而不是 OR ，因为它不能同时是Left和Right。

真相在哪里？

4

3 回答 3

12

如果你有一个 type的值P 和一个type 的值Q（也就是说，你有一个 proof ofP和一个 proof of Q），那么你仍然可以提供一个 type 的值Either P Q。

考虑

x :: P
y :: Q
...

z :: Either P Q
z = Left x    -- Another possible proof would be `Right y`

虽然Either没有明确表示这种情况的特定情况（与 不同These），但它没有做任何事情来排除它（如异或）。

两者都有证明的第三种情况与只有一个有证明的其他两种情况略有不同，这反映了直觉逻辑中“不排除”某事与“包括”某事有点不同的事实，因为Either不提供这个事实的特别证人。但是Either，它不是 XOR 通常工作方式的 XOR，因为正如我所说，它不排除两个部分都有证明的情况。另一方面，丹尼尔瓦格纳在这个答案中提出的更接近异或。

Either就其可能的证人而言，它有点像异或。另一方面，当您考虑是否可以在四种可能的情况下实际创建见证时，它就像一个包容性OR：拥有 P 的证明和 Q 的反驳，拥有 Q 的证明和 P 的反驳，对两者都有证明或对两者都有反驳。[1]当你有 P 和 Q 的证明时你可以构造一个类型的值Either P Q（类似于包含 OR），你无法区分这种情况与只有 P 有一个证明或只有 Q 有一个证明的情况只有一个类型的值Either P Q（类似于异或）。另一方面，Daniel Wagner 的解决方案在两者上都类似于异或建设和解构。

还值得一提的是，These更明确地表示两者都有证明的可能性。These类似于在构造和解构上的包容性OR。但是，还值得注意的是，当您同时拥有 P 和 Q 的证明时，没有什么可以阻止您使用“不正确”的构造函数。These在这方面，您可以扩展为更具代表性的包容性 OR复杂：

data IOR a b
  = OnlyFirst  a       (Not b)
  | OnlySecond (Not a) b
  | Both       a       b

type Not a = a -> Void

如果您只对These与Either证明无关的逻辑系统感兴趣（这意味着无法区分相同的命题），但在您希望在逻辑中具有更多计算相关性的情况下可能很重要。[2]

在编写实际要执行的计算机程序的实际情况中，计算相关性通常非常重要。尽管0和23都是该Int类型存在的证明，但我们当然喜欢在程序中区分这两个值，一般来说！

关于“建设”和“破坏”

本质上，我只是指通过构造“创建类型的值”和通过破坏“模式匹配”（有时人们在这里使用“引入”和“消除”这两个词，特别是在逻辑上下文中）。

对于 Daniel Wagner 的解决方案：

  • 构造：当你构造一个 type 的值时Xor A B，你必须提供一个 or 中的一个的证明和另一个AorB的反驳。这类似于异或。除非A您对其中一个or有一个反驳B 并且对另一个有一个证明，否则不可能构造出 this 的值。A一个特别重要的事实是，如果您有两者的证明并且B您没有对它们中的任何一个进行反驳（与包含OR 不同），则您无法构造此类型的值。

  • 破坏：当你对 type 的值进行模式匹配时Xor A B，你总是有一个类型的证明和另一个类型的反驳。它永远不会为您提供两者的证据。这是从它的定义中得出的。

在这种情况下IOR：

  • 构造：当您创建一个 type 的值时IOR A B，您必须执行以下操作之一：(1) 仅提供 的证明A和反驳B，(2) 提供 的证明B和反驳B，(3) 提供证明A和B。_ 这就像包容性 OR。这三种可能性完全对应于 的三个构造函数中的每一个IOR，没有重叠。请注意，与 的情况不同，在您同时证明和的情况下These，您不能使用“不正确的构造函数” ：在这种情况下，生成类型值的唯一方法是使用（因为否则您需要提供驳斥或_ABIOR A BBothAB）。

  • 破坏：由于您有证明A和中至少一个的B三种可能情况完全由通过对其进行模式匹配为假（如果适用）。IORAB

模式匹配开启IOR

模式匹配的IOR工作方式与任何其他代数数据类型的模式匹配完全相同。这是一个例子：

x :: IOR Char Int
x = Both 'c' 3

y :: IOR Char Void
y = OnlyFirst 'a' (\v -> v)

f :: Not p -> IOR p Int
f np = OnlySecond np 7

z :: IOR Void Int
z = f notVoid

g :: IOR p Int -> Int
g w =
  case w of
    OnlyFirst  p q -> -1
    OnlySecond p q -> q
    Both       p q -> q

-- We can show that the proposition represented by "Void" is indeed false:
notVoid :: Not Void
notVoid = \v -> v

然后是一个示例 GHCi 会话，加载了上面的代码：

ghci> g x
3
ghci> g z
7

[1]当您认为某些陈述是不可判定的，因此您无法为它们构造证明或反驳时，这会变得更加复杂。

[2]同伦类型理论是证明相关系统的一个例子，但这已经达到了我目前知识的极限。

于 2020-10-16T18:46:42.283 回答
6

也许尝试用“证据”替换 Curry-Howard 同构中的“证明”。

下面我将使用斜体来表示命题和证明（我也将其称为证据），同构的数学方面，我将使用code类型和值。

问题是：假设我知道P为真的证据的类型（我将称之为这种类型P），并且我知道Q为真的证据的类型（我称之为这种类型Q），那么什么是命题R = P OR Q的证据类型？

那么有两种方法可以证明R：我们可以证明P，或者我们可以证明Q。我们可以证明两者，但这将是不必要的工作。

现在问应该是什么类型？它是事物的类型，要么是P的证据，要么是Q的证据。即值是类型的P东西或类型的东西Q。该类型Either P Q恰好包含这些值。

如果你有P AND Q的证据怎么办？好吧，这只是 type 的一个值(P, Q)，我们可以编写一个简单的函数：

f :: (p,q) -> Either p q
f (a,b) = Left a

如果我们可以证明P AND Q，这为我们提供了一种证明P OR Q的方法。因此不能对应异或。Either

P XOR Q的类型是什么？

在这一点上，我会说否定在这种建设性逻辑中有点烦人。

让我们将问题转换为我们理解的东西，以及我们不理解的更简单的东西：

P XOR Q = ( P AND (NOT Q )) OR ( Q AND (NOT P ))

现在问：NOT P的证据类型是什么？

对于为什么这是最简单的类型，我没有直观的解释，但如果不是P为真，那么P为真的证据将是一个矛盾，我们称之为证明 FALSE，即无法证明的事情（又名 BOTTOM 或 BOT）。也就是说，NOT P可以用更简单的术语写成：P IMPLIES FALSE。FALSE 的类型称为Void（在 haskell 中）。这是一种没有价值的类型，因为没有证据。因此，如果您可以构造该类型的值，您将遇到问题。IMPLIES 对应于函数，因此对应于 NOT P的类型是P -> Void。

我们将其与我们所知道的相结合，并在命题语言中得到以下等价：

P XOR Q = ( P AND (NOT Q )) OR ( Q AND (NOT P )) = ( P AND ( Q暗示错误)) OR (( P暗示错误) AND Q )

那么类型是：

type Xor p q = Either (p, q -> Void) (p -> Void, q)
于 2020-10-16T21:38:41.420 回答
5

混乱源于逻辑的布尔真值表阐述。特别是，当两个参数都为 True 时，OR 为 True，而 XOR 为 False。从逻辑上讲，这意味着证明 OR 足以证明其中一个论点；但如果另一个也是 True 也没关系——我们只是不在乎。

在 Curry-Howard 的解释中，如果有人给你一个 的元素Either a b，而你能够从中提取 的值a，你仍然对 是一无所知b。它可以有人居住，也可以不有人居住。

另一方面，要证明 XOR，您不仅需要证明一个论点，还必须提供另一个论点的虚假证明。

因此，根据 Curry-Howard 的解释，如果有人给你一个元素 ofXor a b并且你能够从中提取 的值a，你会得出结论b是无人居住的（即，同构于Void）。相反，如果您能够提取 的值b，那么您就会知道那a是无人居住的。

的证明a是一个函数a->Void。Void给定 的值，这样的函数将能够产生 的值a，这显然是不可能的。所以不能有 的值a。（只有一个函数返回Void，那就是 上的标识Void。）

于 2020-10-19T17:15:14.550 回答