0

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.

Rodney
  • 205
  • 2
  • 7
  • 4
    Just as a side note, a solution to the halting problem has to work for _all_ inputs, but there's no problem with deciding whether a subset of inputs terminate, so for example, it's possible to verify by static analysis that `1+2` terminates. The _general_ halting problem is unsolvable, but that doesn't mean halting is never calculable. Thus you can't say it's impossible for `halt` to decide a specific case, you can only say there are cases it can't decide. – AndrewC Aug 13 '14 at 09:01
  • 1
    @AndrewC but any such function has to be defined in terms of *codes* of programs. Lambda functions are monotone in denotation and respect extensional equality. So only trivial examples of `halt` are possible in haskell. – Philip JF Aug 13 '14 at 17:42

2 Answers2

6

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.

pigworker
  • 43,025
  • 18
  • 121
  • 214
0

Haskell uses strict-evaluation for pre-defined operators - i.e. also for (+).

No, not in general. However, specifically for + on Integer the implementation is strict and your further reasoning works (of course, since it starts from a false premise that halt exists, it isn't too useful).

Alexey Romanov
  • 167,066
  • 35
  • 309
  • 487