coq - 为什么基于微积分的语言如此多地使用 Setoid？

Question

一项发现 Setoids 广泛用于 Agda、Coq 等语言……事实上，Lean 等语言认为它们可以帮助避免“Setoid Hell”。首先使用 Setoids 的原因是什么？转向基于HoTT（例如立方体Agda）的扩展类型理论是否会减少对Setoids的需求？

Answer 1

正如夏立尧的回答所描述的，当我们没有或不想使用商时，就会使用 setoids。

在 HoTT 书和精益商中，（基本上）公理化了。Lean 和 HoTT 书之间的一个区别是后者有更多更高的归纳类型，而 Lean 只有商和（常规）归纳类型。如果我们只关注商（在 HoTT 书中设置商），它在 Lean 和 Book HoTT 中的工作方式相同。在这种情况下，您只需假设给定一个类型A和一个等价物R，A您就有一个商Q和一个[-] : A → Q具有属性的函数∀ x y : A, R x y → [x] = [y]。它具有以下消除原则：要g : Q → X为某种类型X（或XHoTT 中的 hSet）构造函数，我们需要一个f : A → X可以证明的函数∀ x y : A, R x y → f x = f y。这带有计算规则，即∀ x : A, g [x] ≡ f x（这是 Lean 和 Book HoTT 中的定义平等）。

这个商的主要缺点是它破坏了规范性。规范性表明（例如）自然数中的每个封闭项（即没有自由变量的项）都归一化为零或某个自然数的后继项。这个商打破规范的原因是我们可以将消除原理应用于=一个商中的新等式，并且这样的术语不会减少。精益的观点是这无关紧要，因为在所有我们关心的情况下，我们仍然可以证明相等，即使它可能不是定义上的相等。

立方类型理论有一种奇特的方式来处理商，同时保持规范性。在 CTT 中，相等的工作方式不同，这意味着可以在保持规范性的同时引入更高的归纳类型。CTT 的潜在缺点是类型论要复杂得多，并且您必须接受 HoTT（尤其是放弃证明无关性）。

Answer 2

[Lia-yao Xia 和 Floris van Doorn 的答案都很出色，所以我会尝试用更多信息来补充它们。]

另一种观点是，商虽然在经典数学中被大量使用，但可能并没有那么大。不取商但坚持 Groupoids正是非交换几何的起点！它告诉我们，有些商的行为非常糟糕，我们想做的最后一件事（在这些情况下！）就是实际商。但是，如果您使用“正确”的工具对其进行处理，那么事情本身并没有那么糟糕，甚至还不错。

可以说，它也深深植根于所有范畴论中，其中没有人对等价对象进行商法。在范畴论中使用“骨架”被认为是低俗的。严格也是如此，还有许多其他事情，所有这些都归结为试图压扁那些最好保持原样的事情，因为它们根本没有害处。我们只是习惯于希望“独特性”反映在我们的表现中——我们应该克服这种情况。

Setoid 地狱的出现不是因为必须证明某些连贯性（您需要证明它们以表明您具有适当的等价性，并且每当您在原始表示而不是在商版本上定义函数时再次证明）。当您在定义不可能“出错”的函数时被迫一次又一次地证明这些连贯性时，就会出现这种情况。所以 Setoid 地狱实际上是由于没有提供适当的抽象机制造成的。

换句话说，如果你正在做足够简单的数学，其中商表现良好，那么应该有一些自动化可以让你顺利地工作。目前，在类型理论中，正在研究到底会是什么样子。Floris 的回答很好地概述了一个陷阱是什么：在某些时候，您放弃了计算将是良好的行为，从那时起，被迫通过证明来做所有事情。

Answer 3

理想情况下，我们当然希望能够将任意等价关系视为莱布尼茨等式 ( eq)，从而能够在任意上下文中进行重写。这意味着通过等价关系定义类型的商。

我不是该主题的专家，但我一直在想同样的问题，我认为对 setoids 的依赖源于商在类型理论中仍然是一个鲜为人知的概念。

1. 当我们没有/不想要商类型时，Setoid Hell 就是我们陷入困境的地方。
2. 我们可以公理化商类型，我相信（我可能弄错了）这就是精益所做的。
3. 我们可以开发一种可以自然表达商的类型理论，这就是 HoTT/Cubical TT 对更高归纳类型所做的事情。

此外，商类型（或我对它们的天真想象）迫使我们以一种可能不太理想的方式将程序和证明打包在一起：两个商类型之间的函数是一个普通函数，以及它尊重潜在等价性的证明关系。虽然在技术上可以做到这一点，但这种编程和证明的交错可以说是不可取的，因为它使程序不可读：人们经常试图将程序和证明保持在两个完全独立的世界中（这样就要求 setoids，保持类型与其等价关系分开） ，或者改变一些表示，使程序和证明是同一个实体（所以我们可能甚至不需要首先明确地推理等价）。