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



Pages:     | 1 | 2 || 4 | 5 |   ...   | 12 |

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

-- [ Page 3 ] --

The converse is not true: the equivalence kernel of a homomorphism is not, in general, a bisimulation (see Example 2.3.3). But the graph of a homomorphism, or more accurately, considering our working definition of a binary class relation, the homomorphism itself, is.

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

Theorem 2.3.

2. h is a homomorphism from C1, γ1 to C2, γ2 if and only if h is a class function from C1 to C2, and a bisimulation between C1, γ1 and C2, γ2.

Proof. See [56, thm. 2.5].

In other words, homomorphisms are functional bisimulations. This should not be surprising: homomorphisms are supposed to preserve structure, and bisimulations to capture equivalence of it. But do they really?

There is not much to be said about homomorphisms; they are too basic to doubt.

Bisimulations, on the other hand, deserve investigation.

We begin with a formal statement of coalgebraic bisimilarity.

We say that c1 and c2 are bisimilar among C1, γ1 and C2, γ2 if and only if there is a bisimulation B between C1, γ1 and C2, γ2 such that c1 B c2.

We say that c1 and c2 are bisimilar in C, γ if and only if c1 and c2 are bisimilar among C, γ and C, γ.

A disturbing fact about coalgebraic bisimilarity is that, unlike ordinary bisimilarity, it is not, in general, an equivalence concept.

Example 2.3.

3. Let F be an endofunctor on Class that assigns to every class C the class

–  –  –

Let S2 = {0}, and γ2 be the unique function from S2 to F (S2 ), namely a function from S2

to F (S2 ) defined by the following mapping:

0 → 0, 0, 0.

Let h be the unique function from S1 to S2, namely a function from S1 to S2 defined by the

following mapping:

0 → 0;

1 → 0.

h is trivially a homomorphism from S1, γ1 to S2, γ2. But whereas h(0) and h(1) are equal, and thus, trivially bisimilar in S2, γ2, 0 and 1 are not bisimilar in S1, γ1, lest there be a binary relation B on S1, and an F -coalgebra graph B, β such that 0, 1 ∈ graph B and β( 0, 1 ) = 0, 0, 0, 1, 1, 1.

Note 2.3.

1. We cannot replace ordered triples with multisets of size 3 having at most two members of multiplicity greater than 0 to the same effect in Example 2.3.3.

Example 2.3.

1.1. Let F be an endofunctor on Class that assigns to every class C the class

–  –  –

For every class C, F (C) is simply the class of all multisets of size 3 having just at most two members of multiplicity greater than 0 (see [62, chap. A]).

Let S = {0, 1}, and γ be a function from S to F (S) defined by the following mapping:

0 → [0, 0, 1];

1 → [0, 1, 1].

We want to show that the full binary relation on S is a bisimulation on S, γ. In order to do so, we must find a function β : S × S → F (S × S) such that both proj1 (S × S) and proj2 (S × S) are homomorphisms from the F -coalgebra S × S, β to S, γ.

One such function is defined by the following mapping:

→[ 0, 0 0, 0, 0, 0, 0, 0 ];

→[ 0, 1 0, 1, 0, 1, 1, 0 ];

→[ 1, 0 0, 1, 1, 0, 1, 0 ];

→[ 1, 1 1, 1, 1, 1, 1, 1 ].

Thus, 0 and 1 are bisimilar in S, γ.

This should cast serious doubt on the coalgebraic notion of bisimulation: how can one hope to capture all of equivalence of structure using a notion, the induced similarity concept of which is not, in general, transitive?

