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



Pages:     | 1 |   ...   | 7 | 8 || 10 | 11 |   ...   | 12 |

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

-- [ Page 9 ] --

And it is not hard to see that gen τ is the greatest fixed point of Gτ, with respect to the aforementioned pointwise ordering. Therefore, we can read Corollary 3.4.9 as saying that every post-fixed point of Gτ is below the greatest fixed point of Gτ in that ordering, which is precisely what the coinduction proof technique of [42] mandates. Unlike the latter, we could not have used Tarski’s Lattice-theoretical Fixpoint Theorem (see [61, thm. 1]) to deduce our proof rule here. For if C is a proper class, then Pow Seq(L × C) is not a complete lattice under inclusion, and so neither is the induced ordering of class functions from C to Pow Seq(L × C). Nevertheless, the principle is the same.

Note that an ordered set can be viewed as a category, an order-preserving function on that set as a functor on that category, and a post-fixed point of that function as a coalgebra for that functor. And if that ordered set is a complete lattice, then, by Tarski’s fixed-point theorem, there is a final coalgebra for that functor. And so the coinduction proof technique of [42] is just another variation of the general finality theme that lies behind the coinduction proof principle of Theorem 2.4.2. The same, of course, is true for the more ad hoc proof rule of Corollary 3.4.9.

For a historical account on the emergence of coinduction in computer science, we refer to [58].

We have now finally reached our generability characterization theorem.

Theorem 3.4.11. ε is generable if and only if the following are true:

–  –  –

Thus, by generalization, (c) is true.

For every c and e, if e ∈ (gen τ )(c) and ∈ (gen τ )(c), then, by Corollary 3.4.10, τ (c) = ∅, and hence, e =. Thus, (d) is true.

By Theorem 3.4.5 and the Axiom of Dependent Choice, (e) is true.

Conversely, suppose that (a), (b), (c), (d), and (e) are true.

We prove that ε = gen(η(C) ◦ ε).

Assume c ∈ C and e ∈ ε(c).

, then, by (d), ε(c) = { }, and thus, η(C)(ε(c)) = ∅.

If e = Otherwise, there is l, c, and e such that ·e.

e= l, c Thus, by definition of η, l, c ∈ η(C)(ε(c)), and by (a), e ∈ ε(c ).

Thus, by generalization, ε is consistent with η(C) ◦ ε, and by Corollary 3.4.9, for any c ∈ C, ε(c) ⊆ (gen(η(C) ◦ ε))(c).

–  –  –

And since η(C)(ε(c )) = ∅, by (e), tailj+1 e ∈ ε(c ).

Otherwise, there is k n + 1 such that j + 1 = k. Then there is l, c, l, c, and e2 such that l, c ∈ η(C)(ε(c )) and

–  –  –

Thus, by (c), e2 ∈ ε(c ). And since l, c ∈ η(C)(ε(c)), there is e1 such that l, c · e1 ∈ ε(c). Thus, by (b), l, c · e2 ∈ ε(c), and hence, e ∈ ε(c).

Thus, by generalization, for any c ∈ C, ε(c) ⊇ (gen(h(C) ◦ ε))(c).

Thus, ε = gen(h(C) ◦ ε), and hence, ε is generable.

Clause (a) of Theorem 3.4.11 corresponds to suffix closure, clause (b), conditioned on (a), to fusion closure, and clause (c) to limit closure. Clause (d) asserts the impossibility of indeterminate termination. Finally, clause (e) is the non-triviality condition discussed earlier, and essentially replaces Emerson’s left totality condition on the generating transition relation (see [20]).

Each of these five properties has come about in connection with a different cause of failure of the converse of Proposition 3.3.4, and hence of Proposition 3.3.1 and 3.3.2. And if we have been thorough enough, we should expect that the conjunction of all five properties be sufficient a condition for eliminating that failure altogether. This turns out to be the case.

We say that C, ε is generable if and only if ε is generable.

