Nonlinear Arithmetic with SMTLIB Division is Undecidable
该论文证明，SMTLIB 标准中定义的非线性实算术（NRA）是不可判定的，因为其将除以零视为未解释函数的处理方式使得不可判定的整数算术问题得以被编码。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象你是一名侦探，试图利用一套极其严格的规则来解开一个谜团。在计算机科学领域，这些规则被称为“理论”，它们帮助计算机判断一个数学谜题是否有解。
本文讨论的是一组特定的规则，称为非线性实数算术（NRA）。你可以将其想象为一种使用实数（如 3.14、-5 或 0.001）进行的游戏，在其中你可以对这些数字进行加、减、乘、除运算。
打破游戏的“魔法”规则
长期以来，数学家们认为这个游戏是完全可解的。如果你给计算机一个使用这些数字的谜题，它最终总能回答：“是的，有解”或者“不，没有解”。
然而，作者 Dejan Jovanović 在官方规则手册（SMTLIB 标准）中发现了一个隐藏的陷阱。这个陷阱在于规则如何处理除以零。
在常规数学中，除以零是一个绝对的“禁止”。但在这本特定的计算机规则手册中，规则规定：“如果你除以零，我们不在乎答案是什么。它可以是任何东西，只要它在非除以零的情况下表现得像一个正常数字。”
作者称此为未解释函数。使用一个类比：想象一台自动售货机，对于你购买的每一种零食，它都能完美运作。但如果你尝试购买“零号零食”，机器并不会崩溃；相反，它会吐出某种东西——可能是一块糖果，可能是一块石头，也可能是一团云。规则并没有告诉你它会吐出什么；它们只是说：“它会吐出某种东西。”
这如何使游戏变得无解
本文认为，这种针对除以零的“随意”规则是开启混乱之门的钥匙。
以下是简化后的逻辑：
- 目标：作者希望证明，如果你拥有这种“魔法”除法法则，你就可以诱骗计算机去解决整数谜题（即包含 1、2、3 等整数的谜题）。
- 问题：众所周知，计算机无法完美地解决所有整数谜题（这被称为希尔伯特第十问题）。这就像试图在一堆不断无限增长的干草堆中寻找一根针。
- 诡计：作者表明，通过利用这种“魔法”除以零，你可以构建一座数学桥梁。你可以利用这个除法诡计，将一个困难的整数谜题转化为一个实数谜题。
- 类比：想象你有一段用只有人类能理解的语言（整数）写成的秘密代码。你制造了一台机器（除法诡计），将这段代码翻译成计算机能理解的语言（实数）。由于计算机的语言中存在这种“魔法”除以零规则，计算机可能会意外地破解人类代码。
- 结果：既然我们知道计算机无法解决所有整数谜题，而这种诡计让它们尝试用实数去解决整数谜题，这就意味着计算机也无法解决所有实数谜题。这个游戏变得不可判定了。
“向下取整”函数的类比
为了证明这一点，作者使用了一个巧妙的技巧。他们表明，如果你拥有这种“魔法”除法，你就可以迫使计算机表现得像一个向下取整函数（一个将数字向下舍入到最接近的整数的函数，例如将 3.9 变为 3）。
一旦计算机能够向下舍入数字，它就可以开始计数整数。一旦它能够计数整数，它就可以尝试解决那些不可能解决的整数谜题。既然这些谜题在一般情况下无法解决，那么包含这种除法规则的整个实数数学体系在一般情况下也就变得无法解决。
这对现实世界意味着什么（根据本文）
本文并未谈论未来的人工智能或医疗用途。它专注于当前计算机基准测试（测试问题）的状态：
- 陷阱：SMTLIB 库（一个用于测试计算机的巨大数学谜题集合）中的许多现有测试问题都使用了带变量的除法（如
x / y）。如果y恰好为零，这些谜题就会落入“不可判定”的陷阱。 - 解决方案？ 作者提出了两种修改规则手册的方法：
- 指定特定答案：规定除以零总是等于某个特定数字（如 0 或 1），就像某些计算机系统处理二进制数那样。
- 拆分游戏：为涉及变量除法的问题创建一个全新的独立类别，并将“安全”类别保留给仅涉及已知数字（常量）除法的问题。
核心结论
本文声称，一条关于计算机如何处理“除以零”的看似无害的特定规则，意外地破坏了计算机解决所有涉及实数的数学问题的能力。它通过允许计算机偷偷解决那些本不该能解决的问题，将一个可解的游戏变成了一个不可解的游戏。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。