This discrepancy was not lost on Aczel and Mendler, who, also in [5], generalized the coalgebraic concept of bisimulation further into that of what they called a precongruence, or in the case of an equivalence class relation, a congruence. This is a technically more complicated concept: to determine whether a binary class relation R on the carrier of an F -coalgebra C, γ is a precongruence on C, γ, one has to invoke a quotient of C with respect to the equivalence class relation generated by R, compose its image under F with γ, and test whether R is contained in the equivalence kernel of the composite. It is also an intuitively more warranted concept, exactly formalizing the idea of a class relation that is compatible with the cooperation of a coalgebra. Every bisimulation on an F -coalgebra is a precongruence, but not every precongruence on an F -coalgebra is a bisimulation. In fact, the endofunctor that we used in Example 2.3.3 is one that was devised in [5] for the express purpose of demonstrating this separation between the two concepts.

CHAPTER 2. TRANSITION SYSTEMS 22 Note 2.3.

2. We can also use Example 2.3.3 to separate the two concepts. For by [31, prop. 4.2], the equivalence kernel of a homomorphism from an F -coalgebra C1, γ1 to an F -coalgebra C2, γ2 is a precongruence on C1, γ1.

Note 2.3.

3. In [5], the concept of precongruence was defined only for binary class relations on single F -coalgebras. However, one can use directed sums (see Definition 2.4.10), to extend this definition to binary class relations between pairs of different F -coalgebras.





Definition 2.3.3.1. A precongruence on C, γ is a binary class relation P on C such that for every quotient q with respect to the equivalence class relation generated by P,

graph P ⊆ graph ker(F (q) ◦ γ).

We say that P is a congruence on C, γ if and only if P is a precongruence on C, γ, and an equivalence class relation on C.

The following is easy:

Proposition 2.3.3.2. P is a precongruence on C, γ if and only if P is a class relation on C, and the equivalence class relation generated by P is a congruence on C, γ.

We say that c1 and c2 are congruent in C, γ if and only if there is a congruence P on C, γ such that c1 P c2.

Definition 2.3.4. A precongruence between C1, γ1 and C2, γ2 is a binary class relation P : C1 ↔ C2 such that

–  –  –

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

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

Let E be the equivalence class relation generated by (inj1 (C1 + C2 ))−1 ; B ; inj2 (C1 + C2 ).

–  –  –

Theorem 2.3.

3.4. h is a homomorphism from C1, γ1 to C2, γ2 if and only if h is a class function from C1 to C2, and a precongruence between C1, γ1 and C2, γ2.

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

Then by Theorem 2.3.2, h is a bisimulation between C1, γ1 and C2, γ2, and thus, by Proposition 2.3.3.3, a precongruence between C1, γ1 and C2, γ2.

Conversely, suppose that h is a precongruence between C1, γ1 and C2, γ2.

Let E be the equivalence class relation generated by (inj1 (C1 + C2 ))−1 ; h ; inj2 (C1 + C2 ).

Let q be a quotient of C1 + C2 with respect to E.

Then the following diagram commutes:

–  –  –

E is the smallest equivalence class relation that contains (inj1 (C1 + C2 ))−1 ; h ; inj2 (C1 + C2 ), or equivalently, the smallest transitive relation that contains the reflexive-symmetric closure of it.

We use induction to prove that for any c1 and c2 such that c1 E c2, the following are true:

CHAPTER 2. TRANSITION SYSTEMS 25

–  –  –

If c1 = c2, then (i) and (ii) are vacuously true. Also, since inj1 (C1 + C2 ) is injective, (iii) is trivially true, and since inj2 (C1 + C2 ) is injective, (iv) is trivially true.

(inj2 (C1 + C2 ))(c2 ) = c2, and h(c ) = c2. Thus, (ii) and (iii) are vacuously true. Also, by the induction hypothesis, if there is c1 such that

–  –  –

(inj1 (C1 + C2 ))(c2 ) = c2, and c = h(c2 ). Thus, (i) and (iv) are vacuously true. Also, by the induction hypothesis, if there is c1 such that (inj2 (C1 + C2 ))(c1 ) = c1, then c1 = c, and hence, h(c2 ) = c1. Thus, (ii) is true. Finally, by the induction hypothesis, if there is c1 such that (inj1 (C1 + C2 ))(c1 ) = c1, then h(c1 ) = c, and hence, h(c1 ) = h(c2 ). Thus, (iii) is true.