Theorem 3.4.

12. If C1, ε1 and C2, ε2 are generable, then h is a homomorphism from C1, ε1 to C2, ε2 if and only if h is a homomorphism from the L-labelled transition coalgebra C1, η(C1 ) ◦ ε1 to the L-labelled transition coalgebra C2, η(C2 ) ◦ ε2.

–  –  –

Then, by Proposition 3.3.1, h is a homomorphism from the L-labelled transition coalgebra C1, η(C1 ) ◦ ε1 to the L-labelled transition coalgebra C2, η(C2 ) ◦ ε2.

Conversely, suppose that h is a homomorphism from C1, η(C1 ) ◦ ε1 to C2, η(C2 ) ◦ ε2.

Let ε2 be a class function from C2 to Pow Seq(L × C2 ) such that for any c2 ∈ C2,

–  –  –

And since h is a homomorphism from C1, η(C1 ) ◦ ε1 to C2, η(C2 ) ◦ ε2, l, h(c1 ) ∈ (η(C2 ) ◦ ε2 )(c2 ).

Thus, by generalization, ε2 is consistent with η(C2 ) ◦ ε2. Then, by Corollary 3.4.9, for any c2 ∈ C 2,

–  –  –

Therefore, for any c1 ∈ C1, (Pow Seq(L × h))(ε1 (c1 )) ⊆ ε2 (h(c1 )).

We use induction to prove that for any c1 ∈ C1 and any finite e2 ∈ ε2 (h(c1 )), there is e1 ∈ ε1 (c1 ) such that

–  –  –

, then (η(C2 ) ◦ ε2 )(h(c1 )) = ∅, and since h is a homomorphism from If e2 = C1, η(C1 ) ◦ ε1 to C2, η(C2 ) ◦ ε2, (η(C1 ) ◦ ε1 )(c1 ) = ∅. Thus, ∈ ε1 (c1 ).

Otherwise, by Corollary 3.4.10, there is l, c2, and e2 such that l, c2 ∈ (η(C2 ) ◦ ε2 )(h(c1 )), e2 ∈ ε2 (h(c1 )), and

–  –  –





and tailn+1 e2 ∈ ε2 (h(c1 )). Thus, by Corollary 3.4.10, there is l, c2, and e2 such that l, c2 ∈ (η(C2 ) ◦ ε2 )(h(c1 )), e2 ∈ ε2 (c2 ), and

–  –  –

Thus, by generalization, for every s ∈ S, there is s such that s R s. Then, by the Axiom of Dependent Choice, there is an infinite sequence d over S such that for every n ∈ ω, head tailn d R head tailn+1 d.

Let n = sec head d.

We use induction to prove that for every j n + 1, there is l, c1, and e1 such that l, c1, j ∈ W (j), e1 ∈ ε1 (c1 ), and

–  –  –

(Seq(L × h))( l, c1 · (Seq(proj1 ((L × C1 ) × ω)))(tail d)) = tailj e2.

Otherwise, there is k n + 1 such that j + 1 = k. By the induction hypothesis, there is l, c1, and e1 such that l, c1, k ∈ W (k), e1 ∈ ε1 (c1 ), and

–  –  –

Since l, c1, k ∈ W (k), there is l, c1, j ∈ W (j) such that l, c1 ∈ (η(C1 ) ◦ ε1 )(c1 ) and head tailk e2 = l, h(c1 ). And clearly, l, c1 · e1 ∈ ε1 (c1 ) and

–  –  –

The following is immediate from Theorem 2.2.10 and 3.4.12:

Theorem 3.4.

13. If C1, ε1 and C2, ε2 are generable, then B is a bisimulation between C1, ε1 and C2, ε2 if and only if B is a bisimulation between the L-labelled transition coalgebra C1, η(C1 ) ◦ ε1 and the L-labelled transition coalgebra C2, η(C2 ) ◦ ε2.

Once more, we can translate all this back to the system side of the theory.

