FOM: Church-Turing hypothesis -- reply to Vorobey and Davis

[Anatoly Vorobey]

You, Joe Shipman, were spotted writing this on Tue, Nov 03, 1998 at 02:37:00PM -0500:
> Vorobey writes:
> 
> > Suppose that you are facing a physical device that you suspect is the
> > oracle for the halting problem.
> 
> > How, do you think, would you be able to *prove* that it really always
> solves
> > the halting problem correctly?
> 
> The same way you prove that an ordinary computer solves a recursively
> solvable problem correctly -- in the context of a mathematized physical
> theory.  

I beg to differ. This isn't at all the way how we normally prove that a 
computer solves a problem correctly. What we actually *do*
is proving that an *algorithm* - a notion completely detached from the
physical world and current physical theories - solves the problem correctly.

Witness the steadily growing field of Program (and chipset) Verification in
CS. One usually describes the program (or chip design) to be verified in
a suitably simplified and poweful high-level programming language; then one
defines the desirable result the program should produce (or chip's behavior)
as an invariant, or a statement in a suitable kind of temporal logic, etc. 
One doesn't rely on quantum electrodynamics (which is needed to make the
computer work), classical electrodynamics, etc. in the course of this process.
Physics is never relevant, mathematized or not.

A "proof" of correctness which relies on current physical theories will not
satisfy *mathematicians*. They would perceive it as lacking the kind of
absoluteness one expects from a proof in mathematics. The first thing they
would ask would be, "What is the current physical theories are incorrect?".

> You first need a physical theory in which mathematically
> definable but nonrecursive funtions are experimentally accessible; if
> the theory passes experimental tests and is acceptable *as physics*, one
> can then derive as a consequence that a particular reproducible
> experimental setup "computes" a nonrecursive function.

But you can't actually *verify* that the device solves the halting problem.
You may have lots of physical evidence (which, by its nature, is never
conclusive) for the particular physical theory
which lets you conclude that the device "computes" a nonrecursive function,
but you cannot confirm that result *by working with the device*. You cannot
prove *mathematically* that the device computes a nonrecursive function; you
cannot confirm that experimentally; the device doesn't "talk back" to you -
it doesn't make new predictions useful for confirming or refuting the
underlying physical theory. Also, the assertion that it computes a nonrecursive
function is nonfalsifiable - and this makes its usefulness dubious, especially
in the Popperian scientific framework.

For all practical purposes, this device is indistinguishable from a very smart
computer program which purports to solve the halting problem and for which
you don't know its algorithm. Imagine that I let you work with a black box,
with one input string and one output string, which purports to solve the 
halting problem. You know that the black box entails an algorithm in the usual
sense of a Turing machine, but you don't know what the algorithm is. You cannot
then prove experimentally, by working with the black box, that it doesn't
solve the halting problem (to be able in general to do that, you would have to
be able to recursively enumerate nonhalting machines to find the one it 
misidentifies as halting - i.e. to be able yourself to solve the halting 
problem). 

And now, imagine the same black box as in the preceding paragraph, only this
time you *don't know* that it's an algorithm in the classical sense. Does the
situation look familiar?

> Since according to our current best theories certain experimentally
> measurable quantities are equal to countably infinite sums of terms each
> of which is a recursive real (with no proof that the sum exists or that
> it is a recursive real if it does exist) this is not inconceivable.  

It is not inconceivable that there are physical phenomena which "compute"
nonrecursive functions. However, in order for us, rational human beings, to
regard this physical behavior as computation (and not as "computation") and
to trust its results we need to be able to view it as a realization of some
abstract, intuitively appealing notion of algorithm/computation, just as we
view physical computers as realizing our various abstract notions of 
algorithms. As yet another thought experiment, imagine a modern computer
solving certain hard recursive problems presented as a gift to Cauchy, in
the form of a black box he can't examine or understand its workings. Cauchy
can of course formulate physical theories that "explain" why the black box
gives correct mathematical statements consistently, but he probably wouldn't
regard such theories as a *proof* that the device always functions correctly.

> This isn't a very good kind of nonrecursiveness because it depends an
> measuring a number to arbitrary precision, though that is certainly
> possible for some kinds of experimental quantities (for example the
> ratio of the radioactive half-lives of two different kinds of atoms
> where you can just count the decays in a very large sample -- you'd need
> exponential time to get n bits of precision here).  

The initial number of atoms you need also, however, grows exponentially, and
therefore your remarks seems to rest on an assumption that you can measure
to arbitrary relative precision the number of atoms, which is not at all
self-evident. 


> The other way to "prove" that the physical device is an oracle for the
> halting problem is just to observe that it always gives an answer, that
> it never answers "no halt" for a machine that does halt, and that it
> never answers "halt" for a machine that provably does not halt.  

But this can never be accepted as a satisfactory proof. Even *in principle*
you cannot turn this into a satisfactory proof, because you'd need to be able
to recursively enumerate nonhalting machines - see above.

> By the way, earlier Davis drew a distinction between Church's_Thesis_1
> (formalizing the informal notion of algorithm) and
> C_T_2 (formalizing what is "computable" by real physical systems).  The

> ** The "Church-Turing Hypothesis" is Davis's C_T_2 (an assertion that
> the laws of physics rule out a certain type of potentially
> experimentally observable behavior, which is falsifiable).

The problem, as I tried to describe it, is that you really need C_T_1
in order to meaningfully talk about perceiving, verifying, refuting,
and otherwise working with C_T_2.

Odifreddi has a surprisingly fruitful philosophic discussion of Church's
Thesis in his otherwise strictly mathematical _Classical Recursion Theory_.
He distinguishes about ten various formulations of the thesis, some of them
further refining C_T_1 and C_T_2 above, and draws from various physical
and cognitive science sources in order to talk about plausibility of
each of them. I'll be glad to summarize his main points on FOM, if there is
interest in this.

-- 
Anatoly Vorobey,
mellon at pobox.com http://pobox.com/~mellon/
"Angels can fly because they take themselves lightly" - G.K.Chesterton