This paper is available on arxiv under CC BY-SA 4.0 DEED license. Authors: (1) Tomáš Jakl, Czech Academy of Sciences and Czech Technical University; (2) Dan Marsden, School of Computer Science University of Nottingham; (3) Nihil Shah, Department of Computer Science University of Oxford. Table of Links Abstract & Introduction Prelimenaries FVM Theorems for Positive Existential Fragments FVM Theorems for Counting Logic FVM Theorems for The Full Logic Abstract FVM Theorems for Products Adding Equality and Other Enrichment Conclusions, Acknowledgments & References Appendix A FVM theorems for coproducts Appendix B Proofs Omitted from Section III Appendix C Proofs Omitted from Section IV Appendix D Proofs Omitted from Section V Appendix E Proofs Omitted from Section VI Appendix F Proofs Omitted from Section VII II. PRELIMINARIES A. Categories of Relational Structures We assume the basic definitions of category theory, including categories, functors and natural transformations, as can be found in any standard introduction such as [29] or [30]. Background on comonads, and any less standard material is introduced as needed. troduced as needed. A relational signature σ is a set of relation symbols, each with an associated strictly positive natural number arity. A σstructure A consists of a universe set, also denoted A, and for each relation symbol R ∈ σ of arity n, an n-ary relation RA on A. A morphism of σ-structures f : A → B is a function of type A → B, preserving relations, in the sense that for n-ary R ∈ σ For a fixed σ, σ-structures and their morphisms form our main category of interest R(σ). We will also have need of the category of pointed relational structures R∗(σ). Here the objects (A, a) are a σ-structure A with a distinguished element a ∈ A. The morphisms are σ-structure morphisms that also preserve the distinguished element. B. Comonads The intuition for each of these comonads is that they encode the moves within one structure during the corresponding model comparison game. We shall introduce their mathematical properties as needed in later sections. See [11] for detailed discussions of all three comonads.
Share Your Thoughts