Academic literature on the topic 'Réécriture, Systèmes de (informatique)'

La recherche d’information subit depuis quelques années une mutation significative liée aux technologies Web et aux dispositifs électroniques personnels qui ont permis à toute personne d’être connectée à la toile à tout moment et depuis pratiquement n’importe quel endroit. Les applications de recherche d’information actuelles se doivent d’adapter son fonctionnement selon l’utilisateur et son contexte, puisque chacun a ses propres besoins, intérêts, contraintes, et préférences. Plusieurs techniques d’adaptation ont vu le jour, en particulier la réécriture de requête permettant de modifier certains prédicats initiaux afin de mieux répondre aux attentes de l’utilisateur. Cependant, la plupart de ces techniques ne sont pas appropriées à la recherche d’information multimédia, de plus en plus produite, partagée, et recherchée par les utilisateurs. Cela est principalement lié: 1-) à la complexité de la description et de la représentation du contenu multimédia pouvant être décrit par des propriétés sémantiques, physiques (couleurs, formes, textures, etc. ), spatiales et temporelles, etc. 2)- à l’ambigüité causée par le pouvoir d’expression des langages d’interrogation proposés pour la recherche d’information multimédia, et 3)- à la prise partielle des préférences de chaque utilisateur. Nous proposons, dans cette thèse, une approche de réécriture de requêtes multimédia qui permet à la fois de considérer la spécificité de chaque propriété multimédia impliquée dans la requête et le profil de l’utilisateur. S’articulant autour du concept de voisinage que nous définissons ici, notre approche comporte trois phases : la pré-réécriture qui permet de définir des voisinages pondérés des valeurs à réécrire, la réécriture brute dans laquelle nous définissons une fonction de relaxation de valeurs et nous intégrons les contraintes de l’utilisateur en appliquant une fonction de contrôle, et la post-réécriture qui a pour mission d’adapter le résultat et le rendre plus pertinent selon les besoins de l’utilisateur. Plusieurs prototypes ont été implémentés ainsi qu’une panoplie de tests expérimentaux ayant été menés dans le but de valider notre proposition.

On aborde dans cette thèse certaines propriétés formelles de systèmes de réécriture qui concernent leurs espaces des dérivations. Les calculs choisis présentent des caractéristiques particulières qui font l'étude des propriétés choisies des défis intéressants. Les contributions les plus importantes de ce travail sont: (1) nous définons une stratégie de réduction multiradicaux pour le Pure Pattern Calculus, un calcul d'ordre supérieur non-séquentiel, et nous prouvons que cette stratégie est normalisante; (2) nous proposons une manière de formaliser le concept de réduction standard pour I Linear Substitution Calculus, un calcul avec substitutions explicites agissent à la distance dont les réductions sont considérés modulo une rélation d'équivalence dans l'ensemble des termes, et nous aboutissons à des résultats d'existence et unicité des reductions standards pour cette formalisation; et (3)nous donnons une charactérisation de l'équivalence entre réductions pour les systèmes de réécriture des termes infinitaires de premier ordre linéares à gauche, et nous nous servons de cette charactérisation pour développer une preuve d'une version renforcée du résultat de compression des réductions infinitaires. Un trait commun a ces trois sujets est l'utilisation de formalismes génériques de systèmes de réécriture. L'étude sur le Pure Pattern Calculus et celui concernant le Linear Substitution Calculus reposent sur le concept de Système Abstrait de Réécriture De son côté, pour le travail sur la réécriture infinitaire, on se sert d'un modèle fondé sur la notion de proof term. Des extensions à ces formalismes génériques sont des contributions additionnelles de cette thèse<br>We study different aspects related to the reduction spaces of diverse rewriting systems. These systems include features which make the study of their reduction spaces a far from trivial task. The main contributions of this thesis are: (1)we define a multistep reduction strategy for the Pure Pattern Calculus, a non-sequential higher-order term rewriting system, and we prove that the defined strategy is normalising;(2)we propose a formalisation of the concept of standard reduction for the Linear Substitution Calculus, a calculus of explicit substitutions whose reductions are considered modulo an equivaience relation defined on the set of terms, and we obtain a result of uniqueness of standard reductions for this formalisation; and finally, (3) we characterise the equivalence of reductions for the infinitary, first-order, left-linear term rewriting systems, and we use this characterisation to develop an alternative proof of the compression result. We remark that we use generic models of rewriting systems: a version of the notion of Abstract Rewriting Systems is used for the study of the Pure Pattern Calculus and the Linear Substitution Calculus, while a model based on the concept of proof terms is used for the study of infinitary rewriting. We include extensions of both used generic models; these extensions can be considered as additional contributions of this thesis

