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

<< HOME
CONTACTS

Pages:     | 1 || 3 | 4 |   ...   | 12 |

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

-- [ Page 2 ] --

CHAPTER 2. TRANSITION SYSTEMS 8 One such endofunctor is the functor Pow, which assigns to every class C the class Pow C = {S | S is a subset of C}, 9 and to every class function f : C1 → C2 a class function Pow f : Pow C1 → Pow C2 such that for every S ∈ Pow C1, (Pow f )(S) = {f (s) | s ∈ S}.

Notice that if the class C is actually a set, then Pow C = P C.

Assume an endofunctor F on Class.

Deﬁnition 2.2.2. An F -coalgebra is an ordered pair C, γ such that the following are

true:

(a) C is a class;

(b) γ is a class function from C to F (C).

Assume an F -coalgebra C, γ.

We call C the carrier of C, γ, and γ the cooperation of C, γ.

We say that C, γ is small if and only if C is a set.

We say that C, γ is large if and only if C is a proper class.

By this deﬁnition, a Pow-coalgebra is just an ordered pair C, τ of a class C and a class function τ : C → Pow C, which is precisely what we have recognized as another way to formalize the concept of transition system, with the caveat that C be a set.

Assume a Pow-coalgebra C, τ.

We call C, τ a transition coalgebra.

We write c −→τ c if and only if c ∈ τ (c).

Assume a transition system S, T.

The following is immediate:

We use the verbal expression “S is a subset of C” instead of the mathematical expression “S ⊆ C” to emphasize the constraint that S be a set.

CHAPTER 2. TRANSITION SYSTEMS 9

Proposition 2.2.3. The following are true:

(a) s −→T s if and only if s −→fun T s ;

(b) if C, τ is small, then c −→τ c if and only if c −→rel τ c.

This is all very nice, but why bother with this alternative formalization in the ﬁrst place?

To begin with, we need to understand what the informal meaning of the concept of F -coalgebra is. For this, it will help to consider the dual concept of F -algebra ﬁrst, where it is not hard to establish a connection with the more common concept of Σ-algebra, the principal object of study in the theory of universal algebra.

Deﬁnition 2.2.4. An F -algebra is an ordered pair C, α such that the following are true:

(a) C is a class;

(b) α is a class function from F (C) to C.

Assume an F -algebra C, α.

We call C the carrier of C, α, and α the operation of C, α.

We say that C, α is small if and only if C is a set.

We say that C, α is large if and only if C is a proper class.

Notice that the only diﬀerence between the deﬁnition of an F -algebra and that of an F -coalgebra is in the direction of the class function, which is reversed. Hence the duality.

Now, the way to think of the concept of F -algebra is as a generalization of the concept of Σ-algebra.

For example, consider a single-sorted signature Σ. We may think of Σ as a set of operation symbols, each annotated with a unique natural number, the arity of that symbol. A Σ-algebra is a semantic interpretation of Σ: a set S, the carrier set of the algebra, together with one n-ary operation fσ on S for each operation symbol σ of arity n in Σ. These operations may be combined together into a single function

–  –  –

then a Σ-algebra is just a small F -algebra.

Algebra is about composition of things. In a Σ-algebra, this composition takes a very speciﬁc form: things are composed according to certain rules, the operations of the Σ-algebra, and each rule determines a unique thing for every ordered n-tuple of things, where n is arbitrary but ﬁxed for that rule. There is no fundamental reason, though, why composition must be restricted to this form. One might, for example, think of a rule that determines a new composite thing for every possible set of things. And if C is the class of all things, then a rule of this kind can be represented simply as a class function from Pow C to C, which is precisely what a Pow-algebra is. In general, an F -algebra C, α will represent one or several rules for composing particular combinations of things, as speciﬁed and encoded by F, into other things, as determined by α.

We may now appeal to the duality between the concepts of F -algebra and F -coalgebra to attach a plausible informal sense to the latter: if F -algebras are generalized rules of composition, then F -coalgebras are generalized rules of decomposition.

