什么类型对应于类型论中的 xor b？

Posted 2023-05-08

【中文标题】什么类型对应于类型论中的 xor b？

【英文标题】：What type corresponds to a xor b in type theory?

【发布时间】：2021-01-30 10:34:37

【问题描述】：

在Category Theory 8.2 的末尾，Bartosz Milewski 展示了一些逻辑、范畴论和类型系统之间对应关系的例子。

我在徘徊什么对应于逻辑异或运算符。我知道

a xor b == (a ∨ b) ∧ ¬(a ∧ b) == (a ∨ b) ∧ (¬a ∨ ¬b)

所以我只解决了部分问题：a xor b 对应于(Either a b, Either ? ?)。但是缺少的两种类型是什么？

看来xor怎么写其实归结为not怎么写。

那么¬a 是什么？我的理解是，如果存在a 类型的元素（至少一个），a 是合乎逻辑的。所以not a 为真，a 应该为假，即它应该是Void。因此，在我看来有两种可能：

(Either a Void, Either Void b) -- here I renamed "not b" to "b"
(Either Void b, Either a Void) -- here I renamed "not a" to "a"

但在最后一段中，我有一种感觉，我只是把狗弄错了。

（跟进问题here。）

【问题讨论】：

异或的另一种可能解释是“非同构”

@luqui 为什么？ Int 和 [Int] 不是同构的（是吗？），但它们都是有人居住的，因此都是真的，因此它们异或为假。我倒不是这样，我的错在哪里？

嗯，是的，我的错。我想我的意思是“不等价”，在逻辑意义上是等价的(A -> B) and (B -> A)。这仍然合法地符合布尔逻辑的异或，但它在直觉上比丹尼尔答案中的弱。

【参考方案1】：

否定的标准技巧是使用-> Void，所以：

type Not a = a -> Void

当a 本身是可证明无人居住的类型时，我们可以构造出这种类型的总居民；如果有a 的任何居民，我们就无法构建这种类型的总居民。听起来像是对我的否定！

内联，这意味着您对 xor 的定义类似于以下之一：

type Xor a b = (Either a b, (a, b) -> Void) -- (a ∨ b) ∧ ¬(a ∧ b)
type Xor a b = (Either a b, Either (a -> Void) (b -> Void)) -- (a ∨ b) ∧ (¬a ∨ ¬b)

【讨论】：

你的第二个版本对我来说似乎有点尴尬，因为两个Eithers 必须走相反的方向。第三种表述：Either (a, b -> Void) (b, a -> Void).

@dfeuer，你能详细说明一下吗？我不明白您是在强调一个不准确之处，还是只是在 4 个可能的选择中，丹尼尔选择的那些比其余的更好/更丑。

@Enrico，没有什么不准确的。但是用它来获得其他公式涉及到额外的案例分支以显示荒谬。