gpt4 book ai didi

haskell - Agda 的停机问题?

转载 作者:行者123 更新时间:2023-12-05 08:12:08 25 4
gpt4 key购买 nike

我正在研究一篇试图在 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/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com