在Agda停止问题？
我正在通过一篇论文试图在Agda中实现他们的Haskell代码。 他们想要制定停机问题，让let bot成为一个程序，以便对于任何数据类型a ：
bot :: a
bot = bot
他们继续定义
data S = T
所以停机问题是这样说的：
功能diverges : 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中的可计算函数必须为更多定义的输入提供更多定义的输出，并且⊤被认为比⊥更加明确（这是一个实际值，与“this is undefined”的符号相反）。