Therefore, q ◦ inj2 (C1 + C2 ) is injective, and thus, has a left inverse.

Another implication, which we are not using for this proof, is that { c1, c2 | q((inj1 (C1 + C2 ))(c1 )) = q((inj2 (C1 + C2 ))(c2 ))} = graph h, is a pullback of q ◦ inj1 (C1 + C2 ) and q ◦ inj2 (C1 + C2 ) in and thus, graph h, dpr h, cpr h F -Coalg.

Let g be a left inverse of q ◦ inj2 (C1 + C2 ).

Since h is a class function, dpr h is bijective, and h = (cpr h) ◦ (dpr h)−1.

–  –  –

Thus, by generalization, h is a homomorphism from C1, γ1 to C2, γ2.

An immediate corollary of Theorem 2.3.2 and 2.3.3.4 is that in the case of single-valued binary class relations, the concepts of bisimulation and precongruence coincide.

Here, mostly for the purpose of accessibility, we have decided to follow the approach of Rutten in [56], who advocates the coalgebraic concepts of bisimulation and bisimulation equivalence as formal duals to the algebraic ones of substitutive relation and congruence.

His tacit preference over the more appropriate concepts of precongruence and congruence of [5] is partly justified by the the fact that more can be proved about bisimulations and bisimulation equivalences than precongruences and congruences. No matter: most of the theory in [56] is developed under the assumption that the endofunctor F preserves weak pullbacks, a technical condition under which the concepts of bisimulation and precongruence coincide. And although we will never need to make explicit mention of it, every particular endofunctor considered here will actually satisfy this condition, unless specifically intended not to.

2.4 Behaviour modelling and final coalgebras Suppose that we wanted to use L-labelled transition systems to model the behaviour of processes of some kind. What we would wish for then is that there be a system diverse enough to model the behaviour of every process, but coarse enough not to distinguish between processes of equivalent behaviour. Is there such a system?

The way to use an L-labelled transition system to model the behaviour of a process is to map the process to a state of the system, and let the branching structure emanating from that state represent the behaviour of the process. Equivalence of behaviour then amounts to similarity of branching structure of some kind, and indeed determines the actual association between ‘behaviour’ and branching structure. If we let bisimilarity be that concept of similarity, and assume for simplicity that any state of every L-labelled transition system models the behaviour of some process, then our question becomes an enquiry over the existence of an L-labelled transition system S, T such that for every L-labelled transition system S, T and any s ∈ S, there is s ∈ S such that s and s are bisimilar among S, T and S, T, and for any s1, s2 ∈ S, s1 and s2 are bisimilar in S, T if and only if s1 = s2.

We want to use Theorem 2.3.2 to turn this enquiry into an instance of a common universal construction problem, namely that of a terminal object of a category.

CHAPTER 2. TRANSITION SYSTEMS 29 An object of a category is a terminal object of that category just as long as for every object of that category, there is exactly one arrow of that category from the latter to the former.

The category pertaining to our enquiry is that of all L-labelled transition coalgebras and all homomorphisms between them. But once again, we work generally.

First, notice that for every F -coalgebra C, γ, id C is an endomorphism on C, γ, and for every homomorphism h1 from an F -coalgebra C1, γ1 to an F -coalgebra C2, γ2, and every homomorphism h2 from C2, γ2 to an F -coalgebra C2, γ2, h2 ◦ h1 is a homomorphism from C1, γ1 to C2, γ2. Thus, F -coalgebras and their homomorphisms form a category.

We write F -Coalg for the category whose objects are all the F -coalgebras, and arrows all the homomorphisms from one F -coalgebra to another.

Note that for any homomorphism h from an F -coalgebra C1, γ1 to an F -coalgebra C2, γ2, the domain and codomain of h as an arrow of F -Coalg are C1, γ1 and C2, γ2 respectively, and not to be confused with the domain and codomain of h as an arrow of Class, which are C1 and C2 respectively.

We say that C, γ is final in F -Coalg if and only if for every F -coalgebra C, γ, there is exactly one homomorphism from C, γ to C, γ.

We use “final” here rather than “terminal” only to conform with common practice in the germane literature: an F -coalgebra is final in F -Coalg if and only if it is a terminal object of F -Coalg.

Notice that if C1, γ1 and C2, γ2 are both final in F -Coalg, then C1, γ1 ∼ C2, γ2, = lest there be another endomorphism, apart from the identity map, on either of them. In plain words, all final F -coalgebras are isomorphic to one another.

Theorem 2.3.

2 suggests that there might be a connection between our enquiry and the notion of finality. We set out to make this connection, if any, precise.

We say that C, γ is weakly complete in F -Coalg if and only if for every F -coalgebra C, γ and any c ∈ C, there is c ∈ C such that c and c are bisimilar among C, γ and C, γ.

Note that our use of the term “weakly complete” is different from, and in general, strictly more inclusive than that in [2], [5], and [3].

–  –  –

Proposition 2.4.1.1. If for every small F -coalgebra C, γ, there is a homomorphism from C, γ to C, γ, then C, γ is weakly complete in F -Coalg.

Proof. Suppose that for every small F -coalgebra C, γ, there is a homomorphism from C, γ to C, γ.

Assume an F -coalgebra C, γ.

Assume c ∈ C.

By Lemma 2.4.



Pages:     | 1 | 2 || 4 | 5 |   ...   | 12 |


Similar works:

«FLOWFIELD CHARACTERIZATION AND MODEL DEVELOPMENT IN DETONATION TUBES A DISSERTATION SUBMITTED TO THE DEPARTMENT OF AERONAUTICS & ASTRONAUTICS AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERISTY IN PARTIAL FULLFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Zachary Clark Owens February 2008 i ii © Copyright by Zachary C. Owens 2008 All Rights Reserved iii iv I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and...»

«Assessing and Detecting Malicious Hardware in Integrated Circuits By Trey Reece Dissertation Submitted to the Faculty of the Graduate School of Vanderbilt University in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY in Electrical Engineering December, 2014 Nashville, TN Approved: William H. Robinson, Ph.D. Bharat L. Bhuva, Ph.D. Gabor Karsai, Ph.D. Thomas D. Loveless, Ph.D. Bradley A. Malin, Ph.D. ELECTRICAL ENGINEERING Assessing and Detecting Malicious Hardware...»

«Page no.57 4. The Superman/Kent hypothesis: On the epistemological limit between human and superhuman. Alexandros Schismenos PhD Scholar Philosophy of Science University of Ioannina Greece ORCID iD: http://orcid.org/0000-0001-8490-4223 E-Mail: abonapartis@gmail.com Abstract Everybody knows that Superman is Clark Kent. Nobody knows that Superman is Clark Kent. Located between these two absolute statements is the epistemological limit that separates the superhero fictitious universe from our...»

«Sodomy by Eugene Rice Encyclopedia Copyright © 2015, glbtq, Inc. Entry Copyright © 2004, glbtq, inc. A painting (ca 1400) of Reprinted from http://www.glbtq.com Dominican theologian Thomas Aquinas by The Biblical inhabitants of Sodom and Gomorrah had long been notorious for their lack Gentile da Fabriano. of hospitality, arrogance, idolatry, injustice, oppression, and neglect of the poor. The one sex-specific sin attributed to the Sodomites in Genesis was to threaten strangers with anal rape....»

«Combined Photoand Thermionic Electron Emission from Low Work Function Diamond Films by Tianyin Sun A Dissertation Presented in Partial Fulfillment of the Requirements for the Degree Doctor of Philosophy Approved November 2013 by the Graduate Supervisory Committee: Robert Nemanich, Chair Fernando Ponce Xihong Peng John Spence Michael Treacy ARIZONA STATE UNIVERSITY December 2013 ABSTRACT In this dissertation, combined photo-induced and thermionic electron emission from low work function diamond...»

«Pre-Course Handbook BA (Hons) Professional Cookery with foundation London Geller College of Hospitality & Tourism BA (Hons) Food and Professional Cookery with foundation Course Handbook 2016-2017 Section BA (Hons) Food and Professional Cookery with foundation Course Handbook Contents Page No. Section 1 Key Information 1.1 Welcome to the Course 4 1.2 Overview of the Course 5 1.3 Sources of Help and Support 6 1.4 Facts and Figures 8 1.5 Your Responsibilities 9 Section 2 Structure and Content 2.1...»

«RANDOM SAMPLING IN GRAPH OPTIMIZATION PROBLEMS a dissertation submitted to the department of computer science and the committee on graduate studies of stanford university in partial fulfillment of the requirements for the degree of doctor of philosophy By David R. Karger January 1995 c Copyright 1995 by David R. Karger All Rights Reserved ii I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of...»

«CHAUCER AND MORAL PHILOSOPHY: THE VIRTUOUS WOMEN OF THE CANTERBURYTALES By: Denise Baker Baker, Denise. “Chaucer and Moral Philosophy: The Virtuous Women of the Canterbury Tales.” Medium Aevum 60 (1992): 241-256.Made available courtesy of The Society for the Study of Medieval Languages and Literature: http://mediumaevum.modhist.ox.ac.uk/ ***Note: Figures may be missing from this format of the document In The Regement of Princes, Hoccleve insists that Chaucer is not only the equal of Cicero...»

«MICHAEL PALENCIA-ROTH ABBREVIATED CURRICULUM VITAE Trowbridge Scholar in Literary Studies Professor of Comparative and World Literature University of Illinois Program in Comparative and World Literature 3030 FLB – MC 160 University of Illinois Urbana, Illinois 61801 (217) 244-2709; fax (217) 333-4987 e-mail: palencia@uiuc.edu Education: Harvard University: Ph.D., 1976 (Comparative Literature) Harvard University: M.A., 1971 (Comparative Literature) Vanderbilt University: B.A., 1968 (English &...»

«THE 13th INTERNATIONAL CONFERENCE OF ISSEI International Society for the Study of European Ideas in cooperation with the University of Cyprus On Nietzsche’s Concept of ‘European Nihilism’ Ruth Burch (PhD in Philosophy, Warwick University) Via Boggia 10 CH-6900 Lugano-Paradiso, Ticino Switzerland Email: burchru@hotmail.com In Nietzsche’s view, the traditional scientists and philosophical moralists are ultimately unstoppably attracted to nihilism. That is why, in The Gay Science,...»

«COACHES MANUAL 3-5 YEAR OLDS WELCOME TO YMCA YOUTH SPORTS Thank you for agreeing to be a coach in the YMCA Youth Sports program. As a YMCA coach, you will introduce a group of young people to the game of soccer. We ask you to not only teach your players the basis skills and rules of the game, but also make learning the game a joyful experience for them. You see, we want them to play soccer not only for this season, but also for many years to come, and we want you to have fun teaching soccer...»

«High hopes and broken promises: Common and diverse concems of Iranian Women for gender equality in education and employment A thesis submitted to the Graduate and Postdoctoral Studies Office In partial fulfillment of the requirements of the degree of Doctor of Philosophy By Minoo Derayeh (7718905) Department of Integrated Studies in Education Faculty of Education McGill University, Montreal, Canada (May 2002) @ Minoo Derayeh, May 2002 National Library Bibliothèque nationale 1+1 of Canada du...»





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