A complete logic for behavioural equivalence in coalgebras of finitary set functors
| Autor: | David Sprunger |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Calculus of functors
Logic Derived functor Functor category 0102 computer and information sciences 02 engineering and technology Mathematics::Algebraic Topology 01 natural sciences Theoretical Computer Science Algebra Computational Theory and Mathematics Mathematics::K-Theory and Homology 010201 computation theory & mathematics Computer Science::Logic in Computer Science Mathematics::Category Theory Natural transformation Ext functor 0202 electrical engineering electronic engineering information engineering Tor functor 020201 artificial intelligence & image processing Exact functor Adjoint functors Software Mathematics |
| Zdroj: | Journal of Logical and Algebraic Methods in Programming. 94:184-199 |
| ISSN: | 2352-2208 |
| Popis: | This paper presents a sound and complete sequent-style deduction system for determining behavioural equivalence in coalgebras of finitary set functors preserving weak pullbacks. We also prove soundness without the weak pullback requirement. Finitary set functors are investigated because they are quotients of polynomial functors: the polynomial functor provides a ready-made signature and the quotient provides necessary additional axioms. We also show that certain operations on functors can be expressed with uniform changes to the presentations of the input functors, making this system compositional for a range of widely-studied classes of functors, including the Kripke polynomial functors. Our system has roots in the F L R 0 proof system of Moschovakis et al., particularly as used by Moss, Wennstrom, and Whitney for non-wellfounded sets. Similarities can also be drawn to expression calculi in the style of Bonsangue, Rutten, and Silva. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect