Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!dali.cs.montana.edu!uakari.primate.wisc.edu!sdd.hp.com!wuarchive!uunet!stanford.edu!agate!dog.ee.lbl.gov!elf.ee.lbl.gov!torek
From: torek@elf.ee.lbl.gov (Chris Torek)
Newsgroups: comp.lang.misc
Subject: Re: Halting Problem Solved! Film at 11!
Message-ID: <13045@dog.ee.lbl.gov>
Date: 10 May 91 14:33:37 GMT
References: <3007@optima.cs.arizona.edu> <STEPHEN.91May10011311@estragon.uchicago.edu> <ROCKWELL.91May10084151@socrates.umd.edu>
Reply-To: torek@elf.ee.lbl.gov (Chris Torek)
Organization: Lawrence Berkeley Laboratory, Berkeley
Lines: 34
X-Local-Date: Fri, 10 May 91 07:33:37 PDT

A quick note that might serve to end all this fuss:

It seems to me that many of you are busy energetically expounding on
a different question than the one which whoever-started-this intended
to ask.  That is,

	given program P in language L, I want an analyser that will say:
		P does not halt for these inputs: <list>
		P might or might not halt for these inputs: <list>
	and I would like as few of the latter answers as possible.

For instance, given the program [yes, I use `unnecessary' semicolons]

	program p (input, output);
	    procedure spin; begin while true do {nothing}; end;
	var v : integer;
	begin
	    write('gimme a number');
	    read(v);
	    if v < 0 then spin;
	end.

we would like to have the program analyser say:

	P does not halt when the input value is less than zero.

We would not like to have it say:

	P might or might not halt for any input.

but the latter is acceptable when P is `sufficiently complicated'.
-- 
In-Real-Life: Chris Torek, Lawrence Berkeley Lab CSE/EE (+1 415 486 5427)
Berkeley, CA		Domain:	torek@ee.lbl.gov