path: root/proof-sketch.txt

                The Three Valued Halting Problem is Undecidable
                         Kaz Kylheku <kaz@kylheku.com>
                                January 15 2015

Abstract:

  Some researchers do not accept the conventional halting problem proof, namely
  that the halting function is not computable. A three-valued version of
  the problem has been proposed to address the alleged problems. However,
  this succumbs to the same techniques. It is shown via an informal proof
  sketch that adding a third value to the range of a halting decider
  computation, such that computations can use this third value to complain
  that they are being tricked, does not work. The proof sketch shows that such
  a third value is not total computable, which means that three-valued halting
  computations cannot reliably detect the "self-referential trickery" of the
  conventional halting problem proof.

Background:

  The halting function is a boolean-valued, two-parameter mathematical function.
  Its parameters are a program and an input. The halting function is true for a
  <program, input> pair which terminates: that is to say, if that program
  terminates when operating on that input. The halting function is false for a
  <program, input> pair when the program does not terminate when processing
  that input. The halting function is total: it provides a boolean value for
  all possible programs and inputs.

  It is not possible to create a computational function (or algorithm) which
  calculates the halting function: a computational function which is total.
  That is to say, a computational function which can examine any <program,
  input> pair, perform a calculation, and then terminate, providing an output
  value which corresponds to the halting function's value. This was
  first shown by Alan Turing[1].

  There is a proof of this which involves a trick. For any function which is
  proposed as a halting decider (a computational implementation of the halting
  function), it is possible to create a wrapper program which incorporates that
  halting decider function. The program passes a representation of itself, and
  to its input down to the halting decider, takes the return value of the
  decider, and then behaves in a way which contradicts that return value: if
  the return value is true ("the program halts on that input") then the program
  deliberately fails to halt, by entering an infinite loop. If the return value
  is false ("the program does not halt"), the program immediately halts.  By
  itself, this does not create a counterexample which proves that the halting
  decider is wrong. One more trick is needed: the program is run, with that
  program itself as its own input. At that point, the decider's return value is
  a comment on the very program which is running, and is logically contradicted
  by the behavior of that program. This contradiction shows that the halting
  decider is computing, for that test case, the wrong value, opposite to the
  halting function. If the halting function says that the program, given itself
  as input halts, the halting decider says that it does not halt, and
  vice versa.

  The proof can be sketched like this:

    program program(input) {
      function halting_decider(program, input) {
        # performs some computation and returns true or false
      }

      function main(input) {
        if (halting_decider(this_program, input))
          loop_forever
        else
          exit(0)
      }

      main(input)
    }

  The program is then invoked with itself as input so that input is this_program,
  and so halting_decider is called as halting_decider(this_program,
  this_program).   Thus the program which is executing is the program invoked on
  itself, and the decider is asked to compute whether that exact test case halts
  or not. Of course, the test case is contrived to contradict the decider.

  Every conceivable implementation of halting_decider succumbs to this trick,
  which shows that for every every attempt to make a halting decider,
  test cases can be found which break it, which shows that no function
  can compute the halting for all possible values.

  For detailed formal proofs related to the halting problem and decidability in
  general, the reader can consult [2].

Motivation:

  Some researchers disbelieve the proof of the halting problem, claiming
  that it is a contrived trick and that the test cases which are generated
  by that trick are somehow invalid, the implication being that deciders
  may be legitimately excused for not being able to to determine whether or not
  these cases halt.

  It has been proposed that a three-valued version of the halting problem
  can provide the necessary framework. Under this notion, the halting function
  is augmented to have a third possible return value, so that for each
  <program, input> pair, it assigns the value true, false or error.  The new
  error value has some meaning such as that <program, input> test case
  constitutes a test case which is trying to break the decider through some
  self-referential trick.

  This paper presents a proof sketch which suggests that the three-valued
  halting function is also not total computable. Using a more refined trick,
  three-valued halting deciders can be shown to be incorrect. For any
  halting decider, a test case can be found such that it incorrectly returns
  error in a situation when no trick is going on: a situation when that decider
  could be altered to return true or false without being contradicted.
  Or else, a test case can be found when that decider incorrectly returns
  true or false which are contradicted, failing to identify that as
  an error situation.

