🚀 go-pugleaf

In article  <3940@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes:
>
>>]		_Bottom_ is NOT synonymous with nontermination!!!!
>>]		We are dealing with a DECLARATIVE paradigm,
>>]		and nontermination is an _operational_ concept.
>
>David Gudeman:		gudeman@cs.arizona.edu <23552@megaron.cs.arizona.edu>
>>	Well, I'd have to say that bottom _is_ synonymous
>>	with nontermination...

Which was answered fairly effectively, so let me take another tack.
The distinguishing feature of bottom is that you don't know what it is
when you have it.  But if your program terminates, then you know what
you have, so what you have isn't bottom.  It _doesn't_ work to say
that the result is still bottom because it was undefined in the
language definition, because then you can prove that bottom = x for
whatever x the program produced, and from that you can prove that x =
y for any x and y.  This seems to me to prove pretty conclusively that
bottom implies nontermination.

The other side is a little more complex, since it is certainly the
case that there are non-terminating programs that produce useful
results.  But when are the results produced?  You can't say that the
results are produced when the computation terminates because it won't.
But you can say that the result of the program is an infinite sequence
of some sort, and that you can look at any desired prefix of the
sequence.  Then you have a non-terminating program that produces a
value distinguishable from bottom.  So it is not true that
non-termination implies bottom.

Well, I was half right.
-- 
					David Gudeman
Department of Computer Science
The University of Arizona        gudeman@cs.arizona.edu
Tucson, AZ 85721                 noao!arizona!gudeman