# «A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Electrical Engineering and Computer ...»

**The following is immediate from Theorem 3.5.3 and 4.3.4:**

Corollary 4.3.5. There is a sequential asynchronous process coalgebra of type I, O that is ﬁnal in SAPC I,O.

4.4 Axiomatization Corollary 4.3.5 is the basis for our axiomatization. Essentially, what are axioms state are that processes are members of a sequential asynchronous process coalgebra of type I, O that is ﬁnal in SAPC I,O. This approach to the deﬁnition of a process is inspired by [2] and [57].

We will not be too obsessed with formalistic issues, as we want these axioms expressed in the same manner they are to be used.

In the following, we will used accented and subscripted variants of p for processes. We will write P, for the class of all process and the cooperation of the corresponding coalgebra.

Essentially, this is a metalinguistic device to refer to the model of the theory from inside the theory. This will enable us to express an extremal axiom that guarantees that are coalgebra is ﬁnal in SAPC I,O. And the consistency of that axiom will be a consequence of Corollary 4.3.5.

## CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 105

Axiom of Unimpeded Input. For every p and any i, m ∈ actin I, O, there is p such i,m that p −→ p.The Extremal Axiom can further be reduced in the obvious way within the language of the theory using Theorem 3.5.3.

4.5 The Postulate of Delegated Output The Postulate of Delegated Output stands out, as it is the only one we have titled a “postulate” instead of an “axiom”. This is done with the purpose of initiating a discussion about its use and connection to the notion of asynchrony. Intuitively, even though it is practically assumed in every formalization of asynchrony that we know of, we would like to exclude it. Because we would like to consider computational processes running

## CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 106

asynchronously on a non-distributed system, and exchanging messages over say queues or buﬀer as asynchronous. But this creates problems.In [14], Brock and Ackerman came up with their famous anomaly that proved that relational semantics was never going to be suﬃcient for the denotational characterization of interactive systems. The following example is from [54], and demonstrates two programs that have the same history relation, yet diﬀerent behaviour when in a feedback

**conﬁguration:**

In [29], Jonsson proved that in order to obtain a compositional semantics, one must at least add enough information to describe the behaviour of a process as observed by a linear, sequential observer. And as it turns out, his result rests on the Postulate of Delegated Output.

The next example shows two diﬀerent components that display the same behaviour with respect to such an observer, but still behave diﬀerently in a feedback conﬁguration. The pseudocode below is understood as the program of a sequential process that reads from a buﬀer i and writes to a buﬀer o. Notice that reads are internal actions, while writes are external. And this is what violates the Postulate of Delegated Output: each of these two processes, when in feedback, after writing something to its own buﬀer, that written value is there to be read the next time a read is attempted. The reader is invited to verify that the traces of the two processes agree as they are, but disagree when in feedback.

## CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 107

It is not hard to see that the problem is created only in direct feedback, and so perhaps it is instead that mechanism that is ill conceived. But more work is required to understand this new kind of anomaly.

Bibliography [1] Karl Abrahamson. Decidability and Expressiveness of Logics of Programs. PhD thesis, University of Washington at Seattle, 1980.

[2] Peter Aczel. Non-well-founded Sets. Number 14 in Lecture Notes. CLSI, 1988.

[3] Peter Aczel. Final universes of processes. In Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, pages 1–28, London, UK, 1994. Springer-Verlag.

[4] Peter Aczel. A semantic universe for the study of fairness. VERY ROUGH AND INCOMPLETE DRAFT, October 1996.

[5] Peter Aczel and Nax Paul Mendler. A ﬁnal coalgebra theorem. In Category Theory and Computer Science, pages 357–365, London, UK, 1989. Springer-Verlag.

[6] Jiˇ´ Ad´mek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories.

rı a New York, NY, USA, 2004.

[7] Jiˇ´ Ad´mek, Stefan Milius, and Jiˇ´ Velebil. On coalgebra based on classes.

rı a rı Theoretical Computer Science, 316(1-3):3–23, 2004. Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott.

[8] Bowen Alpern and Fred B. Schneider. Deﬁning liveness. Information Processing Letters, 21(4):181–185, 1985.

[9] Jos C. M. Baeten. The total order assumption. In Proceedings of the First North American Process Algebra Workshop, NAPAW ’92, pages 231–240, London, UK, 1993.

Springer-Verlag.

[10] Jos C. M. Baeten. A brief history of process algebra. Theoretical Computer Science, 335(2-3):131–146, 2005.

[12] Martin Berger. An interview with Robin Milner.

http://www.informatics.sussex.ac.uk/users/mfb21/interviews/milner/, September 2003.

[13] Garrett Birkhoﬀ. On the structure of abstract algebras. Mathematical Proceedings of the Cambridge Philosophical Society, 31(04):433–454, 1935.

[14] J. Dean Brock and William B. Ackerman. Scenarios: A model of non-determinate computation. In J. D´ and I. Ramos, editors, Formalization of Programming ıaz Concepts, volume 107 of Lecture Notes in Computer Science, pages 252–259. Springer Berlin / Heidelberg, 1981.

[15] Daniela Cancila, Furio Honsell, and Marina Lenisa. Some properties and some problems on set functors. Electronic Notes in Theoretical Computer Science, 164(1):67–84, 2006. Proceedings of the Eighth Workshop on Coalgebraic Methods in Computer Science (CMCS 2006), Eighth Workshop on Coalgebraic Methods in Computer Science.

[16] Constantin Courcoubetis, Moshe Y. Vardi, and Pierre Wolper. Reasoning about fair concurrent programs. In Proceedings of the eighteenth annual ACM symposium on Theory of computing, STOC ’86, pages 283–294, New York, NY, USA, 1986. ACM.

