Substantial revision.

Carefully separated "procedure" and "function" terminology, to avoid confusion.

Removed claims that the space of functions can be searched to find an
equivalent; this is not tractable due to Rice's Theorem, and not germane to the
proof.

Formalized in more detail what the third "error" value of the halt3 function
means.

1 files changed, 99 insertions, 68 deletions

diff --git a/proof-sketch.txt b/proof-sketch.txt
index 985b3d3..7b9809a 100644
--- a/proof-sketch.txt
+++ b/proof-sketch.txt
@@ -25,17 +25,17 @@ Background:
   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
+  It is not possible to create a computational function (or procedure) which
+  calculates the halting function: a procedure which is total.
+  That is to say, a procedure 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 procedure 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
+  halting decider procedure. 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
@@ -54,11 +54,11 @@ Background:
   The proof can be sketched like this:
 
     program program(input) {
-      function halting_decider(program, input) {
+      procedure halting_decider(program, input) {
         # performs some computation and returns true or false
       }
 
-      function main(input) {
+      procedure main(input) {
         if (halting_decider(this_program, input))
           loop_forever
         else
@@ -76,7 +76,7 @@ Background:
 
   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
+  test cases can be found which break it, which shows that no procedure
   can compute the halting for all possible values.
 
   For detailed formal proofs related to the halting problem and decidability in
@@ -121,31 +121,43 @@ The Proof:
   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)) {
+    procedure halting_decider(program, input) {
+      procedure should_return_error(d, p, i) {
+        # ...
+      }
+
+      procedure decide_halting(p, i) {
+        # ...
+      }
+
+      if (should_return_error(source_code(decide_halting), 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
+  The procedures should_return_error and decide_halting are subroutines of
+  halting_decider: they are effectively part of that procedure, and their
   implementation may vary among various proposed halting_deciders.
 
+  In the above, source_code operator denotes some sort of quoting: a way to
+  obtain a representation of a given procedure as code which can be analyzed
+  (as opposed to just a reference which can be invoked).
+
   The attack on the three-valued halting_decider looks like this:
 
     program program(input) {
-      function halting_decider(program, input) {
+      procedure halting_decider(program, input) {
         # performs some computation and returns error, true or false
       }
 
-      function error_decider(decider, program, input) {
+      procedure error_decider(decider, program, input) {
         # performs some computation and returns strictly true or false
       }
 
-      function main(input) {
-        if (error_decider(halting_decider, program, input)) {
+      procedure main(input) {
+        if (error_decider(source_code(halting_decider), input, input)) {
           switch (halting_decider(program, input)) {
           case true:
             exit(0)
@@ -156,7 +168,7 @@ The Proof:
             abort()
           }
         } else {
-          switch (halting_decider(program, input)) {
+          switch (halting_decider(input, input)) {
           case true:
             loop_forever
           case false:
@@ -175,27 +187,27 @@ The Proof:
 
   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
+  There is a now a new procedure 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.
+  to provide suitable error_decider procedure. When a suitable error_decider is
+  provided, 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
+  What is a suitable error_decider? The suitable error_decider is a procedure
   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
+  In the case when error_decider(source_code(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
+  error_decider also returns true, causing the main procedure 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
@@ -207,52 +219,73 @@ The Proof:
   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
+  All that is left is question: does an error_decider exist which
+  attacks 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
+  corresponds to a procedure (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).
+  A procedure is a finite entity chosen from a countably infinite enumerable
+  set (the set of all possible procedures).
 
-  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.
+  In the set of all possible error_deciders, there are procedures which
+  match the computation of should_return_error.  The should_return_error
+  procedure itself necessarily occurs in this set! Not only that, but
+  other procedures which match the return value of should_return_error
+  on just the relevant arguments: those which occur in the test case
+  of interest.
 
 Remarks:
 
-  The concept of a three-valued halting decider function with only two
+  The concept of a three-valued halting decider procedure 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.
+  of the decider procedure, not of the function: it refers to the inability of the
+  decider to compute something.  How this is resolved is that 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.
+
+  Here is the definition of what it means when the value of halt3(d, p, i)
+  is error:
+
+    1. The boolean decider d(p, i) returns true or false, and it is incorrect.
+    2. Another decider d' is also incorrect on d'(p', i').
+    3. These two deciders are related together in that d' is just the
+       logical inverse of d; that is d'(x,y) = not d(x, y).
+    4. The program p contains a procedure equivalent to d, and the only
+       difference between p and p' is that inside p', the equivalent of d is
+       replaced with an equivalent of d'.
+    5. If i = p, then i' = p'. Otherwise i' = i.
+
+  If 4 and 5 are the only differences between the input cases, <p, i>
+  and <p', i'>, and if d(p, i) is wrong, such that d'(p',i') is also wrong
+  where d' = not d, it must be that these test cases are using a
+  self-referential trick to make d and d' wrong.
+
+  Thus if a three-valued decider d3 correctly computes the three-valued
+  halting function, it must determine that its two-valued decider d
+  is incorrect according to the above definition.
+
+  d3 only takes two parameters, because the third parameter is implicit.
+  The decider only computes the halt3 function partially, for a particular
+  value of the decider:
+
+    procedure d3(p, i)
+    {
+       procedure e(d, p, i) { calculates the error function }
+       procedure d(p, i) { boolean halting decider }
+
+       if (e(source(d), p, i))
+         return error;
+       else
+         return d(p, i)
+    }
+
+  A given procedure d3 tries calculate halt3(d, p, i) for only a fixed d,
+  where d represents d3's built-in decider d.
 
 Objection:
 
@@ -270,9 +303,7 @@ Objection:
   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.
+  it be reverse-engineered out of any piece of the halting decider.
 
   By coincidence, error_decider could perform exactly the same computation as
   should_return_error, but this is not a requirement of the proof.