Concurrency in Interaction Nets and Graph Rewriting

Effectué en cotutelle entre le département de Philosophie de l'Università Roma Tre et le Laboratoire d'Informatique de l'Université Paris 13In this work, we study concurrency in non-deterministic extensions of Lafont's interaction nets (a graphical language for functional calculus). These extensions are essentially of three types: multiruled, with multiports and multiwired. They can be combined creating thus seven types of concurrent interaction nets. A first task is to determine a good structural operational semantics to be able to compare the behaviors of these extensions. Based on a known technique in graph rewriting - double pushout with borrowed contexts - we define a method of labeling transitions using derivation rules in the style of process calculi, usual paradigm for modeling concurrency. Moreover, we define an observational semantics based on a parametric notion of barbs, that allows us to give a precise notion of translation between systems. We consider an extensions is more expressive than another if all languages from the second one can be translated into a language of the first one. This allows us to classify the concurrent interaction nets systems into three layers. From the strongest to the weakest: nets with multiport cells, nets with multiwires and finally multiruled nets. Using this, we build a universal language for concurrent interaction nets, which study enlightens us on the fundamental bricks of concurrency.Ce travail est une étude approfondie de la concurrence dans les extensions non-déterministes des réseaux d'interaction de Lafont (langage graphique qui représente, lui, le calcul fonctionnel). Ces extensions sont de trois sortes : les réseaux multirègles, multiports et multifils, et leurs combinaisons donnent ainsi sept types de réseaux. Un premier travail consiste à déterminer une bonne sémantique pour pouvoir comparer ces extensions. On cherche à définir un sémantique opérationnelle structurelle sur les réseaux en se basant sur des technique connues de réécriture des graphes, plus particulièrement celle de " double-pushout with borrowed contexts ". Nous définissons à partir de cette méthode un système d'étiquetage des transitions donné par des règles de dérivations dans le style des langages de processus qui sont le paradigme principal pour étudier les systèmes de calcul concurrents. Nous définissons de plus une sémantique observationnelle sur les réseaux basée sur une notion paramétrique de barbe, qui permet enfin de donner avec précision une notion de traduction entre systèmes. On considère qu'une extension est plus expressive qu'une autre si tout langage de la seconde peut être traduit dans un langage de la première. Ceci nous permet de classer l'ensemble des extensions de manière hiérarchique en trois groupe selon la possibilité de traduire un système de réseau dans un autre. Du plus fort au plus faible : les réseaux contenant des multiports ; ensuite ceux contenant des multifils; enfin les réseaux multirègles. Ceci nous permet de donner un langage universel pour les réseaux dont l'étude donne un point de vue neuf sur les briques fondamentales de la concurrence