Les systemes constructeurs fortement sequentiels admettent une strategie tres efficace pour une suite de reductions. Thatte a decouvert une transformation syntaxique qui permet de simuler tout systeme orthogonal par un systeme constructeur: toute forme normale dans ce nouveau systeme est egalement une forme normale dans le systeme initial. Malheureusement, cette transformation ne conserve pas la forte sequentialite, interdisant l'usage de la strategie efficace pour les systemes fortement sequentiels constructeurs. Dans cette these, nous definissons la classe des systemes equivalents constructeurs pour laquelle la forte sequentialite est conservee ; nous donnons quelques proprietes de cette classe ainsi qu'une caracterisation algebrique. Nous montrons egalement qu'il s'agit d'une sous-classe de la classe des systemes forward-branching definie par strandh qui est elle-meme incluse dans la classe des systemes fortement sequentiels. Ensuite, nous exposons une transformation de notre conception basee sur la notion d'arbre d'index. Cette transformation permet de simuler tout systeme forward-branching par un systeme fortement sequentiel constructeur. Dans le pire des cas, la taille de ce nouveau systeme est quadratique par rapport a la taille du systeme d'origine. Nous ameliorons alors notre transformation afin que la taille du systeme issu de la transformation soit lineaire par rapport a la taille du systeme d'entree

Cette thèse s'inscrit dans le cadre général de la preuve de terminaison de systèmes de réécriture, avec un accent particulier sur le problème de la complexité. La terminaison est une propriété indécidable de la théorie de la réécriture. Il existe toutefois un résultat de combinatoire qui fournit un critère suffisant : le théorème de Kruskal. Ce théorème a conduit à la définition d'ordres de terminaison largement utilisés en démonstration automatique. Nous donnons une analyse de la complexité pour ces ordres de terminaison dans le cas des termes ou des mots et nous envisageons quelles en sont les limites. L'approche que nous avons retenue pour cette étude repose sur la théorie des hiérarchies de fonctions indexées par les ordinaux. Un second volet de la thèse est consacré à une extension des hiérarchies de fonctions, avec la définition d'un système alternatif de termes ordinaux. Les opérateurs fonctionnels sont introduits de manière purement syntaxique. La construction des ordinaux limites est gérée par un opérateur unaire, qui permet d'intégrer les suites fondamentales à la notation. Par rapport aux ordinaux de la théorie des ensembles, ce système est à la fois plus souple dans le maniement des opérateurs fonctionnels et plus précis dans l'analyse de la récursion. Établir la terminaison d'un système de réécriture revient alors à résoudre une équation ordinale générée directement à partir des règles du système. Cela s'apparente à la résolution d'une équation récurrente sur les entiers. La preuve de terminaison fournit en outre une mesure gratuite pour la complexité. Plusieurs exemples illustrent cette approche<br>The thesis is about termination in rewriting theory, with particular emphasis on complexity. Termination is an undecidable property of term rewriting systems. However, there exists a combinatorial result that provides a syntactic sufficient condition for termination: Kruskal's tree theorem. This theorem has given rise to several widely used termination orderings in automated reasoning. We study the complexity of those orderings in the case of string and term rewriting systems and give new upper bounds. This work relies on the theory of number-theoretic hierarchies of functions indexed by ordinals. A second part of the thesis is devoted to a modified approach to number-theoretic hierarchies of functions by means of a syntactic approach to ordinal recursion. Our framework of ordinal terms is defined by a set of function symbols whose semantics are given by a rewrite system. Terms are equipped with a binary operator that builds up limit terms from a fundamental sequence. Compared to set-theoretical ordinals, the calculus we obtain is more flexible and involves a more precise analysis of the recursion principle. It appears to be appropriate for finding semantic termination proofs in a systematic way through the reduction to the problem of solving ordinal term inequations. The proof then gives a complexity measure for free. Various examples of applications illustrate this method

