A Complete Logic for Behavioural Equivalence in Coalgebras of Finitary Set Functors

Abstract : 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 select finitary set functors 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, such as the Kripke polynomial functors. Our system has roots in the $FLR_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.
Type de document :
Communication dans un congrès
Ichiro Hasuo. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. Lecture Notes in Computer Science, LNCS-9608, pp.156-173, 2016, Coalgebraic Methods in Computer Science. 〈10.1007/978-3-319-40370-0_10〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01446025
Contributeur : Hal Ifip <>
Soumis le : mercredi 25 janvier 2017 - 15:24:10
Dernière modification le : jeudi 26 janvier 2017 - 09:14:42
Document(s) archivé(s) le : mercredi 26 avril 2017 - 15:47:48

Fichier

 Accès restreint
Fichier visible le : 2019-01-01

Connectez-vous pour demander l'accès au fichier

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

David Sprunger. A Complete Logic for Behavioural Equivalence in Coalgebras of Finitary Set Functors. Ichiro Hasuo. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. Lecture Notes in Computer Science, LNCS-9608, pp.156-173, 2016, Coalgebraic Methods in Computer Science. 〈10.1007/978-3-319-40370-0_10〉. 〈hal-01446025〉

Partager

Métriques

Consultations de la notice

54