A view on implementing processes: Categories of circuits
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.
KeywordsMonoidal Category Concurrent System Liveness Property Unique Morphism Distributive Category
Unable to display preview. Download preview PDF.
- 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.Micheal Barr and Charles Wells. Category Theory for Computing Science. Series in Computer Science. Prentice Hall, second edition, 1995.Google Scholar
- 3.Francis Borceux. Handbook of Categorical Algebra, volume 1. Cambridge University Press, 1994.Google Scholar
- 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.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.J.R.B. Cockett. Copy categories. submitted, for a copy contact the author: email@example.com, 1995.Google Scholar
- 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.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.Tatsuya Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, 1987.Google Scholar
- 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.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 http://theory.doc.ic.ac.uk:80/tfm/papers/WaltersRFC/bicatproc/.Google Scholar
- 12.Robert Paré. Simply connected limits. Canadian Journal of Mathematics, XLII(4):731–746, 1990.Google Scholar
- 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.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