Assume a binary relation T : S ↔ L × S.

Assume a binary relation E : S ↔ S (L × S).

We write ET (E) for a binary relation between S and S (L × S) such that for any s ∈ S and every e ∈ S (L × S),

–  –  –

The following is trivial:

Proposition 3.4.14. ET (E) = rel Gfun T (fun E).

We think of ET as a function on binary relations between S and S (L × S). And the reason that we are interested in this function is that it preserves the ordering of binary relations between S and S (L × S) induced by the inclusion relation on their graphs: for every binary relation E1, E2 : S ↔ S (L × S), if

–  –  –

This ordering is of course a complete lattice, and hence, by Tarski’s Lattice-theoretical Fixpoint Theorem, so is the set of all fixed points of ET.

We write exec T for the greatest fixed point of ET.

Notice that here, the coinduction proof technique of [42] is directly applicable.

The following follows from Proposition 3.4.14 and the fact that gen fun T is the greatest fixed point of Gfun T :

–  –  –

We say that T generates E if and only if exec T = E.

We say that E is generable if and only if there is a binary relation between S and L × S that generates E.

The following is immediate from Proposition 2.2.1 and 3.4.15:

Proposition 3.4.16. E is generable if and only if fun E is generable.

The following is immediate from Proposition 2.2.1, 3.3.3, 3.4.15, and 3.4.16:

Proposition 3.4.17. The following are true:

–  –  –

(b) if E is generable, then exec trans E = E.

We say that S, E is generable if and only if E is generable.

The following is immediate from Proposition 3.4.16:

Proposition 3.4.18. S, E is generable if and only if the L-labelled execution coalgebra S, fun E is generable.

The following is immediate from Proposition 2.2.1(b), 2.2.15, 3.2.4, and 3.3.3, and

Theorem 3.4.13:

Theorem 3.4.

19. If S1, E1 and S2, E2 are generable, then B is a bisimulation between S1, E1 and S2, E2 if and only if B is a bisimulation between the L-labelled transition systems S1, trans E1 and S2, trans E2.

We would like to finish this section with a few remarks.

Proposition 3.4.17 and Theorem 3.4.19 confirm what has been implicit throughout this section: generable labelled execution systems are just another representation of labelled transition systems. This is even more evident in the coalgebra side of the theory, where, by Proposition 3.4.7 and Theorem 3.4.12, the category of all generable labelled execution coalgebras and all homomorphisms between them is isomorphic to (Pow ◦ (L × Id))-Coalg.

Thus, for all practical purposes, generable labelled execution coalgebras are equivalent to labelled transition coalgebras.

In light of this equivalence, Theorem 3.4.11 does not just characterize generable labelled execution coalgebras. It marks the boundary between the expressive power of labelled transition coalgebras and labelled execution coalgebras. And what it implies is that there CHAPTER 3. EXECUTION SYSTEMS 86 is no sense in choosing the latter over the former, unless we are willing to give up one or more of the five properties listed in the respective clauses of Theorem 3.4.11.

In the next chapter, we will give up two of these properties: limit closure and impossibility of indeterminate termination. Giving up limit closure will enable us to faithfully model the finite delay property, so intrinsically bound to the notion of asynchrony. And indeterminate termination will provide us with the means to simulate the behaviour of a capricious environment that may at any time cease to produce input stimuli.

3.5 Behaviour modelling and covarieties In Section 2.4, in order to motivate the study of final coalgebras, we considered a hypothetical scenario, in which we used L-labelled transition systems to model the behaviour of processes of some kind. And for simplicity, we assumed that any state of every L-labelled transition system modelled the behaviour of some process of that kind.

Here, we wish to consider a different scenario, in which we use L-labelled execution systems instead. And this time, we make no such simplifying assumption.

We have already seen examples of labelled execution systems that are not suitable for modelling the behaviour of processes. In Section 3.3, we argued that non-Abrahamson systems should be excluded from consideration. And in the next chapter, we will exclude even more systems, leaving only those that conform with our intuitive notion of behaviour of an asynchronous process.

