Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!sample.eng.ohio-state.edu!purdue!haven.umd.edu!umd5!newton.cs.jhu.edu!callahan From: callahan@cs.jhu.edu (Paul Callahan) Newsgroups: comp.theory Subject: Re: Question on halting problem Message-ID: Date: 10 May 91 14:55:37 GMT Lines: 22 In article <4765@osc.COM> jgk@osc.COM (Joe Keane) writes: >In article <4760@osc.COM> jgk@osc.UUCP i write: >>Given a program which takes no input, either it halts or it doesn't. > >In article <1991May3.185947.19929@milton.u.washington.edu> >petry@milton.u.washington.edu (David Petry) writes: >>Am I the only one that questions the validity of the above assertion? > >I have to admit i have a certain intuitive uneasiness about assertions like >this. Logically, it's simply the law of the excluded middle. However, it may >be that neither alternative is provable. Wrong. The assertion "program X halts" is provable if and only if it is true. For a proof, we simply exhibit a correct trace of the execution up to step n, the point at which it halts. The assertion "program X does not halt" may not have a proof, but it is simply incorrect to suggest that "neither alternative is provable." This is what it means to say that the set of halting programs is recursively enumerable (though not recursive). -- Paul Callahan callahan@cs.jhu.edu