On 1/19/2010 9:57 AM, John F. Sowa wrote:
> Rob,
>
> I'll admit that the word 'described' could be interpreted in
> more than one way. But the interpretation I intended makes
> the following statement uncontroversial:
>
> JFS>> In fact, every program on every digital computer can be
> > described in FOL. Most aren't, but the machine itself and
> > everything that runs on it can, in principle, be defined
> > in FOL.
>
> RF> This does seem a very strong statement.
>
> The proof follows directly from elementary comp. sci.:
>
> 1. Every digital computer and every digital device attached
> to it (such as I/O devices or graphics engines) can be
> simulated by a Turing machine (TM), which computes exactly
> the same results as the original device, but more slowly.
>
> 2. Anything computable by one of more TMs working together
> can be simulated by a single TM that can compute the same
> results as the original collection of TMs but more slowly.
>
> 3. Every TM can be defined by a finite, but extendible string
> of symbols called a *tape*, a pointer to one symbol somewhere
> on that tape, and a set of axioms in FOL that specifies how
> the current symbol is modified and how the pointer moves to
> another symbol.
>
> This is what I had intended by the term 'describes'. (01)
Even more abstractly still, a TM can simply be /identified /with its
program, a finite set of (typically) 4-tuples. One can then define,
for any TM, a precise notion of a *run* of that TM on any given input
(i.e., on any given initial "tape"), that is, a precise notion of how
the program alters the initial input step-by-step. Mathematically, the
initial input, i.e., a tape, is nothing but a sequence (in the
mathematical sense) of symbols and a run is jut a sequence of such
sequences. All of this is easily definable in first-order set theory. See,
e.g., Davis, Sigal, and Weyuker, /Computability, Complexity, and
Languages/. (02)
> RF> Is it not true that a lot of what we might regard as
> > "meaningful" about some programs, such as whether they
> > will ever halt, will escape any such description?
>
> Those descriptions go beyond the original specification,
> but many of them can also be described in FOL. (03)
They can *all* be described in FOL. (04)
> In fact, the predicate Will_Halt(M,T), which states whether or not
> machine M will halt given tape T, can be defined in FOL. (05)
Yes, it is the simple statement, translated into FOL, that, for some
natural number n, the length of the run of M on tape T is n. (06)
> For some pairs of (M,T), the predicate Will_Halt can be
> determined by a proof in FOL. But for others, the theorem
> prover will loop forever. (07)
Right, whether or not we can PROVE that a given TM will halt on a given
input is an entirely different question, one that has nothing to do with
first-order logic /per se/. (08)
Chris Menzel (09)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (010)
|