In cases like these, a final L-labelled execution coalgebra is no longer the right choice of model. Sure, every behaviour modelled within the class of systems under consideration is accounted for exactly once in such a coalgebra. But there are more behaviours in there, which are neither needed nor wanted. What is required then is a suitable generalization of the final coalgebra approach of the previous chapter.

We will need a couple of last concepts from category theory.

A subcategory of a category is a collection of objects and arrows of that category that is closed under the identity, domain, codomain, and composition operation of that category.

A full subcategory of a category is a subcategory of that category, whose arrows between any two objects are all the arrows between the two objects in that category.

Notice that a full subcategory is completely determined by its objects.

In Section 2.4, we were interested in the terminal object of F -Coalg. Here, by a similar reduction, we are interested in the terminal object of a full subcategory of F -Coalg.

CHAPTER 3. EXECUTION SYSTEMS 87 Assume a full subcategory S of F -Coalg.

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

Clearly, not every full subcategory of F -Coalg has a final F -coalgebra. But as we will see, every “reasonably specified” one does.

We say that S is closed under the formation of homomorphic images if and only if for every F -coalgebra C, γ, if C, γ is in S, and C, γ is a homomorphic image of C, γ, then C, γ is in S.

We say that S is closed under the formation of subcoalgebras if and only if for every F -coalgebra C, γ, if C, γ is in S, and C, γ is a subcoalgebra of C, γ, then C, γ is in S.

We say that S is closed under the formation of direct sums if and only if for every class-indexed family { Ci, γi }i∈I of F -coalgebras, if for every i ∈ I, Ci, γi is in S, then i∈I Ci, γi is in S.

Definition 3.5.1. An F -covariety is a full subcategory C of F -Coalg such that the

following are true:

(a) C is closed under the formation of homomorphic images;

(b) C is closed under the formation of subcoalgebras;

(c) C is closed under the formation of direct sums.



Pages:     | 1 |   ...   | 7 | 8 || 10 | 11 |   ...   | 12 |


Similar works:

«A NEW WAY TO THINK ABOUT PRESS FREEDOM: NETWORKED JOURNALISM AND A PUBLIC RIGHT TO HEAR IN AN AGE OF ―NEWSWARE‖ A DISSERTATION SUBMITTED TO THE DEPARTMENT OF COMMUNICATION AND THE COMMITTEE OF GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Mike Ananny March 2011 © 2011 by Michael Joseph Ananny. All Rights Reserved. Re-distributed by Stanford University under license with the author. This work is licensed under a...»

«CASTLES AND LANDSCAPES: AN ARCHAEOLOGICAL SURVEY OF YORKSHIRE AND THE EAST MIDLANDS VOLUME I Thesis submitted for the degree of Doctor of Philosophy at the University of Leicester by Oliver Hamilton Creighton School of Archaeological Studies University of Leicester December 1998 UMI Number: U117043 All rights reserved INFORMATION TO ALL USERS The quality of this reproduction is dependent upon the quality of the copy submitted. In the unlikely event that the author did not send a complete...»

«The Interpretation of Marketing Actions and Communications by the Financial Markets Isaac Max Dinner Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy under the Executive Committee of the Graduate School of Arts and Sciences COLUMBIA UNIVERSITY 2011 UMI Number: 3454131 All rights reserved INFORMATION TO ALL USERS The quality of this reproduction is dependent upon the quality of the copy submitted. In the unlikely event that the author did not send a...»

«DEVELOPMENT OF VALID MODELS FOR STRUCTURAL DYNAMIC ANALYSIS A thesis submitted for the degree of Doctor of Philosophy By Jose Vicente García Department of Mechanical Engineering Imperial College London – University of London October 2008 I declare that this thesis is my own work and that where any material could be construed as the work of others, it is fully cited and referenced. Jose Vicente García nd 2 October 2008 To Laura Abstract Abstract In the aeroengine industry, simulation models...»

