Relational and Algebraic Methods in Computer Science: 18th International Conference, RAMiCS 2020, Palaiseau, France, October 26–29, 2020, Proceedings (Theoretical Computer Science and General Issues)

This book constitutes the proceedings of the 18th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2020, which was due to be held in Palaiseau, France, in April 2020. The conference was cancelled due to the COVID-19 pandemic. The 20 full papers presented together with 3 invited abstracts were carefully selected from 29 submissions. Topics covered range from mathematical foundations to applications as conceptual and methodological tools in computer science and beyond. Preface Organization Abstracts of Invited Speakers Probabilistic Bisimulation with Silent Moves Weighted Automata and Quantitative Logics Combining Probabilistic and Non-deterministic Choice Via Weak Distributive Laws Contents Commutative Doubly-Idempotent Semirings Determined by Chains and by Preorder Forests 1 Introduction 2 Cdi-Semirings of Height Two 3 Catalan Semirings 4 Boolean Cdi-Semirings and Directed Graphs 5 Conclusion References A Relation-Algebraic Treatment of the Dedekind Recursion Theorem 1 Introduction 2 Mathematical Preliminaries 3 Relation-Algebraic Version of the Recursion Theorem 4 An Application: The Isomorphism Theorem 5 Variants of the Relation-Algebraic Recursion Theorem 6 Concluding Remarks References Hardness of Network Satisfaction for Relation Algebras with Normal Representations 1 Introduction 2 The (General) Network Satisfaction Problem 3 Normal Representations and CSPs 4 The Universal Algebraic Approach 4.1 Clones 4.2 Canonical Functions 5 Finitely Many Equivalence Classes 6 No Non-trivial Equivalence Relations 7 Examples 8 Conclusion and Future Work References The -Join as a Join with 1 Introduction 2 Preliminaries 3 Typed Tuples 4 The -Join 5 Selection as Join 6 Inverse Image and Maximal Elements 7 The Join of Relations 8 Split, Glue and Pair Relations 9 Interchange Laws for Join 10 Compatibility and Matching 11 About Weak Matching 12 Join and Maximal Elements 13 Conclusion and Outlook 14 Appendix References Bisimilarity of Diagrams 1 Introduction 2 Bisimilarity and Bisimulations of Diagrams 2.1 Category of Diagrams 2.2 Open Morphisms of Diagrams 2.3 Bisimulations of Diagrams 3 Diagrammatic Path Logic 4 Relation to Path Bisimilarities of Open Maps Situations 5 Interlude 6 Existential Theory of Invertible Matrices 6.1 The Existential Theory of Some Rings 6.2 Theory of Matrices 6.3 Decidability in R 6.4 The Rational Case 7 Decidability in Diagrams 7.1 Decidability of Bisimilarity 7.2 Decidability of the Model Checking 8 Future Work References Generating Posets Beyond N 1 Introduction 2 Posets and Series-Parallel Posets 3 Interval Orders and Interval Sequences 4 Posets with Interfaces 5 Further Properties of Iposets 6 Generating Iposets 7 Experiments References Automated Algebraic Reasoning for Collections and Local Variables with Lenses 1 Introduction 2 Related Work 3 State Space Modelling with Lenses 4 Relational Programs in Isabelle/UTP 5 State Space Manipulation 6 Dynamic and Collection Lenses 7 Symmetric Lenses 8 Variables Blocks 9 Insertion Sort 10 Conclusions References Weakening Relation Algebras and FL2-algebras 1 Introduction 2 Congruences of FL2-algebras 3 Congruences in GBI-algebras 4 Discriminator Varieties of GBI-algebras 5 The Double Division Conuclei Construction 6 Conclusion References Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras 1 Introduction 2 Related Work 3 Relation Algebras and Kleene Algebras 4 Associative Array Access 5 Disjoint Sets 6 Verifying Disjoint-Set Forests in Isabelle/HOL 6.1 The Make-Set Operation 6.2 The Find-Set Operation 6.3 Path Compression 6.4 The Find-Set Operation with Path Compression 6.5 The Union-Sets Operation 7 Conclusion References A Hierarchy of Algebras for Boolean Subsets 1 Introduction 2 Related Work 3 Boolean Algebras 3.1 Huntington's Axioms 3.2 Boolean Algebras in Isabelle/HOL 4 Alternative Axiomatisations of Boolean Algebras 4.1 Lee Byrne's Formulation A 4.2 Lee Byrne's Formulation B 4.3 An Equational Axiomatisation Based on Semilattices 5 Subset Boolean Algebras 6 Subset Boolean Algebras with Additional Structure 6.1 Assumptions Derived from the New Axiomatisation 6.2 Stronger Assumptions Based on Join and Complement 6.3 Axioms for Meet 6.4 Stronger Assumptions for Meet 7 Subset Boolean Algebras in Stone Algebras 8 Antidomain Semirings 9 Conclusion References Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL 1 Introduction 2 Kleene Algebra with Tests 3 Propositional Hoare Logic and Invariants 4 State Transformer Semantics for Hybrid Programs 5 Differential Hoare Logic for Flows 6 Differential Hoare Logic for Invariants 7 Differential Refinement Calculi 8 Evolution Commands for Flows 9 Conclusion References Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory*-3pt 1 Introduction 2 Higher-Order Full Lambek Calculus 3 Full Lambek Tripos 4 Girard and Kolmogorov Translation for Triposes References Expressive Power and Succinctness of the Positive Calculus of Relations 1 Introduction 2 Preliminaries 3 Expressive Power Equivalence of PCoR and EP3 3.1 Quantifier Alternation and Dot-Dagger Alternation Hierarchies 4 PCoR Is Exponentially Less Succinct Than EP3 4.1 Proof of Lemma20 5 On the Transitive Closure Extension 6 Conclusion References Stone Dualities from Opfibrations 1 Introduction 2 Opfibered Comprehension 3 Formal Space and Fundamental Adjunction 3.1 Coreflexiveness of Fundamental Adjunction 3.2 Representability of Fundamental Adjunction 4 Formal Spaces from Arrow Opfibered Comprehension 4.1 Chu Spaces 4.2 Topological Systems 5 Formal Spaces from Subobject Opfibered Comprehension 6 Change of Bases 7 Conclusion and Future Work References Preorders, Partial Semigroups, and Quantales 1 Introduction 2 Weak Preorders and Partial Semigroups 3 The Intermediate Value Property and Dividing Maps 4 Preorders and Unital Partial Semigroups 5 Partial Semigroups with Partial Subtraction and Relational Embedding of Quantales 6 Conclusion References Counting and Computing Join-Endomorphisms in Lattices 1 Introduction 2 Background: Join-Endomorphisms and Their Space 3 The Size of the Function Space 3.1 Distributive Lattices 3.2 Non-distributive Case 4 Algorithms 4.1 Meet of Join-Endomorphisms in Distributive Lattices 4.2 Using Subtraction and Downsets to Characterize E(L)S 4.3 Algorithms for Distributive Lattices 4.4 Algorithms for Arbitrary Lattices 4.5 Experimental Results and Small Example 5 Conclusions and Related Work References A Unary Semigroup Trace Algebra 1 Introduction 2 Preliminaries 2.1 Monoid Trace Algebra 2.2 Generalised Reactive Processes 3 Unary Semigroup Trace Algebra 3.1 Axioms 3.2 Semigroup Properties 3.3 Prefix and Subtraction 4 Trace Models 4.1 Parametric Pairs 4.2 Synchronous Traces 5 Related Work 6 Conclusions References The Involutive Quantaloid of Completely Distributive Lattices 1 Introduction 2 Definitions and Elementary Results 3 Involutive Quantaloids 4 Cyclic Elements of Q(L) 5 Raney's Transforms 6 Lattcd Is an Involutive Quantaloid 7 Remarks on the Equational Theory of the Q(L) 8 Conclusions and Future Steps References Computer-Supported Exploration of a Categorical Axiomatization of Modeloids 1 Introduction 2 Modeloids 3 Inverse Semigroups and Modeloids 3.1 Inverse Semigroups in Isabelle/HOL 3.2 Modeloid as Inverse Semigroup 4 Categorical Axiomatization of a Modeloid 4.1 Category Theory in Isabelle/HOL 4.2 Categorical Axiomatization of a Modeloid 5 Algebraic Ehrenfeucht-Fraïssé Games 5.1 Rules of EF Game 5.2 The Derivative and Fraïssé's Method 6 Conclusion References Sharpness in the Fuzzy World 1 Introduction 2 Mathematical Preliminaries 2.1 Dedekind, Arrow and Fuzzy Categories 3 L-Fuzzy Sharpness Problem 4 Conclusion References Author Index