如果“任一个”可以是“左”或“右”，但不能同时是“左”或“右”，那么为什么在Curry-Howard对应中它对应于OR而不是XOR？

问题描述

当我问this question时，答案之一（现已删除）暗示Curry-Howard correspondence中的类型List<string> listA ; /* the list is not actually a string,but for our test case let's use this (populated with M=31 items for example)*/ List<string> listB = new List<string>(); int N = 3; for(int i=0;i<listA.Count;i++){ if(i%N == 0)listB.Add(listA[i]); } 对应于XOR，而不是OR，因为它不能Either和Left同时出现。

真相在哪里？

解决方法

如果您有一个P类型的值，并且 有一个Q类型的值（即，您既有P的证明，又有证明Q），那么您仍然可以提供类型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，因为正如我所说，它不排除两个部分都有证明的情况。另一方面，Daniel Wagner proposes in this answer更接近XOR。

就其可能的见证人而言，

Either有点像“异或”。另一方面，这就像 inclusive 或当您考虑是否可以在以下四种可能的情况下实际创建证人：具有P的证明和对Q的反驳，具有Q和P的对立，既有两个证明，又有两个对立。 ^[1] 当你有两个P的证明时，可以构造类型Either P Q的值和Q（类似于包含OR），您无法将这种情况与仅P具有证明或仅Q具有仅使用类型为Either P Q（类似于异或）的值的情况区分开来。 。另一方面，丹尼尔·瓦格纳（Daniel Wagner）的解决方案类似于 构造和解构的异或。

值得一提的是，These更明确地表示了两者都有证明的可能性。 These在构造和解构方面类似于 inclusive 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）的解决方案：

• 构造：构造类型为Xor A B的值时，必须提供A或B中的一个正好与驳斥另一个。这类似于“异或”。除非您反驳A或B 并证明另一个，否则无法构造此的值。一个特别重要的事实是，如果您同时拥有A和B的证明，并且您没有驳斥以下任何一种，则不能构造该类型的值它们（不同于 inclusive OR）。

• 销毁：当对类型为Xor A B的值进行模式匹配时，您总是具有其中一种类型的证明和一种反驳其他的。它永远不会为您提供两者的证明。这是从其定义开始的。

对于IOR：

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

• 销毁：由于您拥有B和A中至少一个的证明的三种可能情况是准确由B表示，并且每个都有一个单独的构造函数（并且这些构造函数之间没有重叠），您将始终确切地知道 哪个IOR和A是对的，通过对它的模式匹配它是假的（如果适用）。

B上的图案匹配

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

IOR

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

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

---

^[1] 当您认为某些陈述无法确定并因此无法为其构造证明或反驳时，这会变得更加复杂。

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

,

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

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

问题是：假设我知道 P 为真的[对应于]的值的类型（我将这种类型称为P），并且我知道证据的类型 Q 是真的（我称这种类型为Q），那么命题 R = P 的证据的类型是什么还是 Q ？

有两种方法可以证明 R ：我们可以证明 P ，或者我们可以证明 Q 。我们可以证明两者，但这将是多余的工作。

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

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

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

如果我们可以证明 P 和 Q ，这为我们提供了证明 P 或 Q 的方法。因此Either不能对应于xor。

---

P XOR Q 是什么类型？

在这一点上，我要说的是，这种建设性逻辑的否定有点令人讨厌。

让我们将问题转换为我们理解的事情，而不是我们不了解的简单事情：

P XOR Q =（ P AND（不是 Q ））或（ Q AND（不是 P ））

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

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

我们将这一点与我们所知道的相提并论，并得到以下命题语言的等价性：

P XOR Q =（ P AND（不是 Q ））或（ Q AND（NOT P ））=（ P AND（ Q 暗示错误））或（（表示假）和 Q ）

类型为：

type Xor p q = Either (p,q -> Void) (p -> Void,q)

,

混淆源于逻辑的布尔真值表说明。特别是，当两个参数均为True时，OR为True，而XOR为False。从逻辑上讲，这意味着证明“或”就足以证明其中一个论点。但如果另一个也为True也可以-我们不在乎。

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

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

因此，按照Curry-Howard的解释，如果有人给您一个Xor a b的元素，并且您能够从中提取a的值，则可以得出结论b是无人居住（即与Void同构）。相反，如果您能够提取b的值，那么您将知道a无人居住。

a的虚假证明是函数a->Void。给定值为Void，这样的函数将能够产生值a，这显然是不可能的。因此，不能存在a的值。 （只有一个函数返回Void，这就是Void上的标识。）