haskell - Agda 的停机问题？

Question

我正在研究一篇试图在 Agda 中实现他们的 Haskell 代码的论文。他们想通过说让 bot 成为这样一个程序来制定停机问题，这样对于任何数据类型 a:

bot :: a
bot = bot

他们继续定义

data S = T

所以停机问题可以表示为:

函数发散:S → S由

定义

diverges(T)= bot
diverges(bot)= T

不可计算，因此无法用我们的语言定义

我尝试在 Agda 中将其实现为:

data S : Set where
  ⊤ : S

⊥ : _
⊥ = ⊥

diverges : S → S
diverges ⊤ = ⊥
diverges ⊥ = ⊤

当我尝试加载它时，Agda 说 diverges ⊥ = ⊤ 是一个无法访问的子句。这是我应该得到的错误还是我只是错误地实现了 Haskell 代码？

Answer 1

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

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

像这样奇怪的循环论证是理解停机问题的核心，因此您正在阅读的论文可能会包含其中的许多论点。

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