如果“任一个"可以是“左"或“右"，但不能同时是“左"或“右"，那么为什么在Curry-Howard对应中它对应于OR而不是XOR? [英] If Either can be either Left or Right but not both, then why does it correspond to OR instead of XOR in Curry-Howard correspondence?

问题描述

当我问此问题时，现在已删除的答案之一，表明

When I asked this question, one of the answers, now deleted, was suggesting that the type Either corresponds to XOR, rather than OR, in the Curry-Howard correspondence, because it cannot be Left and Right at the same time.

真相在哪里?

推荐答案

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

The confusion stems from the Boolean truth-table exposition of logic. In particular, when both arguments are True, OR is True, whereas XOR is False. Logically it means that to prove OR it's enough to provide the proof of one of the arguments; but it's okay if the other one is True as well--we just don't care.

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

In Curry-Howard interpretation, if somebody gives you an element of Either a b, and you were able to extract the value of a from it, you still know nothing about b. It could be inhabited or not.

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

On the other hand, to prove XOR, you not only need the proof of one argument, you must also provide the proof of the falsehood of the other argument.

因此，按照Curry-Howard的解释，如果有人给您Xor a b的元素，并且您能够从中提取a的值，则可以得出结论:b是无人居住的(即同构)到Void).相反，如果您能够提取b的值，那么您就会知道a是无人居住的.

So, with Curry-Howard interpretation, if somebody gives you an element of Xor a b and you were able to extract the value of a from it, you would conclude that b is uninhabited (that is, isomorphic to Void). Conversely, if you were able to extract the value of b, then you'd know that a was uninhabited.

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

The proof of falsehood of a is a function a->Void. Such a function would be able to produce a value of Void, given a value of a, which is clearly impossible. So there can be no values of a. (There is only one function that returns Void, and that's the identity on Void.)

这篇关于如果“任一个"可以是“左"或“右"，但不能同时是“左"或“右"，那么为什么在Curry-Howard对应中它对应于OR而不是XOR?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！