Siin näed erinevusi valitud versiooni ja hetkel kehtiva lehekülje vahel.

Lõlita võrdlemise vaatele

et:teated:2011:picard [2011/05/10 10:44] (Hetkel kehtiv)
Monika Perkmann tekitatud
Rida 1: Rida 1:
 +[[|CS Theory Seminars]]
 +===== Coinductive graph representation =====
 +**[[|Celia Picard]]**
 +[[|Institut de Recherche en Informatique de Toulouse]]\\
 +[[|Université Paul Sabatier (Toulouse 3)]]
 +**Thursday, 12 May 2011, 14:00** \\
 +Cybernetica Bldg (Akadeemia tee 21), room B 101
 +=== 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