议程中的问题

Question

我正在通过一篇论文试图在Agda中实现他们的Haskell代码。他们想要将停止问题表述为让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代码不正确?

Answer 1

您的项目可能无法工作，因为Agda不是图灵完备的语言。首先，它只允许总的函数，所以它不能模拟任何可能不会停止的计算。这意味着它甚至不能在图灵机上模拟完整的计算，因为图灵机可能无法停止。因此，论文中的所有程序都不太可能在Agda中实现。

事实上，通过一个简单的对角线参数，甚至不可能在Agda中编码所有的总计算。想象一下下面的算法:"检查一个文本文件并确定它是否是合法的议程。如果不是，输出空字符串;如果是，就在同一个文本文件上运行Agda程序，并在输出末尾添加一个空格。"这是一个定义良好的算法;最复杂的是"确定它是否是合法的Agda"one_answers"运行该Agda程序"，而做这些事情的程序肯定存在。但是没有Agda程序可以实现它，因为任何候选程序在运行自己的源代码时会给出不同的输出。所有的语言都有类似的参数。

像这样奇怪的圆形扭曲论点是理解停机问题的核心，所以你正在阅读的论文可能会包含许多这样的论点。

顺便说一下，函数diverges在Haskell中是不能定义的。Haskell中的可计算函数必须为更多定义的输入提供更多定义的输出，而⊥被认为是定义更多的(它是一个实际值，而不是表示"this is undefined"的符号)。