Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!newcastle.ac.uk!turing!ndah
From: D.A.Harrison@newcastle.ac.uk (Dave Harrison)
Newsgroups: comp.lang.functional
Subject: Re: Can laziness sometimes be too lazy?
Message-ID: <1990Jul30.193317.12831@newcastle.ac.uk>
Date: 30 Jul 90 19:33:17 GMT
References: <3203@osc.COM>
Sender: news@newcastle.ac.uk
Followup-To: comp.lang.functional
Organization: Computing Laboratory, U of Newcastle upon Tyne, UK NE17RU
Lines: 72


In article <3203@osc.COM>, jgk@osc.COM (Joe Keane) writes:
|>
|>Now, in a lot of cases we can determine that an expression is stuck in an
|>infinite loop.  Usually this is defined to be bottom, but we can extend the
|>semantics so that when this is detected it raises an `infinte loop'
|>exception.
|>However, it should be clear that this is no longer bottom, and that no matter
|>how sophisticated our detection algorithm, some expressions will still be
|>bottom.
|>

Sort of related to this is an idea I found in paper by Manfred Broy [Broy 83].
The idea is to timestamp every element in a domain. For the domain of booleans
you get (tt = true, ff = false, ! = bottom) :


             <infinity, !>
                  |
                  . 
                  . 
                  . 

                  |
                  |
         <2,tt> <2,!> <2,ff>
              \   |   /
               \  |  /
         <1,tt> <1,!> <1,ff>
              \   |   /
               \  |  /
         <0,tt> <0,!> <0,ff>
              \   |   /
               \  |  /
		<0,!>

(Sorry about the diagram - a bit tricky in ASCII and I'm no artist at the best
of times :-) ).

The timestamps on tt and ff denote the times at which a program works out that
the result is true or false. The timestamps on ! denote that the program hasn't
worked out what the result is by that time. The relevance to this thread is 
that non-termination is not modelled by the weakest element, <0,!> but by the 
"highest" <infinity, bottom> (i.e. the program doesn't know the answer "after 
infinite time").

Because of the shape of the diagram above I call these things herring-bone 
domains. Among other things I've used them to give a semantics for a 
functional language for real-time programming [Harrison 88]. 

If anyone is remotely interested please get in touch. 

Dave

[Broy 83]
  "Applicative Real-Time Programming"
  M. Broy
  Proceedings IFIP  1983.
  North-Holland Information Processing 83.

[Harrison 88]
  "Functional Real-Time Programming : The Language Ruth and its Sementics"
  D. Harrison
  T.R. 59, Ph.D. Thesis. University of Stirling 1988

---------------------------------

Dave Harrison				JANET: D.A.Harrison@uk.ac.newcastle
Computing Laboratory			PHONE: +44 91 222 7784
University of Newcastle upon Tyne
Newcastle upon Tyne NE1 7RU
U.K.