La réécriture concurrente est étudiée pour ses aspects théoriques et sa capacité d'expression, puis un modèle d'implantation sur machine parallèle à mémoire distribuée est propose. Des stratégies concurrentes permettent de caractériser des dérivations aux propriétés intéressantes, le résultat principal étant l'optimalité de stratégie maximale. Une méthode effective est proposée pour combiner les spécifications équationnelles (sans idée de changement, par exemple des types abstraits) et non équationnelles (en général indéterministes et irréversibles, par exemple des transitions d'un système). Elle est ensuite appliquée à l'exemple de CCS, avec en corollaire un cadre unifié pour décrire processus et types abstraits. Le modèle d'implantation proposé est basé sur un algorithme de filtrage de bas en haut. Sa réalisation sur une machine à mémoire distribuée, donc sans état global, est décrite en exprimant les opérations de base par des échanges de messages. La réécriture concurrente semble donc un modèle de programmation intéressant pour de telles machines

Une figure 2D constituée de segments unitaires horizontaux et verticaux peut être représentée par une séquence de symboles, chacun d'entre eux engendrant un déplacement unitaire dans l'une des quatre directions: droite, gauche, haut ou bas. L'ensemble de ces symboles est noté P. Ainsi, à tout mot de P* est associée une unique figure inscrite dans le plan cartésien. Nous étudions différents systèmes de réécriture définis sur P* et conservant certaines propriétés des figures associées. D'abord, l'alphabet P contient quatre lettres engendrant des déplacements visibles (crayon baissé). Nous étudions deux systèmes de réécriture S et Sr-red conservant les figures: l'un d'entre eux permet d'obtenir tous les mots décrivant la même figure, l'autre est un système confluent fournissant un unique mot irréductible. Puis, nous complétons cet alphabet avec quatre lettres «blanches» engendrant des déplacements invisibles (crayon levé). Nous définissons un nouveau système de réécriture S' permettant d'obtenir exactement tous les mots décrivant la même figure qu'un mot initial. Pour chacun de ces deux alphabets, nous recherchons un parcours minimal décrivant une figure connexe donnée. Enfin, nous terminons par des résultats de décidabilité relatifs aux langages de mots de figure. Etant donné un langage rationnel inclus dans P*, nous pouvons décider si celui-ci contient des mots de contour de polyominos particuliers. Ces résultats sont établis à l'aide de deux systèmes de réécriture laissant invariantes certaines propriétés des mots de figure

L'objet de cette thèse est l'étude d'un calcul permettant de décrire l'application de règles de réécriture conditionnelles et de représenter les résultats obtenus. Nous introduisons le calcul de réécriture, appelé aussi le rho-calcul, qui généralise la réécriture du premier ordre et le lambda-calcul tout en permettant d'exprimer le non-déterminisme. Dans notre approche, l'opérateur d'abstraction ainsi que l'opérateur d'application sont des objets du calcul. Le résultat d'une réduction dans le calcul de réécriture est soit un ensemble vide représentant l'échec de l'application, soit un singleton représentant un résultat déterministe, soit un ensemble ayant plusieurs éléments représentant un choix non-déterministe de résultats. Au cours de cette thèse nous nous concentrons sur les propriétés du calcul de réécriture utilisant un filtrage syntaxique pour lier les variables à leurs valeurs actuelles. Nous définissons des stratégies d'évaluation garantissant la confluence du calcul et nous montrons que ces stratégies deviennent triviales pour des restrictions du calcul de réécriture général à des calculs plus simples comme le lambda-calcul. Le calcul de réécriture n'est pas terminant dans le cas non-typé mais la terminaison forte est obtenue pour le calcul simplement typé. Dans le calcul de réécriture étendu par un opérateur permettant de tester l'échec de l'application nous définissons des termes représentant la normalisation innermost et outermost par rapport à un ensemble de règles de réécriture. En utilisant ces termes, nous obtenons un codage naturel et concis de la réécriture conditionnelle. Enfin, à partir de la représentation des règles de réécriture conditionnelles, nous montrons comment le calcul de réécriture peut être employé pour donner une sémantique au langage ELAN basé sur l'application de règles de réécriture contrôlées par des stratégies<br>This thesis is devoted to the study of a calculus that describes the application of conditional rewriting rules and the obtained results at the same level of representation. We introduce the rewriting calculus, also called the rho-calculus, which generalizes the first order term rewriting and lambda-calculus, and makes possible the representation of the non-determinism. In our approach the abstraction operator as weIl as the application operator are objects of calculus. The result of a reduction in the rewriting calculus is either an empty set representing the application failure, or a singleton representing a deterministic result, or a set having several elements representing a not-deterministic choice of results. In this thesis we concentrate on the properties of the rewriting calculus where a syntactic matching is used in order to bind the variables to their current values. We define evaluation strategies ensuring the confluence of the calcalus and we show that these strategies become trivial for restrictions of the general rewriting calculus to simpler calculi like the lambda-calculus. The rewriting calculus is not terminating in the untyped case but the strong normalization is obtained for the simply typed calculus. In the rewriting calculus extended with an operator allowing to test the application failure we define terms representing innermost and outermost normalizations with respect to a set of rewriting rules. By using these terms, we obtain a natural and concise description of the conditional rewriting. Finally, starting from the representation of the conditional rewriting rules, we show how the rewriting calculus can be used to give a semantics to ELAN, a language based on the application of rewriting rules controlled by strategies

