Haskell 中关于停止问题的非严格评估答案

【问题标题】：non-strict evaluation in Haskell regarding halting-probHaskell 中关于停止问题的非严格评估
【发布时间】：2014-10-06 11:09:04
【问题描述】：

假设存在一个实现停止问题的 Haskel 函数：

halt :: Integer->Bool

如果定义了 x，则为 True，否则为 False。

假设我们在 Haskell 中的另一个函数中调用这个函数

fHalt x = halt (x+1)

我想知道在这种情况下会发生什么，如果 fHalt 是单调的。我有 2 个可能的答案：

Haskell 对预定义的运算符使用严格求值 - 即也用于 (+)。如果现在用 BOT 评估 fHalt，我的猜测是必须首先评估 BOT+1（导致 BOT），因此整体评估不会终止，也会导致 BOT。
如果 Haskell 以某种方式确定内部 (x+1) 不会终止（由于停止问题，这是不可能的），则结果将为 False 并且 fHalt 将违反单调性。
李>

此时，我很生气，因为我的问题已经暗示了 Haskell 中定义的不可实现的停止功能。虽然我认为答案 1. 是正确的。

【问题讨论】：

顺便说一句，停止问题的解决方案必须适用于所有输入，但决定输入的子集是否终止没有问题，例如，可以通过静态分析验证1+2 终止。 general 停机问题是无法解决的，但这并不意味着停机永远无法计算。因此你不能说halt不可能决定一个具体的案件，你只能说有些案件它不能决定。
@AndrewC 但任何此类功能都必须根据程序的代码来定义。 Lambda 函数在外延上是单调的并且尊重外延相等。所以在haskell中只有halt的简单例子是可能的。

【解决方案1】：

这个问题的预设当然是错误的。

但我们至少应该确定

fHalt undefined = halt (undefined + 1)

只是因为我们希望 beta 定律毫无例外地成立。

现在，如果这个假设的halt 存在，它应该能够检测到

undefined + 1 = undefined

不应该吗？当然，解决这个问题的不是 Haskell，而是 halt 函数的魔力。

【讨论】：

【解决方案2】：

Haskell 对预定义的运算符使用严格求值 - 即也用于 (+)。

不，一般来说不是。但是，特别是对于 Integer 上的 +，实现 is 是严格的，并且您的进一步推理有效（当然，因为它始于 halt 存在的错误前提，所以它不太有用)。

【讨论】：