Adding proof sketch.

1 files changed, 287 insertions, 0 deletions

diff --git a/proof-sketch.txt b/proof-sketch.txt
new file mode 100644
index 0000000..4a79e07
--- /dev/null
+++ b/proof-sketch.txt
@@ -0,0 +1,287 @@
+                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.