Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!cs.utexas.edu!uunet!midway!midway!stephen From: stephen@estragon.uchicago.edu (Stephen P Spackman) Newsgroups: comp.lang.misc Subject: Re: Halting Problem Solved! Film at 11! (Was Re: definitions) Message-ID: Date: 13 May 91 07:47:07 GMT References: <30082@dime.cs.umass.edu> <1991May5.135342.13792@daffy.cs.wisc.edu> <30164@dime.cs.umass.edu> <1991May13.055104.11872@daffy.cs.wisc.edu> Sender: news@midway.uchicago.edu (NewsMistress) Organization: University of Chicago CILS Lines: 81 In-Reply-To: quale@khan.cs.wisc.edu's message of Mon, 13 May 91 05: 51:04 GMT 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 ----------------------------------------------------------------------