Les techniques de réécriture ont été développées depuis les années 1970 et appliquées en particulier au prototypage des spécifications formelles algébriques et à la démonstration de propriétés liées à la vérification de programmes. ELAN est un système qui permet de spécifier et d'exécuter des résolveurs de contraintes, des démonstrateurs et plus généralement tout processus décrit par des règles de transformation. Il possède des opérateurs associatifs-commutatifs (AC) et un langage de stratégies qui permettent une gestion fine de l'exploration d'un arbre de recherche et une manipulation aisée d'opérateurs mathématiques tels que les connecteurs booléens, les opérateurs arithmétiques ou les opérateurs de composition parallèle par exemple. Ces deux notions améliorent grandement l'expressivité du langage mais introduisent un double non-déterminisme lié à la possibilité d'appliquer plusieurs règles, de différentes façons, sur un terme donné. Cela rend difficile et généralement peu efficace leur implantation. L'objectif principal de cette thèse est d'étudier des techniques de compilation qui améliorent l'efficacité de ce type de langages. Nous proposons un nouvel algorithme, à base d'automates déterministes, pour compiler efficacement le filtrage syntaxique. Nous définissons ensuite différentes classes de règles pour lesquelles nous proposons un algorithme efficace de filtrage AC. Cet algorithme utilise une structure de données compacte et les automates définis précédemment, ce qui améliore considérablement les performances du processus de normalisation dans son ensemble. [. . . ]

Dans cette thèse nous formalisons des systèmes de règles de production dans le système ELAN basé sur la logique de réécriture où l'application des règles est contrôlée par des stratégies. Le calcul de réécriture fournit une sémantique opérationnelle à ELAN. Nous avons ainsi été amenés à étendre ELAN tout en respectant sa sémantique. Cette extension comporte tout d'abord la possibilité de définir des classes et des objets en ELAN. Ce langage s'implante en ELAN comme un langage objet à prototype. Nous avons également défini un formalisme de règles travaillant à la fois avec une base d'objets et avec une base de contraintes. Ces deux bases coopérent par l'intermédiaire de variables partagées. Ce nouveau paradigme de programmation avec règles, objets, contraintes et stratégies nous permet de modéliser des problèmes de planification ou d'ordonnancement<br>In this thesis, we design production rule systems in the ELAN system which is based on the rewriting logic and where strategies control the application of the rules. The rewriting calculus gives an operational semantics of ELAN. Thus, we developed an extension of ELAN that respects its semantics. Firstly, in this extension, we give the possibility to define classes and objects in ELAN. This language is implemented in ELAN as a prototype object-language. Then, we define a new formalism of rules working together with an object and a constraint store such that objects and constraints share variables. The application of the set of rules is controlled by strategies. This new programming paradigm with rules, objects, constraints and strategies is here used to model problems such that planification or scheduling

Cette thèse étudie les propriétés calculatoires des présentations d'opérades, ou systèmes de réécriture de diagrammes de Penrose, et leurs liens avec divers types de systèmes de réécriture classiques. Grâce à des nouveaux critères pour la terminaison et la confluence, on démontre la conjecture sur la convergence de la présentation L(Z2) des Z/2Z-espaces vectoriels, une théorie équationnelle commutative. On montre que les présentations d'opérades sont des généralisations des systèmes de réécriture de mots et des réseaux de Petri et qu'elles fournissent un calcul de gestion explicite des ressources pour les systèmes de réécriture de termes linéaires à gauche. Enfin, on étudie les obstructions à ce même résultat concernant le lambda-calcul. Des annexes présentent les liens entre les opérades et d'autres structures de l'algèbre universelle, ainsi qu'un calcul de substitutions explicites.