FOM: Church-Turing hypothesis -- reply to Vorobey

[Joe Shipman]

Thanks for a very interesting response.

     >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.

Yes, but we still need to know that our physical devices really implement that abstract
notion.

     >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.

But why do you believe the computer performs as advertised?  Either because it is
pragmatically seen to work, or because you believe the physics that went into its design
and construction, and both these considerations could also be relevant for nonrecursive
physical systems.

> 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?".
>

Of course you are correct here, because we have the notion of algorithm and accept
"CT1".  But all that tells us is that a person could IN PRINCIPLE solve the problem "by
hand" using an algorithm.  If you look at a calculation that needs to be done by a real
computer, for example the verification that a large integer is prime, you really only
believe the computer because1) it has always worked before, and
2) you have a THEORY of WHY it (considered as a physical system) actually does implement
the abstract notion of algorithm.

> > 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.
>

I claim that this is no different from the position you are in with respect to a real
computer calculation that is too large to be feasibly verified "by hand".

> 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?
>

But this is already the situation we have with respect to "quantum computers".  A quantum
algorithm cannot be simulated "by hand" in the same way a classical algorithm can but
because we believe the physics involved in their design we are willing to say, for
example, that "factoring integers can be done by a quantum computer in polynomial time"
(Shor, 1994).

> 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.

By the same argument, quantum computers "do not compute".

>  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.
>

Yes, but I'm contemplating a different situation where an independently conceived and
verified physical theory is used as the basis for the technology used to construct the
device.

> > 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.
>

No, you can count the number of atoms accurately if you are only doing a limited number
at a time -- this is why I suggested that exponential time would be necessary.  The other
problem is running out of atoms, but this is the same as running out of energy (since you
could create more atoms in theory) and comes back to the original question of the
infiniteness of the total energy of the Universe, which is unresolved but permitted by
the laws of physics we know so far.

> > 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.
>

That's why I used quotes around the word "proof" in that sentence -- it is clearly worse
than the situation where you understand physically what is going on.

> 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.
>
>

I disagree with this; C_T_2 states that no physical device exhibits behavior of a certain
type and can be formalized independently of the informal notion of "algorithm".  Of cause
C_T_1 is a very useful time-saver because we don't have to get formal so much if we can
informally "see" that something is effectively computable and conclude it's recursive.

Steve Simpson will correct me if I'm wrong here, but I think the identification of the
primitive recursive functions as effectively computable goes back to Hilbert and predates
the definition of general recursive functions; it would have been possible to formulate a
C_T_1 and a C_T_2 with respect to *that* notion of computation, and those could have been
*independently* refuted (one could build a device to calculate a non-p.r. function and
prove from physical considerations that it did so, while independently observing that the
same function could be calculated "by hand").

> 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.
>
>

Please do!

One final remark: it is not possible to dismiss the preceding discussion as merely
"about" physics and not mathematics.  Behind every mathematically definable but
nonrecursive function lies an infinity of UNDECIDABLE mathematical sentences (because
otherwise you could compute the function by searching for proofs and disproofs of
sentences of the form f(a)=b).  In particular, only FINITELY MANY values of such a
function need to be "physically accessible" to obtain new truths independent of ZFC
--arbitrary precision is unnecessary.  The statement "PT is correct", where PT is the
physical theory on which the device's technology is based, plays the role of a new axiom
from which proofs are derived by a "computer" which does not work in a way that
corresponds to an informal notion of algorithm -- these proofs would have the same
epistemological status as assertions about the values of a function calculated by a
quantum computer (going further, we could even say they have the same *practical*
epistemological status as assertions about the value of a function calculated by a
conventional computer which is not feasibly computable "by hand").


-- Joe Shipman