## Coinductive graph representation

Institut de Recherche en Informatique de Toulouse

Université Paul Sabatier (Toulouse 3)

Thursday, 12 May 2011, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**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. We
show how to mimic lists by a type of functions and build a Coq theory
for such graphs. Naturally, these coinductive structures have to be
compared by a bisimulation relation, and we define 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 present 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.

(Joint work with Ralph Matthes.)

Celia Picard's visit to Tallinn is supported by the ETF/Egide
Parrot programme.

Tarmo Uustalu

Last update 14.5.2011