Re: Turing machines and tape length

[Howard Pattee <***>]

Tim,

I understand how "indefinitely extensible" can substitute for
"infinite" in Turing computation and many other constructivist
proofs. I still have a problem with the implication that formal proofs
necessarily carry a priori knowledge about the real world.  It is
not clear to me why an entirely syntactic formal limitation like the
Halting Problem (i.e., derived from an errorless rewriting of unencoded
symbol strings) is a priori a limitation on any empirically testable
encoded model that is necessarily verifiable only by approximate
measurements. Einstein said it clearly: "In so far as the
propositions of mathematics are certain they do not apply to reality; and
in so far as they apply to reality they are not
certain." I don't see why any formal proof can
be assumed to be relevant for models of nature.

A classic example is Euclidean geometry that was once assumed to apply to
nature but which turned out to be just a useful approximation for local
models. All proofs have this approximation problem. There is the formal
proof that you can't trisect an idealized angle with straightedge and
compass, but the constructive limits are categorically different from the
formal limits. Formal proofs cannot be approximate or have errors. By
contrast, measurements are always approximate and always have error
limits. Consequently, if you can measure angles with a certain accuracy,
then you can always trisect an angle with that accuracy, so the formal
proof limitation is actually no limitation at all for trisecting material
angles.

Another example is the three-body problem that has clear, provable limits
on a formal solution. However, in practice no astronomer considers this
formal limit as relevant for his models of orbits or his actual
calculations. These examples are typical and could be multiplied
indefinitely.

Rosen uses the fact that formally the rationals are rare compared to the
reals as an analogy to his belief that physical models are rare compared
to biological models. But again, this is only true as a formal condition.
Constructive, empirically verifiable models have much more severe limits
than formal proofs. Specifically, when modeling with real computers we
can represent only a very limited number of the rationals. Real numbers
are only formally definable. We don't even know whether the continuum of
real numbers conforms to any empirical reality, so such formal facts
about real numbers do not in practice limit our models or affect their
empirical verification. In other words, while the proof that enumeration
of real numbers is impossible (and this is certainly a logical
limitation) this formal limitation is not a significant limit on our
practical empirical models.

Turing equivalency is also a formal concept. All the proofs about the
limits of computation are obviously formal, and assuming the
Church-Turing thesis none of the alternative disparate formalisms can
escape these limitations on what number theoretic functions can be
effectively computed. But like all formal statements, no approximations
or errors are tolerated in such proofs.

By contrast, encoded empirically testable models are never exact, and
none of these formal proofs say anything about calculating approximations
of functions. Consequently, as in the examples above, I see no reason why
any formal limits of computation, while they are certain and always hold,
should of necessity be relevant in an empirically encoded model or
simulation that must be tested only by approximate measurements. I am
not claiming that formal limits are never relevant. I am only
pointing out that a formal limitation is often irrelevant for models of
nature in the absence of an empirical test to the contrary. 

Howard

At 10:40 AM 12/23/04 -0500, Tim wrote:

Howard,
 
If the idea of an infinite tape on a Turing machine seems problematic or irrelevant outside the formal proof itself, it suffices to consider Turing machines with arbitrarily long, finite-length, tapes. (The Turing machine is otherwise already defined as being finite, in terms of finite number of distinct internal states, finite symbol expressions per tape square, etc.) From "What is a Turing Machine?" ( http://www.earlham.edu/~peters/courses/logsys/turing.htm):

"It does not matter whether we think of the tape as finite or infinite in length. But if it is finite, we will assume there will always be enough for a given operation. (If this sounds too indefinite for this exact realm, then let us say that whenever the scanner comes within n cells of either end of the tape, a human technician adds another m cells to that end; n and m may be as small as 1 to fix the principle, but we may make them each a trillion if it will bring greater peace of mind.) Since all computable functions take only a finite number of steps to compute, by definition, no operation in which we are interested will require an infinite tape. In short, the remarkable power of the Turing machine does not require an infinite tape."

 
This is described formally in Martin Davis' book, Computability and Unsolvability (Dover ), in "The General Theory of Computability", " Chapter 1: Computable Functions".  (Omitting the formal definitions here) he states:

"At this point, we must remove a basic inconsistency between our rigorous definitions and our intuitive picture. We have visualized our machine as possessing an infinite tape; yet, formally, the _expression_ on the tape of a Turing machine at an instantaneous description a is always finite, and we have required that there always be a symbol scanned at any instaneous description. This difficulty is removed by means of a special symbol S0 or B. We change our intuitive picture to that of a machine with a tape that is always finite but that can be extended. The machine is to have the property that, whenever it is about to rush off the end of the tape, a new square, on which appears a B, is "spliced" onto that end of the tape."[p. 6, ital. orig.]

Thus, strictly speaking, formal Turing proofs do not require infinite length tapes or infinite sets.
 
Obviously, the relevance of the formal Turing machine arises because it defines the limits of "effective calculability", and the class of computable functions (those functions for which an algorithm can be used to compute their values) associated with that notion. [Davis, p.3] Computational complexity seeks to characterize certain qualities or resource-requirements (e.g., of elapsed time) of an algorithm to achieve a result (i.e., to compute some value). Computational complexity is thus primarily concerned with creating a certain taxonomy of all the algorithms which compute some value; that is, of all the algorithms within the universe of algorithms circumscribed entirely by the class of computable functions as determined by the formal Turing machine.
 
(I don't know if there is any interest in computational complexity in a taxonomy of resource requirements for non-computable functions (non-halting algorithms). If so, fine -- that is another universe of functions and algorithms.)
 
Finally, if the formal Turing machine definition still seems problematic, it has also been shown that this same class of functions, (the same limits of effective calculability, and therefore, the same circumscription on the associated universe of algorithms) can be defined equivalently by using Church's l-definability, Herbrand-Godel-Kleene general recursiveness, Post's 1-definability and Post's binormality. [Davis, p.10] Therefore, one need not even invoke the formal Turing machine proof in order to arrive at the same results on the limits of computability, by simply utlizing one of these other criteria instead.
 
Regards,
Tim
 
 
 
 
 -snip-
What I wonder about is if (or how) formal proofs about Turing-equivalent computability that require infinite sets are related to computational limits based on so-called Computational
Complexity Theory where the concern is with number of steps or length of time to a solution with finite sets that nevertheless can explode exponentially.

Howard