🚀 go-pugleaf

In article <1991May13.055104.11872@daffy.cs.wisc.edu> quale@khan.cs.wisc.edu (Douglas E. Quale) writes:

|Real computers are *NOT* FSMs, and I hope most computer engineers are
|not surprised by this.  The rather small workstation on which I'm writing
|this is currently running about 34 asynchronous processes.  The next state
|of the machine depends very greatly on which key I strike next, the exact
|time at which I strike it, the exact current location of the 5 hard disks
|read and write heads, the value of all the peripheral devices hardware and
|hardware registers (many of which cannot be read by the CPU), and whether
|or not someone decides to log on to play Nethack.  (In fact, the state of
|the machine will be rather different if decides to play a priest rather
|than a knight, etc. ad. nauseum.)

I don't think you've demonstrated your point at all. Surely they are
i/o devices, but this idea that input is somehow not subject to type
constraints and could be "anything" is really weird. A serial line can
bring in only 256 (say) distinct codes; each one can arrive at any one
of a few billion cycles each second (it may not be synchronous when
it's sent but it damn well better be synchronised by input port!).
That's a lot of state, but it's still about as finite as you can get.

The trick you are perhaps missing is that at some point you end up
distinguishing the machine from its environment. Since the bandwidth
of the communication channel is finite and the active lifetime of the
channel is finite, and the channel is digital, this in no way
compromises the FSM-hood of the machine (even if there is feedback
in the channel, of course, since this can only constrain the input
space further).

The entire situation is formally equivalent to an FSM that starts off
with one "random" number which is formally an oracle for all the input
it will recieve while running - any further information you can give
about the form of the input stream only serves to constrain things.

|This particular machine is fairly old and unreliable hardware.  Disk and
|other failures are rather common, and unpredictable.  Memory read and write
|errors are always possible, and they are not always corrected or even
|detected.

If the hardware is flakey (or rather WHEN it is) we clearly can't talk
about language semantics or programme behaviour at all. This is a red
herring of the highest order. (Yes, you can talk about fault-tolerant
behaviour, but i order to be theoretically meaningful you have to list
a finite set of failure modes of bounded consequences, which is ABSURD
from a practical point of view (whoever heard of STABLE storage? What
about nuclear war?) and actually doesn't damage the model ANYWAY, it
just means that there's one more i/o device, formally).

|I completely disagree with you as to whether analog considerations are a
|useful way to think about computation.  It's essential to realize that our
|machines are not infallible, digital computation devices.  It's funny to
|see someone complain that TMs are an inappropriate abstraction for
|computation because they don't model real machines but that FSMs are -- and
|completely disregard the reality in real.

Look, we all know about synchroniser failures, but from a formal
semantics point of view, they ARE failures. And from a hardware point
of view too - even if there's nothing that can be done about them. The
machine glitched and the programme that's running is no longer the
programme I wrote. I don't think you CAN formalise software behaviour
in THAT level of reality - certainly you can't without talking about a
programme compiled and running on a specific hardware configuration -
and even if you could the machine would STILL be finite and an FSM
would STILL be a "better" formal model than a turing machine, at least
until the first hardware failure manifested.

|When I asked a favorite math prof of mine what he disliked so about the
|computer proof of the 4 color theorem he started by saying that the proof
|was unsatisfying because he would naturally prefer a proof that he could
|verify in his head, without relying on a machine.  His next statement
|struck me more deeply; he stated that computer proofs are really proofs
|consisting of an experiment in physics.  At first I thought this somewhat
|silly, but I now understand that he was right.  Execution of a program on a
|real machine is really nothing more than an experiment in physics.

I take it that he doesn't use a physical device - say, his brain -
when he verifies a proof of his own devising? :-)
----------------------------------------------------------------------
stephen p spackman         Center for Information and Language Studies
systems analyst                                  University of Chicago
----------------------------------------------------------------------