Skip to main content
SpringerLink
Log in

On the foundations of final semantics: Non-standard sets, metric spaces, partial orders

  • Conference paper
  • First Online:
Semantics: Foundations and Applications (REX 1992)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 666))

Abstract

Canonical solutions of domain equations are shown to be final coalgebras, not only in a category of non-standard sets (as already known), but also in categories of metric spaces and partial orders. Coalgebras are simple categorical structures generalizing the notion of post-fixed point. They are also used here for giving a new comprehensive presentation of the (still) non-standard theory of nonwell-founded sets (as non-standard sets are usually called). This paper is meant to provide a basis to a more general project aiming at a full exploitation of the finality of the domains in the semantics of programming languages — concurrent ones among them. Such a final semantics enjoys uniformity and generality. For instance, semantic observational equivalences like bisimulation can be derived as instances of a single ‘coalgebraic’ definition (introduced elsewhere), which is parametric of the functor appearing in the domain equation. Some properties of this general form of equivalence are also studied in this paper.

The research of Daniele Turi was supported by the Stichting Informatica Onderzoek in Nederland within the context of the project “Non-well-founded sets and semantics of programming languages”. (Project no. 612-316-034.)

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky. A Cook's tour of the finitary non-well-founded sets. Department of Computing, Imperial College, London, 1988.

    Google Scholar 

  2. S. Abramsky. The lazy lambda calculus. In D.A. Turner, editor, Research Topics in Functional Programming, pages 65–116. Addison-Wesley, 1990.

    Google Scholar 

  3. S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.

    Google Scholar 

  4. P. Aczel. Non-well-founded sets. Number 14 in Lecture Notes. CSLI, 1988.

    Google Scholar 

  5. J. Adámek and V. Koubek. Least fixed point of a functor. Jour. of Computer and System Sciences, 19:163–178, 1979.

    Google Scholar 

  6. P. Aczel and N. Mendler. A final coalgebra theorem. In D.H. Pitt, D.E. Ryeheard, P. Dybjer, A.M. Pitts, and A. Poigné, editors, Proceedings category theory and computer science, Lecture Notes in Computer Science, pages 357–365, 1989.

    Google Scholar 

  7. P. America and J.J.M.M. Rutten. Solving reflexive domain equations in a category of complete metric spaces. Journal of Computer and System Sciences, 39(3):343–375, 1989.

    Google Scholar 

  8. J. Barwise. Admisible Sets and Structures. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1975.

    Google Scholar 

  9. M. Barr. Terminal coalgebras in well-founded set theory. Department of Mathematics and Statistics, McGill University, 1991.

    Google Scholar 

  10. J. Barwise and J. Etchemendy. The Liar: An Essay in Truth and Circularity. Oxford University Press, 1988.

    Google Scholar 

  11. S. Brookes and S. Geva. Computational comonads and intensional semantics. Technical Report CMU-CS-91-190, Computer Science Department, CarnagieMellon University, 1991.

    Google Scholar 

  12. J.W. de Bakker and J.-J.Ch. Meyer. Metric semantics for concurrency. BIT, 28:504–529, 1988.

    Google Scholar 

  13. F. van Breugel. Generalised finiteness conditions on labelled transition systems for operational semantics of programming languages. CWI, 1992.

    Google Scholar 

  14. J.W. de Bakker and J.I. Zucker. Processes and the denotational semantics of concurrency. Information and Control, 54:70–120, 1982.

    Google Scholar 

  15. J. Dugundji. Topology. Allyn and Bacon, inc., 1966.

    Google Scholar 

  16. M. Forti and F. Honsell. Set theory with free construction principles. Annali Scuola Normale Superiore, Pisa, X(3):493–522, 1983.

    Google Scholar 

  17. M. Forti and F. Honsell. A general construction of hyperuniverses. Technical Report 1992/9, Istituto di Matematiche Applicate U. Dini, Facoltà di Ingegneria, Università di Pisa, 1992.

    Google Scholar 

  18. T. Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, September 1987.

    Google Scholar 

  19. W.H. Hesselink. Deadlock and fairness in morphisms of transition systems. Theoretical Computer Science, 59:235–257, 1988.

    Google Scholar 

  20. S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, Berlin, 1971.

    Google Scholar 

  21. S. Mac Lane. Mathematics: Form and Function. Springer-Verlag, Berlin, 1986.

    Google Scholar 

  22. A. Levy. Basic Set Theory. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1979.

    Google Scholar 

  23. D. Lehmann and M.B. Smyth. Algebraic specifications of data types: a synthetic approach. Mathematical Systems Theory, 14:97–139, 1981.

    Google Scholar 

  24. R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1980.

    Google Scholar 

  25. E. Moggi. Computational lambda-calculus and monads. In Proc. Fourth IEEE Symp. on Logic In Computer Science, pages 14–23. IEEE Computer Society Press, 1989.

    Google Scholar 

  26. R. Milner and M. Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87:209–220, 1991.

    Google Scholar 

  27. F.J. Oles. A category-theoretic approach to the semantics of programming languages. PhD thesis, School of Computer and Information Science, Syracuse University, August 1982.

    Google Scholar 

  28. D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings 5th GI Conference, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer-Verlag, Berlin, 1981.

    Google Scholar 

  29. A.M. Pitts. A co-induction principle for recursively defined domains. Technical Report 252, Computer Laboratory, University of Cambridge, 1992.

    Google Scholar 

  30. G.D. Plotkin. Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”). Department of Computer Science, Univ. of Edinburgh, 1981.

    Google Scholar 

  31. G.D. Plotkin. A structured approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

    Google Scholar 

  32. J.J.M.M. Rutten. Deriving denotational models for bisimulation from Structured Operational Semantics. In M. Broy and C.B. Jones, editors, Programming concepts and methods, proceedings of the IFIP Working Group 2.2/2.3 Working Conference, pages 155–177. North-Holland, 1990.

    Google Scholar 

  33. J.J.M.M. Rutten. Processes as terms: non-well-founded models for bisimulation. Technical Report CS-R9211, CWI (Centre for Mathematics and Computer Science), Amsterdam, 1992. To appear in Mathematical Structures in Computer Science.

    Google Scholar 

  34. M.B. Smyth. I-categories and duality. In M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors, Applications of categories in computer science, volume 177 of London Mathematical Society Lecture Note Series, pages 270–287. Cambridge University Press, 1992.

    Google Scholar 

  35. M.B. Smyth and G.D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM J. Comput., 11:761–783, 1982.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Kruislaan 413, NL - 1098 SJ, Amsterdam

    Jan J. M. M. Rutten & Daniele Turi

Authors
  1. Jan J. M. M. Rutten
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Daniele Turi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rutten, J.J.M.M., Turi, D. (1993). On the foundations of final semantics: Non-standard sets, metric spaces, partial orders. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Semantics: Foundations and Applications. REX 1992. Lecture Notes in Computer Science, vol 666. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56596-5_45

Download citation

  • DOI: https://doi.org/10.1007/3-540-56596-5_45

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56596-3

  • Online ISBN: 978-3-540-47595-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation