假设存在一个实现停止问题的 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. 是正确的。
The question's presupposition is, of course, false.
But we should at least be sure that
fHalt undefined = halt (undefined + 1)
just because we expect the beta-law to hold without exception.
Now, if this hypothetical halt existed, it should be able to detect that
undefined + 1 = undefined
shouldn't it? Of course, it wouldn't be Haskell which figures that out, but the magic in the halt function.
Haskell 对预定义的操作符使用严格的求值 - 也就是 (+)。
不，一般不会。但是，特别是+在Integer实现上是严格的并且您的进一步推理有效（当然，由于它是从halt存在的错误前提开始的，所以它不太有用）。