Under this interpretation, a transition coalgebra will represent a rule for decomposing each thing in the carrier of the coalgebra to a set of other things in it. This, of course, imposes a particular view on a transition system: each state of the system is a composite thing, decomposed by the cooperation of the corresponding coalgebra to the set of all immediate successors of it in the system. And this may not be the most intuitive view to impose on a transition system. But never mind. The merit of the coalgebraic approach is not in the interpretation per se, but in the machinery available for relating the corresponding decomposition structure of one system to that of another.

Assume F -coalgebras C1, γ1 and C2, γ2.

Deﬁnition 2.2.5. A homomorphism from C1, γ1 to C2, γ2 is a class function h : C1 → C2 such that

–  –  –

We say that h is a monomorphism from C1, γ1 to C2, γ2 if and only if h is an injective homomorphism from C1, γ1 to C2, γ2.

We say that h is an epimorphism from C1, γ1 to C2, γ2 if and only if h is a surjective homomorphism from C1, γ1 to C2, γ2.

We say that C1, γ1 is a homomorphic image of C2, γ2 if and only if there is an epimorphism from C2, γ2 to C1, γ1.

We say that h is an isomorphism between C1, γ1 and C2, γ2 if and only if h is a bijective homomorphism from C1, γ1 to C2, γ2.

Proposition 2.2.6. If h is an isomorphism between C1, γ1 and C2, γ2, then h−1 is an isomorphism between C2, γ2 and C1, γ1.

Proof. See [56, prop. 2.3].

We say that C1, γ1 and C2, γ2 are isomorphic if and only if there is an isomorphism between C1, γ1 to C2, γ2.

We write C1, γ1 ∼ C2, γ2 if and only if C1, γ1 and C2, γ2 are isomorphic.

= Assume an F -coalgebra C, γ.

We say that h is an endomorphism on C, γ if and only if h is a homomorphism from C, γ to C, γ.

We say that h is an automorphism on C, γ if and only if h is an isomorphism between C, γ to C, γ.

The concept of homomorphism from one F -coalgebra to another is the coalgebraic counterpart of the concept of homomorphism from one F -algebra to another, which is a generalization, in the same sense as before, of the concept of homomorphism from one Σ-algebra to another. It is a structure-preserving map carrying the decomposition patterns CHAPTER 2. TRANSITION SYSTEMS 12 of one coalgebra to those of another. In particular, it establishes a similarity of structure between its domain and range.

In the case of Pow, this similarity can take a very familiar form.

Example 2.2.

7. Assume transition coalgebras C1, τ1 and C2, τ2.

Suppose that h is a homomorphism from C1, τ1 to C2, τ2.

Assume c1 ∈ C1.

By extensionality, this is equivalent to the following being true:

(i) if c1 −→τ1 c1, then h(c1 ) −→τ2 h(c1 );

(ii) if h(c1 ) −→τ2 c2, then there is c1 such that c1 −→τ1 c1 and c2 = h(c1 ).

(i) and (ii) look very much like the deﬁning clauses of the concept of bisimulation between transition systems. And indeed, if C1, τ1 and C2, τ2 are small, then, by Proposition 2.2.3(b), we may simply replace each instance of τ1 with rel τ1 and each instance of τ2 with rel τ2 in (i) and (ii), to conclude, by generalization, that graph h is a bisimulation between the transition systems C1, rel τ1 and C2, rel τ2.

From the perception of this connection between the concepts of homomorphism and bisimulation, it is a small step to a coalgebraic generalization of the latter.

–  –  –

Thus, B is a bisimulation between C1, γ1 and C2, γ2 just as long as it is a binary class relation between C1 and C2, and there is a class function β : graph B → F (graph B) such

that the following diagram commutes:

–  –  –

We say that B is a bisimulation on C, γ if and only if B is a bisimulation between C, γ and C, γ.

We say that B is a bisimulation equivalence on C, γ if and only if B is a bisimulation on C, γ, and an equivalence class relation on C.

