Coinductive Graph Representation: the Problem of Embedded Lists

Célia Picard (1) , Ralph Matthes (2, 3)

1 IRIT - Institut de recherche en informatique de Toulouse
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
3 CNRS - Centre National de la Recherche Scientifique

When trying to obtain formally certified model transformations, one may want to represent models as graphs and graphs as greatest fixed points. To do so, one is rather naturally led to define co-inductive types that use lists (to represent a finitebut unbounded number of children of internal nodes). These concepts are rather well supported in the proof assistant Coq. However, their use in our intended applications may cause problems since the co-recursive call in the type definition occurs in the list parameter. When defining co-recursive functions on such structures, one will face guardedness issues, and in fact, the syntactic criterion applied by the Coq system is too rigid here.We offer a solution using dependent types to overcome the guardedness issues that arise in our graph transformations. We also give examples of further properties and results, among which finiteness of represented graphs. All of this has been fully formalized in Coq

Mots clés: theorem proving; guardedness; dependent types; metamodels; coinduction/corecursion

Domaines: Théorie et langage formel [cs.FL]

Célia Picard, Ralph Matthes. Coinductive Graph Representation: the Problem of Embedded Lists. Electronic Communications of the EASST, 2011, Graph Computation Models Selected Revised Papers from the Third International Workshop on Graph Computation Models (GCM 2010), 39. ⟨hal-02015853⟩