Search code examples
haskellhalting-problemmonotone

non-strict evaluation in Haskell regarding halting-prob

Suppose there exists a Haskel-function realizing the halt-problem:

halt :: Integer->Bool

that evaluates to True if x is defined and to False otherwise.

Let's assume we are calling this function in Haskell in another function as

fHalt x = halt (x+1)

I'm wondering what would happen in this situation and if fHalt is monotone. 2 possible answers arise for me:

  1. Haskell uses strict-evaluation for pre-defined operators - i.e. also for (+). If fHalt is now evaluated with BOT, my guess is that BOT+1 has to be evaluated first (resulting in BOT) and thus the overall evaluation does not terminate and also results in BOT.

  2. If somehow Haskell would determine that the inner (x+1) does not terminate (which is impossible due to the halt-problem) the result would be False and fHalt would violate monotonicity.

At this point, I'm irritated since my question already implied a non-realizable halt-function defined in Haskell. Though I would suppose that answer 1. is correct.

Solution

  • 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.