So, a binary class relation between two F -coalgebras is a bisimulation just as long as we can impart it with the structure of an F -coalgebra in a way that turns the projections from the graph of the class relation to the carriers of the two F -coalgebras into homomorphisms.

In general, however, there might be more than one way to do this.

Example 2.2.

9. Let S = {0, 1}, and τ be a function from S to Pow S deﬁned by the

following mapping:

0 → S;

1 → S.

–  –  –

Another is deﬁned by the following mapping:

→{ };

0, 0 0, 1, 1, 0 →{ };

0, 1 0, 0, 1, 1 →{ };

1, 0 0, 0, 1, 1 →{ }.

1, 1 0, 1, 1, 0 In fact, there is nothing special about the graph of the class relation and its projections either.

Theorem 2.2.

10. B is a bisimulation between C1, γ1 and C2, γ2 if and only if there is an F -coalgebra C, γ, a homomorphism h1 from C, γ to C1, γ1, and a homomorphism h2 from C, γ to C2, γ2, such that

–  –  –

Proof. See [56, lem. 5.3] and [23, thm. 5.11].

Assume F -coalgebras C1, γ and C2, γ.

The following is immediate:

Corollary 2.2.11. If B is a bisimulation between C1, γ1 and C2, γ2, h1 a homomorphism from C1, γ1 to C1, γ1, and h2 a homomorphism from C2, γ2 to C2, γ2, is a bisimulation between C1, γ1 and C2, γ2.

The following will come of use:

Theorem 2.2.

12. For every class-indexed family {Bi }i∈I of bisimulations between C1, γ1 and C2, γ2, there is a bisimulation B between C1, γ1 and C2, γ2 such that

–  –  –

This coalgebraic deﬁnition of bisimulation was ﬁrst introduced in [5], and does indeed generalize the concept of bisimulation between labelled transition systems. To see this, we must ﬁrst go over the coalgebraic representation of such systems.

The functor that we are going to use is the endofunctor Pow ◦ (L × Id) on Class, namely the composite of Pow with the left product endofunctor L × Id on Class, which assigns to every class C the class

–  –  –

By Proposition 2.2.1, an L-labelled transition system S, T can be represented as a (Pow ◦ (L × Id))-coalgebra, namely as S, fun T, and conversely, a (Pow ◦ (L × Id))-coalgebra C, τ can be represented as an L-labelled transition system, namely as C, rel τ, again with the caveat that C be a set.

Assume a (Pow ◦ (L × Id))-coalgebra C, τ.

We call C, τ an L-labelled transition coalgebra.

l We write c −→τ c if and only if l, c ∈ τ (c).

Assume an L-labelled transition system S, T.

The following is immediate:

Proposition 2.2.13. The following are true:

–  –  –

Proof. Suppose that B is a bisimulation between C1, τ1 and C2, τ2.

Let graph B, β be an L-labelled transition coalgebra such that dpr B is a homomorphism from graph B, β to C1, τ1, and cpr B one from graph B, β to C2, τ2.

Assume c1 and c2 such that c1 B c2.

Thus, by generalization, B is a bisimulation between C1, τ1 and C2, τ2.

Assume L-labelled transition systems S1, T1 and S2, T2.

The following is immediate from Proposition 2.2.13(a), 2.2.14, and the deﬁnition of

bisimulation between labelled transition systems:

Proposition 2.2.15. B is a bisimulation between S1, T1 and S2, T2 if and only if B is a bisimulation between the L-labelled transition coalgebras S1, fun T1 and S2, fun T2.

Proposition 2.2.14 and 2.2.15 can of course be adapted for transition coalgebras and transition systems: simply replace every instance of Pow ◦ (L × Id) with Pow, and erase every instance of l.

–  –  –

The ﬁrst thing to note is that every bisimulation equivalence is the equivalence kernel of a homomorphism. In a theory of sets, this is straightforward. But in a theory of classes, some care is needed.

Assume a class C and an equivalence class relation E on C.

