Skip to main content
SpringerLink
Log in
Book cover

Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems)

REX 1993: A Decade of Concurrency Reflections and Perspectives pp 530–582Cite as

Initial algebra and final coalgebra semantics for concurrency

  • Conference paper
  • First Online:

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

Abstract

The aim of this paper is to relate initial algebra semantics and final coalgebra semantics. It is shown how these two approaches to the semantics of programming languages are each others dual, and some conditions are given under which they coincide. More precisely, it is shown how to derive initial semantics from final semantics, using the initiality and finality to ensure their equality. Moreover, many facts about congruences (on algebras) and (generalized) bisimulations (on coalgebras) are shown to be dual as well.

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

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

    Google Scholar 

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

    Google Scholar 

  3. A. Arnold and A. Dicky. An algebraic characterization of transition system equivalences. Information and Computation, 82:198–229, 1989.

    Google Scholar 

  4. M.A. Arbib and E.G. Manes. Parameterized data types do not need highly constrained parameters. Information and Control, 52:139–158, 1982.

    Google Scholar 

  5. 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, volume 389 of Lecture Notes in Computer Science, pages 357–365, 1989.

    Google Scholar 

  6. 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 

  7. E. Badouel. Une construction systématique de modèles à partir de spécifications opérationnelles structurelles. Technical Report 764, INRIA, Rennes, 1987.

    Google Scholar 

  8. E. Badouel. Models of concurrency. Handout at the fifth ESSLLI, Faculdade de Letras, Universidade de Lisboa, 1993.

    Google Scholar 

  9. M. Barr. Terminal coalgebras in well-founded set theory. Theoretical Computer Science, 114(2):299–315, 1993. A revised version has appeared under the title “Terminal coalgebras for endofunctors on sets”, McGill University, Montreal, 1993.

    Google Scholar 

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

    Google Scholar 

  11. F. van Breugel. Three metric domains of processes for bisimulation. Report CS-R9335, CWI, Amsterdam, 1993. To appear in Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, LNCS, Springer-Verlag, 1993.

    Google Scholar 

  12. M. Barr and C. Wells. Toposes, Triples and Theories. Springer-Verlag, 1985.

    Google Scholar 

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

    Google Scholar 

  14. P. Darondeau and B. Gamatié. Modelling infinitary behaviours of communicating systems. Technical Report 749, INRIA, Rennes, 1987.

    Google Scholar 

  15. S. Eilenberg and G.M. Kelly. Closed categories. In S. Eilenberg et al., editor, Proc. of La Jolla Conf. on Categorical Algebra, pages 421–562. Springer-Verlag, 1966.

    Google Scholar 

  16. M. Fiore. A coinduction principle for recursive data types based on bisimulation. In Proceedings of the Eighth IEEE Symposium on Logic In Computer Science, 1993.

    Google Scholar 

  17. R.J. van Glabbeek. Full abstraction in structural operational semantics (extended abstract). In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Proceedings of the Third International Conference on Algebraic Methodology and Software Technology, pages 77–84. Springer-Verlag, 1993.

    Google Scholar 

  18. J.A. Goguen, J.W. Thatcher, and E.G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In R. Yeh, editor, Current Trends in Programming Methodology, pages 80–149. Prentice-Hall, 1978.

    Google Scholar 

  19. J.F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202–260, 1992.

    Google Scholar 

  20. M.C.B. Hennessy. A fully abstract denotational model for higher-order processes. In Proceedings 8th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 1993.

    Google Scholar 

  21. M.C.B. Hennessy and G.D. Plotkin. Full abstraction for a simple parallel programming language. In J. Bečvář, editor, Proc. 8th Int'l Symp. on Mathematical Foundations of Computer Science, volume 74 of Lecture Notes in Computer Science, pages 108–120. Springer-Verlag, 1979.

    Google Scholar 

  22. B. Jacobs. Semantics of weakening and contraction. To appear in Annals of Pure and Applied Logic, 1992.

    Google Scholar 

  23. R.E. Kent. The metric closure powerspace construction. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of the 3rd MFPS, volume 298 of Lecture Notes in Computer Science, pages 173–199. Springer-Verlag, 1987.

    Google Scholar 

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

    Google Scholar 

  25. F.E.J. Linton. Autonomous equational categories. J. of Mathematics and Mechanics, 15(4):637–642, 1966.

    Google Scholar 

  26. S. Mac Lane and I. Moerdijk. Sheaves in geometry and logic: a first introduction to topos theory. Universitext. Springer-Verlag, 1992.

    Google Scholar 

  27. E.G. Manes. Algebraic theories, volume 26 of Graduate Texts in Mathematics. Springer-Verlag, 1976.

    Google Scholar 

  28. J. Meseguer and J.A. Goguen. Initiality, induction, and computability. In M. Nivat and J.C. Reynolds, editors, Algebraic Methods in Semantics, pages 459–541. Cambridge University Press, 1985.

    Google Scholar 

  29. R. Milner. Communication and Concurrency. Prentice Hall, 1989.

    Google Scholar 

  30. 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, 1981.

    Google Scholar 

  31. A.M. Pitts. A co-induction principle for recursively defined domains. Technical Report 252, Computer Laboratory, University of Cambridge, 1992. To appear in Theoretical Computer Science.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  34. J.J.M.M. Rutten and D. Turi. On the foundations of final semantics: Nonstandard sets, metric spaces, partial orders. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX workshop on Semantics: Foundations and Applications, volume 666 of Lecture Notes in Computer Science, pages 477–530. Springer-Verlag, 1993. FTP-available at ftp.cwi.nl as pub/CWIreports/AP/CS-R9241.Z.

    Google Scholar 

  35. J.J.M.M. Rutten. Processes as terms: non-well-founded models for bisimulation. Mathematical Structures in Computer Science, 2:257–275, 1992.

    Google Scholar 

  36. J.J.M.M. Rutten. A structural co-induction theorem. Technical Report CS-R9346, CWI, 1993. To appear in Proceedings of the Ninth Conference on the Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, Springer-Verlag, 1994.

    Google Scholar 

  37. J. Sifakis. Property preserving homomorphisms of transition systems. In E. Clarke and D. Kozen, editors, Logics of programs, volume 164 of Lecture Notes in Computer Science, pages 458–473. Springer-Verlag, 1984.

    Google Scholar 

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

    Google Scholar 

  39. D. Turi and B. Jacobs. On final semantics for applicative and non-deterministic languages. Fifth Biennal Meeting on Category Theory and Computer Science, Amsterdam, September 1993.

    Google Scholar 

  40. G. Winskel and M. Nielsen. Models for concurrency. Handout at the TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, P.O. Box 94079, 1090, GB Amsterdam

    Jan Rutten & Daniele Turi

Authors
  1. Jan 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

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rutten, J., Turi, D. (1994). Initial algebra and final coalgebra semantics for concurrency. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) A Decade of Concurrency Reflections and Perspectives. REX 1993. Lecture Notes in Computer Science, vol 803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58043-3_28

Download citation

  • DOI: https://doi.org/10.1007/3-540-58043-3_28

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58043-0

  • Online ISBN: 978-3-540-48423-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation