无法在 C 中添加自然数的后果答案

【问题标题】：Consequences of inability to add natural numbers in C无法在 C 中添加自然数的后果
【发布时间】：2011-12-01 21:23:46
【问题描述】：

在 System F 中，我可以使用 Church 数字定义真正的总加法函数。

在 Haskell 中，由于底部值，我无法定义该函数。例如，在 haskell 中，如果 x + y = x，那么我不能说 y 为零 - 如果 x 是底部，对于任何 y，x + y = x。所以加法不是真正的加法，而是它的近似值。

在 C 中我无法定义该函数，因为 C 规范要求所有内容都具有有限的大小。所以在 C 中可能的近似值甚至比在 Haskell 中更糟糕。

所以我们有：

在 System F 中可以定义加法，但不可能有完整的实现（因为没有无限的硬件）。

在 Haskell 中无法定义加法（因为底部），也不可能有完整的实现。

在 C 语言中，不可能定义总加法函数（因为所有事物的语义都是有界的），但兼容的实现是可能的。

因此，所有 3 个正式系统（Haskell、System F 和 C）似乎都有不同的设计权衡。

那么选择一个而不是另一个的后果是什么？

【问题讨论】：

如果不是“没有无限的硬件”，那么“C 规范要求一切都具有有限的大小”是什么意思？ C 确实将动态分配的内存块限制为小于 pow(2, 8 * sizeof(size_t)) 字节，但如果您的硬件有足够的内存，您可以将它们链接起来。
System F Turing 完成了吗？如果是这样，我认为您无法避免 x + y = x 问题，因为 y 可以无限递归。
@Owen：系统 F 不是图灵完备的；有很多方法可以编码一些复杂的递归程序，但它仍然是强规范化
@acfoltzer 在这种情况下，我会说这是一个重大的权衡；）
@MikeSamuel 我不能无限链接这些，因为指针大小是固定的。所以我不能将 C 中的任意整数表示为任意长度的链表——语义总是施加限制。相比之下，SystemF 或 Haskell 的语义没有指定限制。

标签： haskell types language-design turing-complete

【解决方案1】：

Haskell

这是一个奇怪的问题，因为您使用的是 = 的模糊概念。 _|_ = _|_ 仅在域语义级别“持有”（即使那样你也应该真正使用 ⊑）。如果我们区分域语义级别可用的信息和语言本身的相等性，那么说True ⊑ x + y == x --> True ⊑ y == 0 是完全正确的。

问题不是加法，问题也不是自然数——问题只是区分语言中的相等性和语言语义中关于相等性或信息的陈述。如果没有底部的问题，我们通常可以使用朴素的等式逻辑来推理 Haskell。对于底部，我们仍然可以使用等式推理——我们只需要更复杂地处理我们的等式。

在优秀论文“Fast and Loose Reasoning is Morally Correct”中对全部语言和通过提升它们定义的部分语言之间的关系进行了更全面、更清晰的阐述。

您声称 C 要求所有内容（包括可寻址空间）都具有有限的大小，因此 C 语义对可表示的自然的大小“施加了限制”。并不真地。 C99 standard 说明如下：“任何指针类型都可以转换为整数类型。除非前面指定，否则结果是实现定义的。如果结果不能用整数类型表示，行为未定义。结果不必在任何整数的值范围内类型。” 基本原理文档进一步强调“C 现在已经在广泛的体系结构上实现。虽然其中一些体系结构具有统一指针，其大小与某些整数类型相同，最大可移植代码不能假定不同指针类型和整数类型之间有任何必要的对应关系。在某些实现中，指针甚至可以比任何整数类型都宽。”

如您所见，没有明确假设指针的大小必须是有限的。

【讨论】：

@nponeccop：我的观点是，在语义上，Haskell 中的加法仍然是“真正的加法”——只是它是在提升的域上定义的。如果这不是您要寻找的，那么您的问题实际上只是关于总函数式编程的权衡。参见 Turner (2004) citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.5271 和引用它的论文，并参见，例如，这个 ltu 讨论：lambda-the-ultimate.org/node/3076
当你说有限环算术与 Peano 算术相同并且有限环中的加法只是在有限域上定义的加法时，我敢打赌数学家会嘲笑你。我的问题是在 N、提升 N 和有限环或其他合理的有限“近似”中工作时推理相对容易。

【解决方案2】：

您有一套理论作为框架来进行推理；有限现实、Haskell 语义、系统 F 只是其中之一。

您可以为自己的工作选择合适的理论，从头开始构建新的理论，或者将现有的大量理论聚集在一起。例如，您可以考虑一组始终终止的 Haskell 程序并安全地使用无底语义。在这种情况下，您的添加将是正确的。

对于低级语言，可能需要考虑插入有限性，但对于高级语言，省略这些是值得的，因为更抽象的理论允许更广泛的应用。

在编程时，您使用的不是“语言规范”理论，而是“语言规范+实现限制”理论，因此在语言规范或语言实现中存在内存限制的情况之间没有区别。当您开始在语言语义框架中构建纯理论结构时，没有限制就变得很重要。例如，您可能想证明一些程序等价或语言翻译，并发现语言规范中的每一个不需要的细节都会给证明带来很大的痛苦。

【讨论】：

【解决方案3】：

相信你一定听过这样一句格言：“理论上，理论与实践没有区别，但在实践中是有区别的。”

在这种情况下，理论上存在差异，但所有这些系统都处理相同的有限数量的可寻址内存，因此在实践中没有区别。

编辑：

假设您可以在这些系统中的任何一个中表示自然数，那么您可以在其中任何一个中表示加法。如果您担心的约束阻止您表示自然数，那么您不能表示 Nat*Nat 加法。

将自然数表示为一对（最大位大小的启发式下限和延迟评估的位列表）。

在 lambda 演算中，您可以将列表表示为一个函数，该函数返回一个函数，以 true 调用返回 1 位，以 false 调用返回一个对 2 位执行相同操作的函数，依此类推。

然后，加法是应用于传播进位位的这两个惰性列表的 zip 的操作。

您当然必须将最大位大小启发式表示为自然数，但如果您仅实例化位数严格小于您所表示的数字的数字，并且您的运算符不会破坏该启发式，那么位大小在归纳上是一个比您要操作的数字更小的问题，因此操作终止。

关于解决边缘情况的难易程度，C 对你的帮助很少。您可以返回特殊值来表示上溢/下溢，甚至尝试使它们具有传染性（如 IEEE-754 NaN），但如果您未能检查，您将不会在编译时收到投诉。您可以尝试重载信号 SIGFPE 或类似陷阱问题的东西。

我不能说 y 是零 - 如果 x 是底部，x + y = x 对于任何 y。

如果您希望进行符号操作，Matlab 和 Mathematica 是用类似 C 和 C 的语言实现的。也就是说，python 有一个优化良好的 bigint 实现，可用于所有整数类型。不过，它可能不适合表示非常大的数字。

【讨论】：

问题不在于计算能力 - 主要在于编程过程中考虑边缘情况的难易程度。
@nponeccop，我仍然不确定你要什么。请查看我的编辑。