[TYPES] CPO semantics of recursive types

[Achim Jung]

Malcolm, for cpos and continuous functions we have solutions to all 
recursive domain equations, for example, D =  [D -> D].

If [D -> D] is interpreted as the (pointwise ordered) cpo of monotone 
functions then D = [D -> D] has only the one-point cpo as a solution. This 
was first shown in the paper

@Article{davies71,
   author = 	{R. O. Davies and A. Hayes and G. Rousseau},
   title = 	{Complete Lattices and the Generalized {Cantor}
 		  Theorem},
   journal = 	{Proceedings of the AMS},
   year = 	1971,
   volume = 	27,
   pages = 	{253--258}
}

Best regards,

Achim.

-------------------------------------------------------------------------
  Prof Achim Jung			Tel.: (+44) 121 41 44776
  School of Computer Science		Sec.: (+44) 121 41 43711
  The University of Birmingham		Fax.: (+44) 121 41 44281
  Edgbaston				Email: A.Jung at cs.bham.ac.uk
  BIRMINGHAM, B15 2TT			Web: http://www.cs.bham.ac.uk
  England
-------------------------------------------------------------------------



On Thu, 26 Oct 2006, Malcolm Tyrrell wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
> Hello,
>
> I have a question concerning the denotational semantics of
> recursive types using complete partial orders.
>
> For a programming language, the domain for a function type T->U is
> defined as the space of all continuous functions from the domain of T
> to the domain of U. I understand that recursively defined domains
> have solutions in this semantics.
>
> I am working with a specification language, and the domains I'm using
> for function types T->U is the space of all *monotonic* functions from
> the domain of T to the domain of U. Can anyone tell me (or even better,
> point me to a reference) whether this has any ramifications for the
> existence of recursively defined domains?
>
> Thanks for any help,
>
> Malcolm.
>