We say that q is a quotient of C with respect to E if and only if q is a surjective class function such that dom q = C and ker q = E.

In [5], existence of quotients is deduced from an assumed global form of the Axiom of Choice, and in [3], from a postulated quotient existence principle for classes. In a theory of sets, there is no such need: for every set S and every equivalence relation R on S, one can simply turn to the quotient set of S by R, namely the set

–  –  –

But in a theory of classes, these constructs are not, in general, well deﬁned. For example, if R is the full binary class relation on a proper class C, then for every c ∈ C,

–  –  –

which cannot be a member of any class.

Here, we will assume existence of quotients as a theorem of the underlying theory of classes, and not worry about its precise deduction. We only remark that in the standard von Neumann-Bernays-G¨del theory of classes, existence of quotients is readily deduced o from the Axiom of Limitation of Size.

Assume an F -coalgebra C, γ.

Proposition 2.3.1. For every bisimulation equivalence B on C, γ, and every quotient q of C with respect to B, there is exactly one F -coalgebra cod q, δ such that q is an epimorphism from C, γ to cod q, δ.

Proof. See [5, lem. 5.1 and prop. 6.1].

–  –  –

Pages:     | 1 || 3 | 4 |   ...   | 12 |

Similar works:

«A DEFINITION AND DEFENSE OF HARD PATERNALISM: A CONCEPTUAL AND NORMATIVE ANALYSIS OF THE RESTRICTION OF SUBSTANTIALLY AUTONOMOUS SELF-REGARDING CONDUCT VOLUME ONE OF TWO A Dissertation submitted to the Faculty of the Graduate School of Arts & Sciences of Georgetown University in partial fulfillment of the requirements for the degree of Doctor of Philosophy in Philosophy By Thaddeus Mason Pope, J.D. Washington, D.C. June 10, 2002 Copyright 2003 by Thaddeus Mason Pope All Rights Reserved ii A...»

«HIGH PERFORMANCE COMPUTING FOR IRREGULAR ALGORITHMS AND APPLICATIONS WITH AN EMPHASIS ON BIG DATA ANALYTICS A Thesis Presented to The Academic Faculty by Oded Green In Partial Fulﬁllment of the Requirements for the Degree Doctor of Philosophy in the School of Computational Science and Engineering Georgia Institute of Technology May 2014 Copyright c 2014 by Oded Green HIGH PERFORMANCE COMPUTING FOR IRREGULAR ALGORITHMS AND APPLICATIONS WITH AN EMPHASIS ON BIG DATA ANALYTICS Approved by:...»

«Keeping Betty Ugly: Manufacturing Diversity for Network TV by Michelle Martinez A Dissertation Presented in Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy Approved April 2015 by the Graduate Supervisory Committee: Bambi Haggins, Chair Julia Himberg Marivel Danielson ARIZONA STATE UNIVERSITY May 2015 ABSTRACT This dissertation examines the ways ABC/Disney's Ugly Betty (ABC 2006-2010) manufactures diversity to create an illusion of the U.S. as a site of multiple...»

«PROBLEMS AND CHALLENGES Faced by Liberian Refugee Children and Youths as they enter the formal Educational Systems at the Buduburam Refugee Camp in Ghana TIEN KEAH BORTU A thesis submitted in fulfillment of the requirement for the degree of Master of Philosophy in Comparative and International Education INSTITUTE FOR EDUCATIONAL RESEARCH, FACULTY OF EDUCATION UNIVERSITETET I OSLO SPRING 2009 ABSTRACT This study addresses the challenges that Liberian refugee children and youths living at the...»

«Saint Ambrose Catholic School Family Handbook 2013-2014 Monsignor Vincent R. Bommarito Pastor Sr. Barbara Zipoli, ascj Principal Revised August 2013 Mission Statement Saint Ambrose Catholic School is a parish elementary school. Our mission is to nurture the spiritual, academic, and personal needs of the students and their families. We provide a quality education by fostering creativity, divergent thinking, and the skills needed to meet the challenges of a changing world. We prepare children to...»

