我正在研究一篇试图在 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 代码?
最佳答案
您的项目可能无法运行,因为 Agda 不是图灵完备的语言。一方面,它只允许总函数,所以它不能模拟任何可能不会停止的计算。这意味着它甚至无法对图灵机上的完整计算进行建模,例如,因为图灵机可能无法停止。所以论文中的所有程序都不可能在 Agda 中实现。
事实上,通过一个简单的对角参数,甚至不可能在 Agda 中编写所有总计算。想象以下算法:“检查一个文本文件并确定它是否是合法的 Agda。如果不是,则输出空字符串;如果是,则在同一个文本文件上运行 Agda 程序,并在文件末尾添加一个空格输出。”这是一个定义明确的算法;大部分的复杂性在于“确定它是否是合法的 Agda”和“运行那个 Agda 程序”,并且确实存在执行这些操作的程序。但是没有 Agda 程序可以实现它,因为任何候选者在其自己的源代码上运行时都会给出不同的输出。任何总体语言都受到类似的争论。
像这样奇怪的循环论证是理解停机问题的核心,因此您正在阅读的论文可能会包含其中的许多论点。
顺便说一句,diverges
函数在 Haskell 中是不可定义的。 Haskell 中的可计算函数必须为更多定义的输入提供更多定义的输出,并且 ⊤ 被认为比 ⊥ 更定义(它是一个实际值,而不是“这是未定义的”符号)。
关于haskell - Agda 的停机问题?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/30547230/