[17] Philippe Darondeau. About fair asynchrony. Theoretical Computer Science, 37:305–336, 1985.

[18] Philippe Darondeau and Laurent Kott. On the observational semantics of fair parallelism. In Josep Diaz, editor, Automata, Languages and Programming, volume 154 of Lecture Notes in Computer Science, pages 147–159. Springer Berlin / Heidelberg, 1983.

[19] Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

[20] E. Allen Emerson. Alternative semantics for temporal logics. Theoretical Computer Science, 26(1-2):121–130, 1983.

[21] E. Allen Emerson and Joseph Y. Halpern. “Sometimes” and “not never” revisited: On branching versus linear time temporal logic. J. ACM, 33:151–178, January 1986.

[24] Matthew Hennessy. Axiomatising ﬁnite delay operators. Acta Informatica, 21:61–88, 1984.

[25] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32:137–161, January 1985.

[26] Matthew Hennessy and Colin Stirling. The power of the future perfect in program logics. Information and Control, 67(1-3):23–52, 1985.

[27] Thomas T. Hildebrandt. A fully abstract presheaf semantics of SCCS with ﬁnite delay. Electronic Notes in Theoretical Computer Science, 29:102–126, 1999. CTCS ’99, Conference on Category Theory and Computer Science.

[28] Bart Jacobs and Jan J. M. M. Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin, 62:62–222, 1997.

[29] Bengt Jonsson. A fully abstract trace model for dataﬂow networks. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’89, pages 155–165, New York, NY, USA, 1989. ACM.

[30] Richard M. Karp and Raymond E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147–195, 1969.

[31] Yasuo Kawahara and Masao Mori. A small ﬁnal coalgebra theorem. Theoretical Computer Science, 233(1-2):129–145, 2000.

[32] Robert M. Keller. Formal veriﬁcation of parallel programs. Commun. ACM, 19(7):371–384, 1976.

[33] Joachim Lambek. A ﬁxpoint theorem for complete categories. Mathematische Zeitschrift, 103:151–161, 1968.

[34] Leslie Lamport. “Sometime” is sometimes “not never”: On the temporal logic of programs. In Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’80, pages 174–185, New York, NY, USA,

1980. ACM.

[35] Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer, 2nd edition, 1998.

[37] Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980.

[38] Robin Milner. A ﬁnite delay operator in synchronous CCS. Technical Report CSR-116-82, University of Edinburgh, 1982.

[39] Robin Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25(3):267–310, 1983.

[40] Robin Milner. A calculus of communicating systems. Report ECS-LFCS-86-7, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, August 1986. (First published by Springer-Verlag as Vol.92 of Lecture Notes in Computer Science).

[41] Robin Milner. Communication and Concurrency. Prentice-Hall, Upper Saddle River, NJ, USA, 1989.

[42] Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87(1):209–220, 1991.

[43] Edward F. Moore. Gedanken-experiments on sequential machines. Automata Studies, 34:129–153, 1956.

[44] Lawrence S. Moss and Norman Danner. On the foundations of corecursion. Logic Journal of IGPL, 5(2):231–257, 1997.

[45] David Park. On the semantics of fair parallelism. In Dines Bjoorner, editor, Abstract Software Speciﬁcations, volume 86 of Lecture Notes in Computer Science, pages 504–526. Springer Berlin / Heidelberg, 1980.

[46] David Park. Concurrency and automata on inﬁnite sequences. In Peter Deussen, editor, Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer Berlin / Heidelberg, 1981.

[47] Benjamin C. Pierce. Basic Category Theory for Computer Scientists. Foundations of Computing. The MIT Press, 1991.

[48] Gordon D. Plotkin. A structural approach to operational semantics (Aarhus notes).

Technical Report DAIMI FN–19, Computer Science Department, Aarhus University, September 1981.

[50] Amir Pnueli. The temporal semantics of concurrent programs. In Gilles Kahn, editor, Semantics of Concurrent Computation, volume 70 of Lecture Notes in Computer Science, pages 1–20. Springer Berlin / Heidelberg, 1979.

[51] John Power and Hiroshi Watanabe. An axiomatics for categories of coalgebras.

Electronic Notes in Theoretical Computer Science, 11:158–175, 1998. CMCS ’98, First Workshop on Coalgebraic Methods in Computer Science.

[52] Vaughan R. Pratt. Process logic: Preliminary report. In Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, POPL ’79, pages 93–100, New York, NY, USA, 1979. ACM.

[53] M. Reynolds. An axiomatization of full computation tree logic. The Journal of Symbolic Logic, 66(3):1011–1057, 2001.

[54] James R. Russell. Full abstraction for nondeterministic dataﬂow networks. In Foundations of Computer Science, 1989., 30th Annual Symposium on, pages 170–175, 1989.

[55] Jan J. M. M. Rutten. A calculus of transition systems (towards universal coalgebra).

Technical report, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, The Netherlands, 1995.

[56] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000.

[57] Jan J. M. M. Rutten and Daniele Turi. On the foundations of ﬁnal semantics:

Non-standard sets, metric spaces, partial orders. In Proceedings of the REX Workshop on Sematics: Foundations and Applications, pages 477–530, London, UK, 1993.

Springer-Verlag.

[58] Davide Sangiorgi. On the origins of bisimulation and coinduction. ACM Trans.

Program. Lang. Syst., 31(4):1–41, 2009.

[60] Michael B. Smyth and Gordon D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):761–783, 1982.

[62] Terese. Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

[63] Hermann Weyl. Mathematics and logic. The American Mathematical Monthly,