«Promoting Interactions in Preschoolers with Autism Spectrum Disorder via Peer-Mediated Intervention. by Esther Ruch Katz A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Department of Speech-Language Pathology University of Toronto © Esther Ruch Katz 2014 Promoting Interactions in Preschoolers with Autism Spectrum Disorder via Peer-Mediated Intervention. Esther Ruch Katz Doctor of Philosophy Department of Speech-Language Pathology University of...»

«Morphologies of Becoming: Posthuman Dandies in Fin-de-Siècle France. by Marina E. Starik B.A., University of Utah, 2003 M.A. University of Utah, 2005 Submitted to the Graduate Faculty of The Kenneth P. Dietrich School of Arts and Sciences in partial fulfillment of the requirements for the degree of Doctor of Philosophy University of Pittsburgh UNIVERSITY OF PITTSBURGH Dietrich School of Arts and Sciences This dissertation was presented by Marina E. Starik It was defended on November 12, 2012...»

«An Iterative Approach to Examining the Eﬀectiveness of Data Sanitization By ANHAD PREET SINGH B.Tech. (Punjabi University) 2007 M.S. (University of California, Davis) 2012 DISSERTATION Submitted in partial satisfaction of the requirements for the degree of DOCTOR OF PHILOSOPHY in COMPUTER SCIENCE in the OFFICE OF GRADUATE STUDIES of the UNIVERSITY OF CALIFORNIA DAVIS Approved: Matthew Bishop (Co-Chair) Sean Peisert (Co-Chair) Raquel Loran Hill Committee in Charge [2015] i c Anhad Preet Singh,...»

«THE UNIVERSITY OF CHICAGO URBANISM AND SOCIETY IN THE THIRD MILLENNIUM UPPER KHABUR BASIN VOLUME ONE A DISSERTATION SUBMITTED TO THE FACULTY OF THE DIVISION OF THE HUMANITIES IN CANDIDACY FOR THE DEGREE OF DOCTOR OF PHILOSOPHY DEPARTMENT OF NEAR EASTERN LANGUAGES AND CIVILIZATIONS BY JASON ALIK UR CHICAGO, ILLINOIS DECEMBER 2004 Copyright 2004 by Jason Alik Ur All rights reserved For Heather TABLE OF CONTENTS VOLUME ONE LIST OF FIGURES LIST OF TABLES ACKNOWLEDGEMENTS CHAPTER ONE: SOCIAL...»

«Cambridge University Press 978-0-521-87347-5 The Cambridge Companion to Epicureanism Edited by James Warren Excerpt More information james warren Introduction Philosophy, as long as a drop of blood shall pulse in its world-subduing and absolutely free heart, will never grow tired of answering its adversaries with the cry of Epicurus: ‘The truly impious man is not he who denies the gods worshipped by the multitude, but he who afﬁrms of the gods what the multitude believes about them’. Karl...»

«The Theological Reception of the Book of Isaiah in the Nineteenth-Century Church of England By Robert Lewis Knetsch A Thesis Submitted to the Faculty of Wycliffe College and the Theology Department of the Toronto School of Theology In partial fulfilment of the requirements for the degree of Doctor of Philosophy in Theology awarded by the University of St. Michael’s College © Copyright by Robert L. Knetsch 2013 THE THEOLOGICAL RECEPTION OF THE BOOK OF ISAIAH IN THE NINETEENTH-CENTURY CHURCH...»

«Article The Scepticism of Descartes’s Meditations James Thomas Laval théologique et philosophique, vol. 67, n° 2, 2011, p. 271-279.Pour citer cet article, utiliser l'information suivante : URI: http://id.erudit.org/iderudit/1007008ar DOI: 10.7202/1007008ar Note : les règles d'écriture des références bibliographiques peuvent varier selon les différents domaines du savoir. Ce document est protégé par la loi sur le droit d'auteur. L'utilisation des services d'Érudit (y compris la...»

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