haskell - 进一步滥用代数数据类型的代数 - 为什么这有效？

Question

所以我一直在阅读如何将 ADT 转换为类似于实数的内容并操作它们，在 this SO question 之类的页面上和 this 3 part series和 especially this .

最后一个链接的“问题”部分引起了我的注意，我试图解决 Nat即使文章指出这是不可能的。

Nat = 1 + Nat
Nat - Nat = 1
Nat(1 - 1) = 1
Nat = 1 / (1 - 1)

这可能看起来完全是无稽之谈，因为我只是除以 0(您可能是对的)，但是如果您阅读任何这些链接或类似内容，那么您会注意到它看起来与列表的定义非常相似。

List(x) = 1 / (1 - x)

所以你可以像 Nat = List(1) = 1 + 1 + 1 + ... 这样写 Nat ，这正是您通过在起始方程中重复替换得到的结果。这也相当于在 Haskell 中定义这样的自然数:

type Nat = [()]

这绝对是自然数的有效编码，其中 0 = []和 S(N) = () : N .

所以我的问题是我怎么得到一个有效的结果呢？我只是除以零。更不用说起始方程本身就是一个矛盾。

那么我怎么会在这结束时得到一些有意义的东西呢？这只是纯粹的巧合，还是在这种情况下以某种方式定义的除以 0 有意义？

Answer 1

自 Nat是无限的，你真的不能用 Nat - Nat = Nat ⋅ (1 - 1) = Nat ⋅ 0 = 0 .区别Nat - Nat是某个有限数，正如它是，而 Nat显然是无限的。所以这个1 - 1不是真正的零，它更像是 nonstandard analysis 中的一个无穷小值.如果你除以一个无穷小的东西，你得到的东西会很大(无穷大，确实......废话)，但你不会完全被零除。

事实上，我认为你问的悖论可以看作是“证明Nat是无限的”——因为如果它是有限的，你就会除以零。

当然，除了你不能真正用这种类型的算术证明任何东西……这是一种有趣的消遣，但不是真正可靠的数学。