进一步滥用代数数据类型的代数 - 为什么这样做可以？

Question

我一直在阅读有关将ADT转换为类似实数并进行操作的内容，例如这个SO问题，以及这个三部曲和特别是这个。

最后一个链接的“麻烦”部分引起了我的注意，尽管文章指出这是不可能的，但我仍然试图解决其中的Nat问题。

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

如果你读过那些链接或类似的内容，你会发现这个看起来非常像列表的定义。尽管我刚刚除以0可能看起来完全无意义（你可能是对的），但是请注意这点。

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

因此，您可以像这样编写Nat：Nat = List(1) = 1 + 1 + 1 + ...，这正是在起始方程中重复替换所得到的。这也等同于在Haskell中这样定义自然数：

type Nat = [()]

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

---

那么我的问题是，我为什么能从中得到一个有效的结果？我只是除以了零。更不用说起始方程本身就是矛盾的。

那么我为什么在这个过程的末尾得到了有意义的东西？这只是纯粹的巧合还是0的除法在这种情况下被定义成有意义的呢？

- The Red Fox

---

严格来说，1 != 1*1，因此更正确的写法应该是 Nat = 1 + 1*1 + 1*1*1 + ...。 - chepner

@chepner，您能否解释一下为什么？我理解的方式是，类型形成了一个半环，其中1是*的单位元。换句话说，对于任何x，都有x * 1 = 1。因此，1和1*1是等价的。 - The Red Fox

它们是同构的，而不是等价的。有序对((), ())与() 是不同的。x * 1 == x是因为你可以无损地将值(a, ()) :: (x,())转换为a :: x，反之亦然。 - chepner

@chepner，所有这些类型的操作都是在同构意义下进行的（最好）。如果您愿意，可以将“=”解释为“同构于”。请注意，翻译后的内容应保持原意，通俗易懂，不得添加任何额外的信息。 - Reid Barton

我认为答案可能是，您只进行了一些操作，这些操作也可以使用List（x）完成，但是您使用1代替x。但是我不确定这里是否有真正的问题。 - Reid Barton

Answer 1

由于自然数集合是无限的，所以你不能真正使用“Nat - Nat = Nat ⋅ (1 - 1) = Nat ⋅ 0 = 0”。差值“Nat - Nat”是一些有限的数字，而“Nat”显然是无限的。因此，“1-1”实际上并不是零，而更像是非标准分析中的一个无穷小值。如果你把某个数除以一个无穷小量，你会得到一个发散的大数（甚至是无穷大），但你并没有遇到除以零的情况。

事实上，我认为你所问的这个悖论可以被看作是“证明了自然数集合是无限的”，因为如果它是有限的，你就会除以零。

当然，你不能用这种类型的算术来真正“证明”任何东西……这只是一种娱乐方式，而不是真正的数学。

- leftaroundabout

---

不是用这种排序方式，但是通过更仔细的排序（差分演算法之类的），你肯定可以。 - dfeuer