A view on implementing processes: Categories of circuits

  • Ulrich Hensel
  • David Spooner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


We construct a category of circuits: the objects are alphabets and the morphisms are deterministic automata. The construction differs in several respects from the bicategories of circuits appearing previously in the literature: it is parameterized by a monad which allows flexibility in the emergent notion of process.

We focus on the circuits which arise from a distributive category and the exception monad. These circuits are partial in that they may, based on their state, choose to abort on some inputs. Consequently, certain circuits determine languages, and safety and liveness properties with respect to these languages are captured by circuit equations. Actually, the notions of safety and liveness arise abstractly in any copy category. Extracting the category of circuits which are both safe and live corresponds to the extensive completion of a distributive copy category.

Partial circuits coincide with elements of the terminal coalgebra of a specific datatype. The co-induction principle provides mechanisms for the construction of circuits, the normalization of circuit expressions and for the proof of safety and liveness properties.


Monoidal Category Concurrent System Liveness Property Unique Morphism Distributive Category 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Samson Abramsky, Simon J. Gay, and Rajagopal Nagarajan. Interaction categories and the foundation of typed concurrent programming. In M.Broy, editor, Deductive Program Design: Proceedings of the 1994 Marktoberdorf Summer School, NATO ASI Series F: Computer and System Sciences. Springer Verlag, 1994.Google Scholar
  2. 2.
    Micheal Barr and Charles Wells. Category Theory for Computing Science. Series in Computer Science. Prentice Hall, second edition, 1995.Google Scholar
  3. 3.
    Francis Borceux. Handbook of Categorical Algebra, volume 1. Cambridge University Press, 1994.Google Scholar
  4. 4.
    A. Carboni, S. Kasangian, and R. Street. Bicategories of spans and relations. Journal of Pure and Applied Algebra, 33:259–267, 1984.Google Scholar
  5. 5.
    J. R. B. Cockett and D. A. Spooner. SPROC categorically. In CONCUR 94: Fifth Internation Conference on Concurrency Theory, Uppsala, Sweden, Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
  6. 6.
    J.R.B. Cockett. Copy categories. submitted, for a copy contact the author:, 1995.Google Scholar
  7. 7.
    J.R.B. Cockett and D.Spencer. Strong categorical datatypes ii: A term logic for categorical programming. Theoretical Computer Science, 139:69–113, 1995.Google Scholar
  8. 8.
    J.R.B. Cockett and T. Fukushima. About charity. Technical Report 92/480/18, Department of Computer Science, University of Calgary, 1992.Google Scholar
  9. 9.
    Tatsuya Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, 1987.Google Scholar
  10. 10.
    Ulrich Hensel and Horst Reichel. Defining equations in terminal coalgebras. In Egidio Astesiano, Gianna Reggio, and Andrzej Tarlecki, editors, Recent Trends in Data Type Specification, volume 906 of Lecture Notes in Computer Science. Springer Verlag, 1995.Google Scholar
  11. 11.
    P. Katis, N. Sabadini, and R.F.C Walters. The bicategory of processes. Journal of Pure and Applied Algebra, 1995. to appear, available via www from Scholar
  12. 12.
    Robert Paré. Simply connected limits. Canadian Journal of Mathematics, XLII(4):731–746, 1990.Google Scholar
  13. 13.
    Horst Reichel. An approach to object semantics based on terminal co-algebras. Mathematical Structure in Computer Science, 5:129–152, 1995.Google Scholar
  14. 14.
    Colin Stirling. Modal and temporal logics. In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter Modal and Temporal Logics. Oxford Science Publications, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Ulrich Hensel
    • 1
  • David Spooner
    • 2
  1. 1.Institut für Theoretische InformatikTechnische Universität DresdenDresdenGermany
  2. 2.Department of Computer ScienceUniversity of CalgaryCalgaryCanada

Personalised recommendations