Permutations in Coinductive Graph Representation

Abstract : In the proof assistant Coq, one can model certain classes of graphs by coinductive types. The coinductive aspects account for infinite navigability already in finite but cyclic graphs, as in rational trees. Coq’s static checks exclude simple-minded definitions with lists of successors of a node. In previous work, we have shown how to mimic lists by a type of functions and built a Coq theory for such graphs. Naturally, these coinductive structures have to be compared by a bisimulation relation, and we defined it in a generic way.However, there are many cases in which we would not like to distinguish between graphs that are constructed differently and that are thus not bisimilar, in particular if only the order of elements in the lists of successors is not the same. We offer a wider bisimulation relation that allows permutations. Technical problems arise with their specification since (1) elements have to be compared by a not necessarily decidable relation and (2) coinductive types are mixed with inductive ones. Still, a formal development has been carried out in Coq, by using its built-in language for proof automation.Another extension of the original bisimulation relation based on cycle analysis provides indifference concerning the root node of the term graphs.
Type de document :
Communication dans un congrès
Dirk Pattinson; Lutz Schröder. 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Mar 2012, Tallinn, Estonia. Springer, Lecture Notes in Computer Science, LNCS-7399, pp.218-237, 2012, Coalgebraic Methods in Computer Science. 〈10.1007/978-3-642-32784-1_12〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01539884
Contributeur : Hal Ifip <>
Soumis le : jeudi 15 juin 2017 - 15:02:46
Dernière modification le : mercredi 12 septembre 2018 - 17:46:03
Document(s) archivé(s) le : mercredi 13 décembre 2017 - 12:07:27

Fichier

978-3-642-32784-1_12_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Célia Picard, Ralph Matthes. Permutations in Coinductive Graph Representation. Dirk Pattinson; Lutz Schröder. 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Mar 2012, Tallinn, Estonia. Springer, Lecture Notes in Computer Science, LNCS-7399, pp.218-237, 2012, Coalgebraic Methods in Computer Science. 〈10.1007/978-3-642-32784-1_12〉. 〈hal-01539884〉

Partager

Métriques

Consultations de la notice

90

Téléchargements de fichiers

32