«Exploring a Holistic Content Approach to Personal Meaning Zvi J. Bellin B.A. Binghamton University M.A. New York University Submitted to the Department of Pastoral Counseling of Loyola University in Maryland In Partial Fulfillment of the Requirement for the Degree of Doctor of Philosophy [Counselor Education/Pastoral Counseling] December 7, 2009 ACKNOWELDGEMENTS Thank you to the source of all being and blessing. I would like to acknowledge several authors whose works have inspired me to think...»

«OPTIMIZATION OF ANAEROBIC DEGRADATION OF 1,1,1-TRICHLORO-2,2-DI(4CHLOROPHENYL)ETHANE (DDT), 1-CHLORO-4-[2,2-DICHLORO-1-(4CHLOROPHENYL)EHTYL]BENZENE (DDD) AND 1,1-BIS-(4-CHLOROPHENYL)-2,2DICHLOROETHENE (DDE) IN ORGANIC MUCK SOILS OF LAKE APOPKA By HIRAL GOHIL A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY UNIVERSITY OF FLORIDA © 2011 Hiral Gohil To my parents ACKNOWLEDGMENTS I express...»

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

«Patterns and Consequences of Competition for Pollination between Introduced and Native Species with Different Floral Traits by Benjamin R. Montgomery A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Biology) in The University of Michigan 2007 Doctoral Committee: Associate Professor Beverly J. Rathcke, Chair Professor Deborah E. Goldberg Professor Earl E. Werner Emily D. Silverman, U.S. Fish and Wildlife Service Acknowledgements As I...»

«Epistemic Contextualism: A Normative Approach Robin McKenna University of Edinburgh rbnmckenna@gmail.com Penultimate draft. Final version forthcoming in Pacific Philosophical Quarterly. Abstract In his Knowledge and Practical Interests Jason Stanley argues that the view he defends, which he calls interest-relative invariantism, is better supported by certain cases than epistemic contextualism. In this paper I argue that a version of epistemic contextualism that emphasizes the role played by the...»

«Syed ​Zafar​ ul Hussan ​Gilani William Gates Building, 15 JJ Thomson Ave, Cambridge CB3 0FD, UK +44 7459 789978 | ​Cambridge email​ | ​Personal email​ | ​Webpage​ | ​Github​ | ​LinkedIn​ | ​Google Scholar CURRENT RESEARCH INTERESTS: Distributed Systems, Social Network Analysis, Information Propagation/Dissemination EDUCATION: ● Aug 2017, University of Cambridge Doctor of Philosophy (Ph.D.) in Computer Science Dissertation: “Measuring and Modelling the impact of...»

«Revised August 2015 Curriculum Vita J. Michael Martinez, Ph.D. Assistant Professor School of Kinesiology Louisiana State University Baton Rouge, LA jmmartinez@lsu.edu Education Doctor of Philosophy: Middle Tennessee State University Murfreesboro, TN Program: Human Performance May, 2009 Specialization: Sport Management Master of Science: The University of Southern Mississippi Hattiesburg, MS Program: Public Relations May, 2003 Bachelor of Science: The University of Southern Mississippi...»

«GRAPHENE MODIFIED INDIUM TIN OXIDE ELECTRODES FOR ORGANIC SOLAR CELLS CHANG CI’EN SHARON (B. Sc.(Hons.), NATIONAL UNIVERSITY OF SINGAPORE) A THESIS SUBMITTED FOR THE DEGREE OF DOCTOR OF PHILOSOPHY NUS GRADUATE SCHOOL FOR INTEGRATIVE SCIENCES AND ENGINEERING NATIONAL UNIVERSITY OF SINGAPORE & DEPARTMENT OF MATERIALS IMPERIAL COLLEGE LONDON Declaration I hereby declare that this thesis is my original work and it has been written by me in its entirety. I have duly acknowledged all the sources of...»





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