假设存在一个实现停止问题的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.是正确的 .
2 回答
当然,问题的预设是错误的 .
但我们至少应该确定
仅仅因为我们期望beta法律毫无例外地持有 .
现在,如果存在这个假设
halt
,它应该能够检测到它不应该是哈斯克尔那个想出来的,但是
halt
函数中的魔力 .不,不是一般的 . 但是,特别是对于
Integer
Integer
,实施是严格的,你的进一步推理工作(当然,因为它从halt
存在的错误前提开始,它不是太有用) .