Home Articles

在Haskell中关于停止概率的非严格评估

Asked
Viewed 788 times
0

假设存在一个实现停止问题的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 Answers

  • 6

    当然,问题的预设是错误的 .

    但我们至少应该确定

    fHalt undefined = halt (undefined + 1)
    

    仅仅因为我们期望beta法律毫无例外地持有 .

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

    undefined + 1 = undefined
    

    不应该是哈斯克尔那个想出来的,但是 halt 函数中的魔力 .

  • 0

    Haskell对预定义的运算符使用严格评估 - 也就是() .

    不,不是一般的 . 但是,特别是对于 Integer Integer ,实施是严格的,你的进一步推理工作(当然,因为它从 halt 存在的错误前提开始,它不是太有用) .

Related