The Proof:

  We begin by forming a model of the three-valued decider, and argue
  that this model is completely general: any three-valued decider
  which totally computes the three-valued halting function can conform
  to this model.

  The three-valued decider has to perform some computation which tells it
  whether to return error, or whether to determine the boolean halting value.
  In other words, it has this structure:

    function halting_decider(program, input) {
      if (should_return_error(program, input)) {
        return error
      } else {
        return decide_halting(program, input) # strictly true or false
      }
    }

  The functions should_return_error and decide_halting are subroutines of
  halting_decider: they are effectively part of that function, and their
  implementation may vary among various proposed halting_deciders.

  The attack on the three-valued halting_decider looks like this:

    program program(input) {
      function halting_decider(program, input) {
        # performs some computation and returns error, true or false
      }

      function error_decider(decider, program, input) {
        # performs some computation and returns error, true or false
      }

      function main(input) {
        if (error_decider(halting_decider, program, input)) {
          switch (halting_decider(program, input)) {
          case true:
            exit(0)
          case false:
            loop_forever
          case error:
            print("incorrect error case: no contradiction is going on!")
            abort()
          }
        } else {
          switch (halting_decider(program, input)) {
          case true:
            loop_forever
          case false:
            exit(0)
          case error:
            print("correct error case: contradiction is being perpetrated!")
            abort()
          }
        }
      }

      main(input)
    }

  As before, the program is invoked on itself as input.

  Here is how this setup differs from the two-valued halting problem proof.

  There is a now a new function error_decider. Whereas the two-valued proof
  uses a boiler-plate wrapper program that easily produces invalid test
  cases upon the mere insertion of the halting decider, the three-valued proof
  requires the attacker to not only insert the halting decider under test, but
  to perform a search for a suitable error_decider function. When a suitable
  error_decider is found, then when the resulting program is invoked on itself,
  the halting_decider is shown to be erroneous on that input case.

  What is a suitable error_decider? The suitable error_decider is a function
  which, for at least the relevant input arguments required in the test case,
  produces the same result as the halting_decider's should_return_error
  subroutine.

  In the case when error_decider(halting_decider, program, input)  happens to
  produce the same value as should_return_error(program, input), the
  halting_decider calculates the incorrect value.

  In this situation, should_return_error might return true, indicating
  to halting_decider that it should return the error code, because a trick is
  supposedly being instigated.  But if that is so, then the wrapper program's
  error_decider also returns true, causing the main function to execute the
  consequent branch of the if statement, in which no trickery is going on: the
  true value maps to termination, and false to non-termination.  The decider's
  error case ends up here and is reported as being incorrect.  On the other
  hand, if should_return_error indicates false, then the halting_decider will
  return true or false instead of error. But error_decider also returns false,
  and so the halting_decider's true or false value is routed to the second
  switch statement, in the antecedent "else" branch of the if inside main.
  In that statement, the true or false is met with contradicting behavior,
  showing it to be erroneous, similarly to the situation in the two-valued
  halting proof.

  All that is left is question: can an error_decider always be found
  to attack any possible halting_decider?  This is true because halting_decider
  has to compute somehow whether or not to return error. That computation
  corresponds to a function (which we modeled as should_return_error: a
  subroutine of the halting_decider).

  Now, a function is a finite entity chosen from a countably infinite
  enumerable set (the set of all possible functions).

  The attacker simply has to enumerate through the sequence of all possible
  functions that are suitable as error_decider, and keep re-generating the
  program with each successive choice of function.  This search is
  guaranteed to eventually find an error_decider function which matches the
  computation of the halting_decider's should_return_error function---at least
  on the relevant arguments, if not the entire argument space.

Remarks:

  The concept of a three-valued halting decider function with only two
  parameters is troublesome, because we would like to maintain the property that
  we are exploring the relationship between a mathematical function, and a
  procedure which computes it.  Yet, the error value appears to be a property
  of the decider, not of the function: it refers to the inability of the
  decider to compute something.  In the three-valued decider situation, the
  underlying mathematical function must in fact be regarded as in fact having
  three parameters: halt3(decider, program, input). The function either decides
  whether the <program, input> pair halts. Or else it declares error. The error
  return means this: "neither true nor false is the correct return value for
  the specified decider with regard to the <program, input> test case". Thus if
  that decider correctly computes the three-valued halting function, it must
  return error the inputs (program, input). The third argument is implicit: it
  is that decider itself.  The decider knows its own identity.

  It must be remembered that if the value of halt3(d, p, i) is error,
  the function halt(p, i) still has a true or false value: the program
  either halts or doesn't halt. halt3(d, p, i) = error asserts that
  decider d is not able to determine this, because it is somehow being "gamed"
  by that test case.

  This is also the reason we have three arguments in the error_decider: for
  that function, the three-argument space is made explicit. It does not refer
  to itself but to a specific decider that it is passed as an argument.

  Thus, in this proof sketch, the argument is essentially this:
  a decider d(p, i) cannot compute halt3(d, p, i) over all
  possible p, i combinations.

Objection:

  I hereby anticipate the following objection to the proof. Surely,
  if error_decider is found which is similar to should_return_error,
  then in fact since should_return_error is a subroutine of the
  halting_decider, then in fact the decider is the target of foul play.

  However, this is not the case. The error_decider function isn't actually
  similar to should_return_error, let alone the same. It only has to have the
  same value as should_return_error for one single combination of argument
  values: that which occurs in the test case. We have to consider this in the
  light of the argument space of these functions being infinite! Two
  functions over infinite domains which agree in just one value are hardly similar at
  all, by any sane definition of similar.

  The error_decider is independently discovered; there is no requirement that
  it be reverse-engineered out of any piece of the halting decider. It may be
  discovered by a fair search which proceeds through the possible functions
  until the inevitable event that the halting decider happens to break.

  By coincidence, error_decider could perform exactly the same computation as
  should_return_error, but this is not a requirement of the proof.
  Furthermore, more than one error_decider exists that can produce the
  necessary test case.

References:

[1] _On computable numbers, with an application to the Entscheidungsproblem_,
    Alan Turing, Proceedings of the London Mathematical Society,
    Series 2, Volume 42 (1937), pp 230–265.

[2] _Mathematical Logic_, Stephen Cole Kleene, 1966,
    Chapter V: Computability and Decidability.