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

— |
et:teated:2011:picard [2011/05/10 10:44] (Hetkel kehtiv) Monika Perkmann tekitatud |
||
---|---|---|---|

Rida 1: | Rida 1: | ||

+ | [[http://cs.ioc.ee/~tarmo/tsem10/|CS Theory Seminars]] | ||

+ | ---- | ||

+ | ===== Coinductive graph representation ===== | ||

+ | |||

+ | **[[http://www.irit.fr/~Celia.Picard/|Celia Picard]]** | ||

+ | |||

+ | [[http://www.irit.fr/|Institut de Recherche en Informatique de Toulouse]]\\ | ||

+ | [[http://www.ups-tlse.fr/|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 | ||

+ | programme. |