WWW.DISSERTATION.XLIBX.INFO FREE ELECTRONIC LIBRARY - Dissertations, online materials

<< HOME
CONTACTS

Pages:     | 1 |   ...   | 10 | 11 ||

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

-- [ Page 12 ] --

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,

Pages:     | 1 |   ...   | 10 | 11 ||

Similar works:

«Forthcoming in Philosophy and Phenomenological Research Tense, Timely Action and Self-Ascription Stephan Torre Abstract I consider whether the self-ascription theory can succeed in providing a tenseless (B-theoretic) account of tensed belief and timely action. I evaluate an argument given by William Lane Craig for the conclusion that the self-ascription account of tensed belief entails a tensed theory (A-theory) of time. I claim that how one formulates the selfascription account of tensed...»

«È caso da intermedio! Comic Theory, Comic Style and the Early Intermezzo by Keith James Johnston A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Faculty of Music University of Toronto © Copyright by Keith James Johnston, 2011 È caso da intermedio! Comic Theory, Comic Style and the Early Intermezzo Keith James Johnston Doctor of Philosophy Faculty of Music University of Toronto ABSTRACT This dissertation is a study of the comic intermezzo’s...»

«TOWARDS ANGLE-CONTROLLED VAN DER WAALS HETEROSTRUCTURES A Dissertation Presented to the Faculty of the Graduate School of Cornell University In Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy by Lola Brown August 2015 This work is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License. To view a copy of this license, visit http://creativecommons.org/licenses/by-nc-sa/4.0/. 2015, Lola Brown TOWARDS ANGLE-CONTROLLED VAN...»

«The Process of Salvation I. Foundational Premises The conclusions one draws are heavily influenced by the basic and foundational assumptions or premises one brings to the question at issue. The premises which underlie this study are as follows: 1) That there is an objective right and wrong. We live in a philosophical climate dominated by the theory of evolution which holds that life is a product of blind chance. There is no plan behind man’s existence and, hence, ultimately no purpose to it....»

«Extending ACID Semantics to the File System via ptrace A Dissertation Presented by Charles Philip Wright to The Graduate School in Partial fulﬁllment of the Requirements for the Degree of Doctor of Philosophy in Computer Science Stony Brook University Technical Report FSL-06-04 May 2006 Copyright by Charles Philip Wright 2006 Abstract of the Dissertation Extending ACID Semantics to the File System via ptrace by Charles Philip Wright Doctor of Philosophy in Computer Science Stony Brook...»

«Early Detection and Treatment of Breast Cancer by Random Peptide Array in neuN Transgenic Mouse Model by Hu Duan A Dissertation Presented in Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy Approved June 2015 by the: Graduate Supervisory Committee: Stephen Albert Johnston, Chair Leland Hartwell Valentin Dinu Yung Chang ARIZONA STATE UNIVERSITY August 2015 ABSTRACT Breast cancer is the most common cancer and currently the second leading cause of death among women in...»

«02 Schriften des Zentrums für Interdisziplinäre Regionalstudien Felix Girke (ed.) Ethiopian Images of Self and Other Band 2 Schriften des Zentrums für Interdisziplinäre Regionalstudien Herausgegeben vom Direktorium des Zentrums für Interdisziplinäre Regionalstudien Felix Girke (ed.) Ethiopian Images of Self and Other Felix Girke studied social anthropology, cultural geography, and philosophy at the Johannes Gutenberg University in Mainz. Since 2003, he has pursued intensive ethnographic...»

«On the Influence of Age of Acquisition and Proficiency on Second Language Processing DISSERTATION zur Erlangung des akademischen Grades doctor philosophiae (Dr. phil.) im Fach Allgemeine Sprachwissenschaft von Juliane Domke geb. Schütte Präsident der Humboldt-Universität zu Berlin Prof. Dr. Jan-Hendrik Olbertz Dekanin der Philosophischen Fakultät II Prof. Dr. Helga Schwalm Gutachterinnen/Gutachter: 1. Prof. Dr. Sophie Repp 2. Prof. Dr. Rainer Dietrich eingereicht am 01. April 2015...»

«Lying and Asserting Andreas Stokke — penultimate version, published in Journal of Philosophy, CX(1), 2013, 33–60 — Abstract The paper argues that the correct deﬁnition of lying is that to lie is to assert something one believes to be false, where assertion is understood in terms of the notion of the common ground of a conversation. It is shown that this deﬁnition makes the right predictions for a number of cases involving irony, joking, and false implicature. In addition, the proposed...»

«HOW METHODISTS WERE MADE: THE ARMINIAN MAGAZINE AND SPIRITUAL TRANSFORMATION IN THE TRANSATLANTIC WORLD, 1778-1803 by LIAM IWIG-O’BYRNE Presented to the Faculty of the Graduate School of The University of Texas at Arlington in Partial Fulfillment of the Requirements for the Degree of DOCTOR OF PHILOSOPHY THE UNIVERSITY OF TEXAS AT ARLINGTON May 2008 Copyright © by Liam Iwig-O’Byrne 2008 All Rights Reserved ACKNOWLEDGEMENTS I would like to thank my committee for their work on my behalf,...»

«Animosity or Alliance? Identifying the Factors that Promote Black and Latino Electoral Coalitions by Andrea Benjamin A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Political Science) in The University of Michigan Doctoral Committee: Professor Vincent L. Hutchings, Chair Professor Nancy Burns Professor Andrei Markovits Assistant Professor Cara Wong, University of Illinois, Urbana Champaign TO MY PARENTS: HERMAN M. AND JOAN M. BENJAMIN...»

<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.