Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!rphroy!caen!sdd.hp.com!elroy.jpl.nasa.gov!ncar!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: Re: The Halting Problem is _not_ solvable on real com
Message-ID: <3008@optima.cs.arizona.edu>
Date: 9 May 91 19:32:38 GMT
Sender: news@cs.arizona.edu
Lines: 28

In article  <1991May9.122526.13533@s1.msi.umn.edu> David Epstein writes:
]
]>Proof: Suppose that Halt exists.  Then define 
]>    Paradox = (Halt::E(Paradox)) -> CLoop ; CAccept
]>what is the result of running Paradox?
]
]Is this a misprint, David? You can't define Paradox in terms of
]itself.

It was sort of a misprint, I guess I should have asked about the
behavior of Halt::E(Paradox).  But the definition of Paradox is OK.
E(Paradox) is a representation of Paradox in the input language so I'm
defining Paradox in terms of a representation of itself.  This is
certainly possible on a real computer, since you can have the program
Paradox open the file that contains its own source code and read it.

Incidentally, I'm not happy with the conditions I stated for the
theorem since some of them should be assumptions about all classes of
automata.  The existence of an encoding E seems to apply for any
alphabet with two or more characters as long as C is a countable set.
It seems that the existence of 'CAccept' and 'M1->M2;M3' are immediate
consequences of the definition of an automaton (I obviously didn't
give a full definition), and I'm also inclined to believe that 'M::S'
is a consequence of the definition an automaton.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman