Haskell中整数的非整数居民答案

【问题标题】：Non-integer inhabitants of integers in HaskellHaskell中整数的非整数居民
【发布时间】：2012-01-18 10:58:17
【问题描述】：

Haskell 中定义为data Peano = Zero | Succ Peano 的Peano 自然数是相当奇怪的野兽：除了普通的自然数和底值之外，其中还有一个“无限整数”inf = Succ inf。

还有其他Peano 类型的居民吗？这个无限数有名字吗？

【问题讨论】：

标签： haskell types integer infinity

【解决方案1】：

嗯，有Succ _|_、Succ (Succ _|_) 等。不过，您可能已将它们包含在“底部值”中。 inf = Succ inf 通常称为infinity 或omega（作为自然数的序数）。

【讨论】：

但是因为inf = Succ inf，它不可能是自然数的序数，对吧？它将同时是 ω 和 ω+1。 inf 不是更类似于 aleph-null，即 N 的基数吗？
@larsmans 取决于您是将Succ n 解释为n+1 还是1+n、1 + ω = ω /= ω + 1。

【解决方案2】：

它们并不奇怪，它们只是 Coinductive 自然物。抛开⊥的问题，我们可以在这里定义自然数类型为Zero或Succ应用于自然数。归纳定义将假定一个明确定义的结束，即任何数字都从 Zero 构造函数开始。共归纳定义只是说给定任何自然数，它要么是Zero，要么我们可以去掉外部的Succ，得到另一个自然数。

看似细微的区别在于，共归纳定义包括无穷无尽的Succ 构造函数系列，这确实是无限的真实表示。这很有意义，因为归纳定义是关于确保递归将达到定义良好的基本情况，而归纳定义是关于确保始终有一个定义良好的下一步可用。

由于数据构造函数是懒惰的，所以在 Haskell 中，协推解释很方便，并且在某些方面是强制性的。

所以，正如 Daniel Fischer 所说，这个无限数确实是无穷大，或者如果您需要指定哪个无穷大，则为 ω。它只是一个共归纳无穷，很像更常见的无穷列表。

如果您通过教堂编码来考虑自然数，有限数意味着“将此函数迭代 N 次”； ω 的意思是“无限期地迭代这个函数”。

【讨论】：

这通常被称为“扩展自然数”，它经常以一种非常简单的方式出现：ncatlab.org/nlab/show/extended%20natural%20number%20system, golem.ph.utexas.edu/category/2008/12/…
@sclv：作为一名 Haskell 程序员，我最喜欢的事情是人们说某事“直截了当”，然后用指向 nLab 的链接进行说明，哈哈。但是，是的，我以前读过那些，它们很有趣。
哈哈我想我有一个“直截了当”的移动目标，我用它来表示“我实际上可以稍微挥手并解释一下”，就像人们使用“琐碎”来表示“如果有足够的时间，我相信我可以证明这一点。”
@sclv：我喜欢费曼根据观察数学学生对“微不足道”的定义，大致是“任何已经被证明或显然可以通过努力证明的东西”。 “琐碎”的反义词大概是“一个悬而未决的问题”。