haskell - 停止 Agda 中的问题？

Answer 1

您的项目可能无法运行，因为 Agda 不是图灵完备的语言。一方面，它只允许总函数，因此它不能对任何可能不会停止的计算进行建模。这意味着它甚至无法对图灵机上的完整计算进行建模，例如，因为图灵机可能无法停止。所以论文中的所有程序都不太可能在 Agda 中实现。

事实上，在 Agda 中，甚至不可能通过一个简单的对角参数来编写所有总计算。想象一下下面的算法：“检查一个文本文件并确定它是否是合法的 Agda。如果不是，则输出空字符串；如果是，则在同一个文本文件上运行该 Agda 程序，并在末尾添加一个空格输出。” 这是一个定义明确的算法；大部分复杂性在于“确定它是否是合法的 Agda”和“运行那个 Agda 程序”，而且确实存在执行这些操作的程序。但是没有 Agda 程序可以实现它，因为任何候选程序在其自己的源代码上运行时都会给出不同的输出。任何总语言都受到类似论点的影响。

像这样奇怪的循环论证是理解停机问题的核心，所以你正在阅读的论文可能包含许多这样的论证。

顺便说一句，该函数在 Haskell 中diverges是不可定义的。Haskell 中的可计算函数必须为更多定义的输入提供更多定义的输出，并且 ⊤ 被认为比 ⊥ 更定义（它是一个实际值，而不是“这是未定义”的符号）。