- Renseignements pratiques
- Enseignement
Contact
LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2
Email:
contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37
Accéder aux Rapports de l'année : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018
RR-2006-01 Abstract Branching for Quantified Formulas
Marco Benedetti
Résumé :
Mot(s) Clé(s) :
RR-2006-02 Minimal proper interval completions
Ivan Rapaport, Karol Suchan, Ioan Todinca
Résumé : Nous étudions le problème d'ajout d'arêtes à un graphe quelconque pour que le graphe obtenu soit un graphe d'intervalles propres. Notre objectif est d'ajouter un ensemble minimal d'arêtes. Ce qui signifie qu'aucun sous-ensemble propre des arêtes supplémentaires ajoutées au graphe de départ ne peut donner un graphe d'intervalles propres. Ce problème est proche du problème d'ajout d'un ensemble minimal d'arêtes à un graphe pour obtenir un graphe triangulé ou un graphe d'intervalles. Cependant, tandis qu'il existe des algorithmes pour obtenir un graphe triangulé ou un graphe d'intervalles de cette façon, le problème analogue d'obtention d'un graphe d'intervalles propres était ouvert jusqu'à présent. Dans ce papier, nous donnons un algorithme en temps linéaire pour obtenir une complétion d'intervalles propres minimale d'un graphe quelconque, ainsi nous résolvons la complexité de ce problème.
Mot(s) Clé(s) : graphe, triangulation, intervalle, propre, complétion, exploration, complexité, algorithme, polynômial, linéaire.
RR-2006-03 Automata for Analyzing and Querying Compressed Documents
Siva Anantharaman, Barbara Fila
Résumé : In a first part of this work, tree/dag automata are defined as extensions of (unranked) tree automata which can run indifferently on trees or dags; they can thus serve as tools for analyzing or querying any semi-structured document, whether or not given in a compressed format. In a second part of the work, we present a method for evaluating positive queries expressed in terms of Core XPath axes, on any XML document t, compressed or not. To each Core XPath location step of a certain basic type, we associate an automaton; these automata run on the hedges of the minimal straightline regular tree grammar associated to the document, or on its dependency dag. Any given Core XPath query can be decomposed into queries of the basic type; and the answers to the query can then be expressed as a sub-document of t, suitably labeled under the runs of such automata.
Mot(s) Clé(s) : Tree automata, Tree grammars, Dags, XML, Core XPath.
RR-2006-04 Deciding Satisfiability of positive Second Order Joinability Formulae
Sébastien Limet, Pierre Pillot
Résumé : Ce rapport traite d'une classe de formules du second ordre où le seul prédicat est la joignabilité modulo un système de réécriture conditionnel, les variables du premier ordre étant des termes clos et les variables du second ordre sont interprétées comme des relations sur les termes clos (c.à.d des ensembles de n-uplet de termes clos). On définit un algorithme générique qui décide de la satisfiabilité des formules positives de joignabilités du second ordre quand un algorithme est connu concernant la représentation finie des solutions des formules du premier ordre correspondant. Le résultat est alors un programme logique qui représente les instances des variables du second ordre. On applique cette technique a la classe des formules positives pseudo-régulière du second ordre. On définit également une transformation qui traduit cette instance sous forme de système de réécriture conditionnel. Notre technique peut être utilisée pour synthétiser automatiquement un programme qui définit une relation par sa spécification.
Mot(s) Clé(s) : programmation logique; système de réécriture; langage d'arbres; second ordre.
RR-2006-05 Solving First-Order Constraints in the Theory of the Evaluated Trees
Thi-Bich-Hanh Dao, Khalil Djelloul
Résumé : Nous présentons dans ce papier un algorithme général de résolution de contraintes du premier ordre dans la théorie T des arbres évalués. Cette théorie est une combinaison de la théorie des arbres finis ou infinis et de la théorie des rationnels munis de l'addition, de la soustraction et d'une relation d'ordre dense sans extrême. L'algorithme est donné sous forme d'un ensemble de 28 règles de réécriture et transforme toute formule du premier ordre P, qui peut éventuellement contenir des variables libres, en une disjonction Q de formules résolues, équivalente à P dans T, sans nouvelles variables libres, et telle que Q est soit la formule Vrai, soit la formule Faux, soit une formule ayant au moins une variable libre et n'étant équivalente ni à Vrai ni à Faux dans T. En particulier, si P est sans variables libres, Q est soit la formule Vrai soit la formule Faux. Si Q contient des variables libres, les solutions sur ces variables sont exprimées d'une façon explicite et Q peut se transformer directement en une combinaison booléenne de conjonctions quantifiées de formules atomiques, qui n'acceptent pas d'élimination de quantificateurs. La correction de notre algorithme est une autre preuve de la complétude de la théorie T.
Mot(s) Clé(s) : contraintes du premier ordre; théorie des arbres; théorie des rationnels additifs ordonnés; résolution de contraintes; règles de réécriture.
RR-2006-07 Extension of First-Order Theories into Trees
Khalil Djelloul, Thi-Bich-Hanh Dao
Résumé : We present in this paper an automatic way to combine any first-order theory T with the theory of finite or infinite trees. First of all, we present a new class of theories that we call zero-infinite-decomposable and show that every decomposable theory T accepts a decision procedure in the form of six rewriting which for every first order proposition give either true or false in T. We present then the axiomatization T* of the extension of T into trees and show that if T is flexible then its extension into trees T* is zero-infinite-decomposable and thus complete. The flexible theories are theories having elegant properties which enable us to eliminate quantifiers in particular cases.
Mot(s) Clé(s) : first-order theories, theory of finite or infinite trees. complete theories.
RR-2006-08 Minimal interval completion through graph exploration
Karol Suchan, Ioan Todinca
Résumé : Etant donne un graphe quelconque $G=(V,E)$, un graphe d?intervalles $H=(V,E)$ est appelé complétion d?intervalles de $G$ si $E \subseteq F$. Le graphe $H$ est appelé complétion d?intervalles minimales si, pour tout graphe sandwich $H? = (V, F?)$ avec $E \subseteq F? \subset F$, $H?$ n?est pas un graphe d?intervalles. Nous présentons dans cet article un algorithme de complexité $\mathcal{O}(nm)$ calculant une complétion d?intervalles minimale d?un graphe quelconque.
Mot(s) Clé(s) : graphe, triangulation, intervalle, propre, complétion, exploration, complexité, algorithme, polynômial, linéaire.
RR-2006-09 Characterizing minimal interval completions: Towards better understanding of profile and pathwidth
Pinar Heggernes, Karol Suchan, Ioan Todinca, Yngve Villanger
Résumé : Les complétions d?intervalles minimales sont au coeur de la compréhension de deux paramètres de graphes très étudiés : la largeur arborescente linéaire (pathwidth) et le profile. L?étude des complétions minimales semble nécessaire pour avancer sur le calcul des deux paramètres. Une complétion d?intervalles d?un graphe est $G$ est un graphe d?intervalles $H$, ayant le même ensemble de sommets que $G$, obtenu en rajoutant des arêtes au graphe $G$. Si, de plus, on ne peut pas enlever une partie des arêtes rajoutées sans détruire la propriété de graphe d?intervalles, nous dirons que $H$ est une complétion d?intervalles minimales. Dans cet article, nous donnons pour la première fois une caractérisation des complétions d?intervalles minimales. Nous présentons également un algorithme polynomial qui extrait, à partir d?une complétion d?intervalles quelconque, une complétion d?intervalles minimale du graphe de départ.
Mot(s) Clé(s) : graphe, triangulation, intervalle, propre, complétion, exploration, complexité, algorithme, polynômial, linéaire.
RR-2006-10 Pathwidth of circular-arc graphs
Karol Suchan, Ioan Todinca
Résumé : La largeur arborescente linéaire (pathwidth) d?un graphe $G$ est définie comme le nombre de clique minimum de $H$ moins un, parmi tous les graphes d?intervalles $H$ contenant $G$. Bien que la largeur arborescente linéaire soit un paramètre bien connu et très étudié, il existe très peu de classes de graphes pour lesquelles on dispose d?algorithmes polynomiaux calculant le paramètre. Nous présentons dans cet article un algorithme de complexité $\mathcal{O}(n2)$, calculant la largeur arborescente linéaire des graphes d?intervalles circulaires.
Mot(s) Clé(s) : graphe, pathwidth, circular-arc, triangulation, intervalle, complétion, complexité, algorithme, polynômial.
RR-2006-11 Problem Modeling and Solving in QCSP made Practical
Marco Benedetti, Arnaud Lallouet, Jérémie Vautard
Résumé :
Mot(s) Clé(s) :
RR-2006-12 La visualisation distante
S. Limet, S. Madougou, E. Melin, S. Robert
Résumé : La visualisation de données est de plus en plus exploitée dans de nombreux domaines scientifiques et devient un élément essentiel dans la compréhension de phénomènes étudiés dans les différentes disciplines scientifiques. De plus, face aux enjeux de la complexité des simulations sous-jacentes et de la taille des données générées, le développement des applications scientifiques se base désormais sur des systèmes parallèles et distribués. Ainsi, il devient classique d'envisager un déploiement d'une application sur plusieurs sites dont un qui réalise l'affichage des résultats. Cet état de l'art s'intéresse à ce dernier point et a été réalisé dans le cadre d'un contrat de recherche avec le CEA/DIF de Bruyères-le-Châtel. Nous nous sommes ainsi intéressés à différentes solutions de visualisation distante afin d'obtenir une classification permettant de juger de leur qualité en fonction des attentes des utilisateurs. Nous avons choisi d'aborder cette classification en fonction du lieu du rendu qui influe sur les performances en terme de taux de rafraîchissement de l'image par rapport à la qualité du réseau. Ce point de vue permet de traiter les différentes méthodes possibles pour répartir le pipeline graphique entre les deux sites impliqués et d'en voir les avantages et les inconvénients. La visualisation distante s'appuie également sur une infrastructure réseau dont dépendent les performances finales. Ces différentes infrastructures possibles seront décrites dans une deuxième partie, ainsi que les concepts plus généraux formalisant les aspects réseau pour des déploiements de type Grid. Enfin, il existe déjà aujourd'hui des systèmes que nous qualifions d'autonomes dédiés directement ou indirectement à la visualisation distante. Ils constituent la dernière partie de ce document et nous permettront de conclure sur la pérennité des systèmes existants et les différentes possibilités pour les systèmes à venir.
Mot(s) Clé(s) :
RR-2006-13 Synchronized-ContextFree Tree-tuple Languages
Jacques Chabin, Jing Chen, Pierre Réty
Résumé : Using logic programs, we define a new class of tree-(tuple) languages, that combines the synchronized-regular tree-(tuple) languages with the context-free tree languages. Thus, this class can express an unbounded counting both in several independent branches (like in a synchronized-regular language), and at two nested positions (like in a context-free language). Despite its bigger expressivity, the new class has the same useful properties as the former ones\,: closure under union, closure under intersection of one tuple-component with a regular tree language, decidability of membership and emptiness. Therefore, it should give rise to many applications.
Mot(s) Clé(s) : tree languages, logic programming, rewriting
RR-2006-14 Visibly Pushdown Languages and Term Rewriting
Jacques Chabin, Pierre Réty
Résumé : To combine tree languages with term rewriting, we introduce a new class of tree languages, that both extends regular languages and restricts context-free languages, and that is closed under intersection (unlike context-free languages). To do it, we combine the concept of visibly pushdown language, with top-down pushdown tree automata, and we get the visibly pushdown tree automata. Then, we use them to express the sets of descendants for a sub-class of growing term rewrite systems, and thanks to closure under intersection, we get that joinability and (restricted) unifiability are decidable.
Mot(s) Clé(s) : tree languages, term rewriting.
Les rapports de recherche du LIFO en 2006
RR-2006-01
Abstract Branching for Quantified Formulas
Marco Benedetti
Date : 2006-06-16
Résumé Télécharger
RR-2006-02
Minimal proper interval completions
Ivan Rapaport, Karol Suchan, Ioan Todinca
Date : 2006-03-09
Résumé Télécharger
RR-2006-03
Automata for Analyzing and Querying Compressed Documents
Siva Anantharaman, Barbara Fila
Date : 2006-03-07
Résumé Télécharger
RR-2006-04
Deciding Satisfiability of positive Second Order Joinability Formulae
Sébastien Limet, Pierre Pillot
Date : 2006-05-29
Résumé Télécharger
RR-2006-05
Solving First-Order Constraints in the Theory of the Evaluated Trees
Thi-Bich-Hanh Dao, Khalil Djelloul
Date : 2006-05-09
Résumé Télécharger
RR-2006-07
Extension of First-Order Theories into Trees
Khalil Djelloul, Thi-Bich-Hanh Dao
Date : 2006-06-20
Résumé Télécharger
RR-2006-08
Minimal interval completion through graph exploration
Karol Suchan, Ioan Todinca
Date : 2006-07-11
Résumé Télécharger
RR-2006-09
Characterizing minimal interval completions: Towards better understanding of profile and pathwidth
Pinar Heggernes, Karol Suchan, Ioan Todinca, Yngve Villanger
Date : 2006-07-11
Résumé Télécharger
RR-2006-10
Pathwidth of circular-arc graphs
Karol Suchan, Ioan Todinca
Date : 2006-07-11
Résumé Télécharger
RR-2006-11
Problem Modeling and Solving in QCSP made Practical
Marco Benedetti, Arnaud Lallouet, Jérémie Vautard
Date : 2006-07-18
Résumé Télécharger
RR-2006-12
La visualisation distante
S. Limet, S. Madougou, E. Melin, S. Robert
Date : 2006-12-20
Résumé Télécharger
RR-2006-13
Synchronized-ContextFree Tree-tuple Languages
Jacques Chabin, Jing Chen, Pierre Réty
Date : 2006-09-20
Résumé Télécharger
RR-2006-14
Visibly Pushdown Languages and Term Rewriting
Jacques Chabin, Pierre Réty
Date : 2006-12-22
Résumé Télécharger
Résumés des rapports de recherche
RR-2006-01 Abstract Branching for Quantified Formulas
Marco Benedetti
Résumé :
Mot(s) Clé(s) :
RR-2006-02 Minimal proper interval completions
Ivan Rapaport, Karol Suchan, Ioan Todinca
Résumé : Nous étudions le problème d'ajout d'arêtes à un graphe quelconque pour que le graphe obtenu soit un graphe d'intervalles propres. Notre objectif est d'ajouter un ensemble minimal d'arêtes. Ce qui signifie qu'aucun sous-ensemble propre des arêtes supplémentaires ajoutées au graphe de départ ne peut donner un graphe d'intervalles propres. Ce problème est proche du problème d'ajout d'un ensemble minimal d'arêtes à un graphe pour obtenir un graphe triangulé ou un graphe d'intervalles. Cependant, tandis qu'il existe des algorithmes pour obtenir un graphe triangulé ou un graphe d'intervalles de cette façon, le problème analogue d'obtention d'un graphe d'intervalles propres était ouvert jusqu'à présent. Dans ce papier, nous donnons un algorithme en temps linéaire pour obtenir une complétion d'intervalles propres minimale d'un graphe quelconque, ainsi nous résolvons la complexité de ce problème.
Mot(s) Clé(s) : graphe, triangulation, intervalle, propre, complétion, exploration, complexité, algorithme, polynômial, linéaire.
RR-2006-03 Automata for Analyzing and Querying Compressed Documents
Siva Anantharaman, Barbara Fila
Résumé : In a first part of this work, tree/dag automata are defined as extensions of (unranked) tree automata which can run indifferently on trees or dags; they can thus serve as tools for analyzing or querying any semi-structured document, whether or not given in a compressed format. In a second part of the work, we present a method for evaluating positive queries expressed in terms of Core XPath axes, on any XML document t, compressed or not. To each Core XPath location step of a certain basic type, we associate an automaton; these automata run on the hedges of the minimal straightline regular tree grammar associated to the document, or on its dependency dag. Any given Core XPath query can be decomposed into queries of the basic type; and the answers to the query can then be expressed as a sub-document of t, suitably labeled under the runs of such automata.
Mot(s) Clé(s) : Tree automata, Tree grammars, Dags, XML, Core XPath.
RR-2006-04 Deciding Satisfiability of positive Second Order Joinability Formulae
Sébastien Limet, Pierre Pillot
Résumé : Ce rapport traite d'une classe de formules du second ordre où le seul prédicat est la joignabilité modulo un système de réécriture conditionnel, les variables du premier ordre étant des termes clos et les variables du second ordre sont interprétées comme des relations sur les termes clos (c.à.d des ensembles de n-uplet de termes clos). On définit un algorithme générique qui décide de la satisfiabilité des formules positives de joignabilités du second ordre quand un algorithme est connu concernant la représentation finie des solutions des formules du premier ordre correspondant. Le résultat est alors un programme logique qui représente les instances des variables du second ordre. On applique cette technique a la classe des formules positives pseudo-régulière du second ordre. On définit également une transformation qui traduit cette instance sous forme de système de réécriture conditionnel. Notre technique peut être utilisée pour synthétiser automatiquement un programme qui définit une relation par sa spécification.
Mot(s) Clé(s) : programmation logique; système de réécriture; langage d'arbres; second ordre.
RR-2006-05 Solving First-Order Constraints in the Theory of the Evaluated Trees
Thi-Bich-Hanh Dao, Khalil Djelloul
Résumé : Nous présentons dans ce papier un algorithme général de résolution de contraintes du premier ordre dans la théorie T des arbres évalués. Cette théorie est une combinaison de la théorie des arbres finis ou infinis et de la théorie des rationnels munis de l'addition, de la soustraction et d'une relation d'ordre dense sans extrême. L'algorithme est donné sous forme d'un ensemble de 28 règles de réécriture et transforme toute formule du premier ordre P, qui peut éventuellement contenir des variables libres, en une disjonction Q de formules résolues, équivalente à P dans T, sans nouvelles variables libres, et telle que Q est soit la formule Vrai, soit la formule Faux, soit une formule ayant au moins une variable libre et n'étant équivalente ni à Vrai ni à Faux dans T. En particulier, si P est sans variables libres, Q est soit la formule Vrai soit la formule Faux. Si Q contient des variables libres, les solutions sur ces variables sont exprimées d'une façon explicite et Q peut se transformer directement en une combinaison booléenne de conjonctions quantifiées de formules atomiques, qui n'acceptent pas d'élimination de quantificateurs. La correction de notre algorithme est une autre preuve de la complétude de la théorie T.
Mot(s) Clé(s) : contraintes du premier ordre; théorie des arbres; théorie des rationnels additifs ordonnés; résolution de contraintes; règles de réécriture.
RR-2006-07 Extension of First-Order Theories into Trees
Khalil Djelloul, Thi-Bich-Hanh Dao
Résumé : We present in this paper an automatic way to combine any first-order theory T with the theory of finite or infinite trees. First of all, we present a new class of theories that we call zero-infinite-decomposable and show that every decomposable theory T accepts a decision procedure in the form of six rewriting which for every first order proposition give either true or false in T. We present then the axiomatization T* of the extension of T into trees and show that if T is flexible then its extension into trees T* is zero-infinite-decomposable and thus complete. The flexible theories are theories having elegant properties which enable us to eliminate quantifiers in particular cases.
Mot(s) Clé(s) : first-order theories, theory of finite or infinite trees. complete theories.
RR-2006-08 Minimal interval completion through graph exploration
Karol Suchan, Ioan Todinca
Résumé : Etant donne un graphe quelconque $G=(V,E)$, un graphe d?intervalles $H=(V,E)$ est appelé complétion d?intervalles de $G$ si $E \subseteq F$. Le graphe $H$ est appelé complétion d?intervalles minimales si, pour tout graphe sandwich $H? = (V, F?)$ avec $E \subseteq F? \subset F$, $H?$ n?est pas un graphe d?intervalles. Nous présentons dans cet article un algorithme de complexité $\mathcal{O}(nm)$ calculant une complétion d?intervalles minimale d?un graphe quelconque.
Mot(s) Clé(s) : graphe, triangulation, intervalle, propre, complétion, exploration, complexité, algorithme, polynômial, linéaire.
RR-2006-09 Characterizing minimal interval completions: Towards better understanding of profile and pathwidth
Pinar Heggernes, Karol Suchan, Ioan Todinca, Yngve Villanger
Résumé : Les complétions d?intervalles minimales sont au coeur de la compréhension de deux paramètres de graphes très étudiés : la largeur arborescente linéaire (pathwidth) et le profile. L?étude des complétions minimales semble nécessaire pour avancer sur le calcul des deux paramètres. Une complétion d?intervalles d?un graphe est $G$ est un graphe d?intervalles $H$, ayant le même ensemble de sommets que $G$, obtenu en rajoutant des arêtes au graphe $G$. Si, de plus, on ne peut pas enlever une partie des arêtes rajoutées sans détruire la propriété de graphe d?intervalles, nous dirons que $H$ est une complétion d?intervalles minimales. Dans cet article, nous donnons pour la première fois une caractérisation des complétions d?intervalles minimales. Nous présentons également un algorithme polynomial qui extrait, à partir d?une complétion d?intervalles quelconque, une complétion d?intervalles minimale du graphe de départ.
Mot(s) Clé(s) : graphe, triangulation, intervalle, propre, complétion, exploration, complexité, algorithme, polynômial, linéaire.
RR-2006-10 Pathwidth of circular-arc graphs
Karol Suchan, Ioan Todinca
Résumé : La largeur arborescente linéaire (pathwidth) d?un graphe $G$ est définie comme le nombre de clique minimum de $H$ moins un, parmi tous les graphes d?intervalles $H$ contenant $G$. Bien que la largeur arborescente linéaire soit un paramètre bien connu et très étudié, il existe très peu de classes de graphes pour lesquelles on dispose d?algorithmes polynomiaux calculant le paramètre. Nous présentons dans cet article un algorithme de complexité $\mathcal{O}(n2)$, calculant la largeur arborescente linéaire des graphes d?intervalles circulaires.
Mot(s) Clé(s) : graphe, pathwidth, circular-arc, triangulation, intervalle, complétion, complexité, algorithme, polynômial.
RR-2006-11 Problem Modeling and Solving in QCSP made Practical
Marco Benedetti, Arnaud Lallouet, Jérémie Vautard
Résumé :
Mot(s) Clé(s) :
RR-2006-12 La visualisation distante
S. Limet, S. Madougou, E. Melin, S. Robert
Résumé : La visualisation de données est de plus en plus exploitée dans de nombreux domaines scientifiques et devient un élément essentiel dans la compréhension de phénomènes étudiés dans les différentes disciplines scientifiques. De plus, face aux enjeux de la complexité des simulations sous-jacentes et de la taille des données générées, le développement des applications scientifiques se base désormais sur des systèmes parallèles et distribués. Ainsi, il devient classique d'envisager un déploiement d'une application sur plusieurs sites dont un qui réalise l'affichage des résultats. Cet état de l'art s'intéresse à ce dernier point et a été réalisé dans le cadre d'un contrat de recherche avec le CEA/DIF de Bruyères-le-Châtel. Nous nous sommes ainsi intéressés à différentes solutions de visualisation distante afin d'obtenir une classification permettant de juger de leur qualité en fonction des attentes des utilisateurs. Nous avons choisi d'aborder cette classification en fonction du lieu du rendu qui influe sur les performances en terme de taux de rafraîchissement de l'image par rapport à la qualité du réseau. Ce point de vue permet de traiter les différentes méthodes possibles pour répartir le pipeline graphique entre les deux sites impliqués et d'en voir les avantages et les inconvénients. La visualisation distante s'appuie également sur une infrastructure réseau dont dépendent les performances finales. Ces différentes infrastructures possibles seront décrites dans une deuxième partie, ainsi que les concepts plus généraux formalisant les aspects réseau pour des déploiements de type Grid. Enfin, il existe déjà aujourd'hui des systèmes que nous qualifions d'autonomes dédiés directement ou indirectement à la visualisation distante. Ils constituent la dernière partie de ce document et nous permettront de conclure sur la pérennité des systèmes existants et les différentes possibilités pour les systèmes à venir.
Mot(s) Clé(s) :
RR-2006-13 Synchronized-ContextFree Tree-tuple Languages
Jacques Chabin, Jing Chen, Pierre Réty
Résumé : Using logic programs, we define a new class of tree-(tuple) languages, that combines the synchronized-regular tree-(tuple) languages with the context-free tree languages. Thus, this class can express an unbounded counting both in several independent branches (like in a synchronized-regular language), and at two nested positions (like in a context-free language). Despite its bigger expressivity, the new class has the same useful properties as the former ones\,: closure under union, closure under intersection of one tuple-component with a regular tree language, decidability of membership and emptiness. Therefore, it should give rise to many applications.
Mot(s) Clé(s) : tree languages, logic programming, rewriting
RR-2006-14 Visibly Pushdown Languages and Term Rewriting
Jacques Chabin, Pierre Réty
Résumé : To combine tree languages with term rewriting, we introduce a new class of tree languages, that both extends regular languages and restricts context-free languages, and that is closed under intersection (unlike context-free languages). To do it, we combine the concept of visibly pushdown language, with top-down pushdown tree automata, and we get the visibly pushdown tree automata. Then, we use them to express the sets of descendants for a sub-class of growing term rewrite systems, and thanks to closure under intersection, we get that joinability and (restricted) unifiability are decidable.
Mot(s) Clé(s) : tree languages, term rewriting.
Université d'Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 