Le Faust de Goethe a provoqué une réelle onde de choc dans la vie culturelle des pays germaniques et des territoires francophones. Mais le drame allemand, et plus encore son personnage diabolique, n’ont pas fait l’objet d’une réception identique des deux côtés du Rhin, comme le révèle un examen détaillé du discours de la presse : tandis que les artistes et hommes de lettres germaniques rapportent le personnage aux incarnations infernales de la légende populaire faustienne, leurs homologues français y voient une réactualisation originale la figure mythique de Satan, dans la lignée des œuvres de Byron ou Milton. Après un état de la recherche portant sur le Méphistophélès de Goethe, nous avons dessiné l’évolution de son interprétation par la presse et de sa réutilisation par les artistes au-travers de l’analyse d’articles de presse, d’œuvres visuelles (Seibertz, Ramberg, Retzsch, Johannot), dramatiques (Holtei, B. v. Braunthal, Lesguillon) ou opératiques (Gounod). Enfin, l’analyse intermédiale comparée et détaillée des personnages diaboliques du Faust de Lenau, de la série lithographique de Delacroix et de La Damnation de Faust de Berlioz permet de reconstituer l’évolution des mythes de Faust et du diable au cours de la période étudiée, et de constater que, lorsque le diable s’humanise, l’homme se diabolise. Une réflexion sur le bienfondé des termes de « réécriture » et d’ « illustration », auxquels l’auteur préfère, selon l’opportunité, celui de « reformulation », clôt ce travail au carrefour des théories de la réception, de la mythocritique et de l’intermédialité / Goethe’s Faust had a significant impact on German and French cultural life in the nineteenth century. But the German drama, and even more his devilish character, were not perceived similarly on right hand side and the left hand side of the Rhine. Whereas the German artists and the literary critics associated Goethe’s Mephistopheles with the devilish character of the popular Faust’s legend, the French counterparts take Mephistopheles as the mythical character of Satan and a revision of the heroes of Byron and Milton. After a description of the state of the art about Goethe’s Mephistopheles, a depiction of the evolution of his interpretation in the press and of his re-utilisation by the artists through an analysis of articles and visual (Seibertz, Ramberg, Retzsch, Johannot), dramatic (Holtei, B. v. Braunthal, Lesguillon) and musical works (Gounod). Last but not least, the detailed intermedial comparative analysis of the devilish heroes of Lenau’s Faust, of Delacroix’s lithographs and of Berlioz’ The Damnation of Faust enable us to recreate the evolution of the myths of Faust and of the devil within the considered period. So we could point out that when devil is getting human features, man becomes a devil. Finally, a consideration about the french terms of “réécriture” and “illustration”, that the author propose, in some case, to replace with “reformulation”, conclude this work that crosses reception theory, mythocriticism and intermediality.

L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés.

L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés / The objective of this thesis is to explore formal descriptions for the structure and functioning of biological systems, as well as formal tools for reasoning about their behavior. This work takes place in the overall prospective to study safe computational models where computations are expressed via rewriting, and where we can rely on formal verification to express and validate suitable properties. In this thesis we develop a higher-order calculus rewriting for describing molecules, reaction patterns, and biochemical network generation. The calculus is based on the chemical metaphor by describing the computations in terms of chemical solutions in which molecules representing data freely interact according to reaction rules. This way we obtained an Abstract Biochemical Calculus as an extension of the higher-order chemical model by considering structured molecules. The calculus is provided with a natural specification of concurrency and of controlling mechanisms by expressing rewrite strategies as molecules. The description of molecular complexes or chemical reactants belong to specific classes of graphs. We define the structure of port graphs and we show how the principles of the biochemical calculus instantiated for port graphs are expressive enough for modeling autonomous systems and biochemical networks. In addition, strategic rewriting techniques open the way to reason about the computations and to verify properties of the modeled systems

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Si Paul Nougé (1895-1967), cabeza pensante del grupo surrealista de Bruselas, es poco conocido, al contrario que su amigo y cómplice René Magritte, es también porque él hizo todo lo posible para permanecer en la sombra. Habiendo publicado muy poco por propia iniciativa, además adoptó la actitud de escribir a través de las palabras de otros. La dimensión que toma la reescritura en sus intervenciones poéticas no es extraño que sorprenda. Es el caso cuando reescribe uno u otro texto de un autor determinado (las octavillas de Correspondance, Le Dessous des cartes, Le Jeu des mots et du hasard, J. Vaché, Quelques écrits de Clarisse Juranville, La Parole est à Baudelaire, Un miroir exemplaire de Maupassant, por no citar sino los que hemos estudiado). El análisis genético de las "tentativas" nougeanas apenas había sido desarrollado hasta ahora (con excepción de las octavillas de Correspondance y de Un portrait d'après nature), ni siquiera en el caso de los hipotextos conocidos. La comparación del texto de Nougé y de su hipotexto es reveladora, tanto de los procedimientos utilizados como de la orientación ética y antiliteraria que le confiere la reescritura, que se puede calificar con razón de détournement (desviación). Por otra parte, en Nougé se encuentra una serie de textos breves, de falsos anuncios, aforismos y locuciones incluidas en poemas en los que resuena un eco polifónico. Una evocación a veces vaga, a veces precisa, se insinúa en la memoria del lector, le hace detenerse para identificar esa reminiscencia. Nougé retoma las palabras de otros, las palabras de todo el mundo o "lugares-comunes", para asignarles otro destino y alcanzar al lector en lo más profundo de su lengua y de su cultura, en el núcleo de su identidad. Sometemos al análisis un corpus de textos para dar cuenta de los procedimientos utilizados. Decir procedimientos es decir medios y, en este caso, medios de acción utilizados en función de un "fin superior". Es conocido el compromiso comunista de Nougé; no obstante, puesto que sus textos no son en absoluto militantes ni propagandistas y aún menos realistas socialistas, nunca se había cuestionado la relación entre sus prácticas de escritura (y más concretamente de reescritura) y sus convicciones políticas. Esta es, sin embargo, la hipótesis que nos hemos planteado: la reescritura en Nougé tendría una justificación y unos fines revolucionarios. Del marxismo, Nougé obtiene un método, el método dialéctico, y lo combina con el método experimental que practicó a lo largo de su vida de científico para aplicarlo con rigor a sus experiencias de escritura. Todo su trabajo de escritor se orienta a provocar un efecto bouleversant (desestabilizador) en el lector de manera que lo impulse a inventar su vida transformando el mundo. La táctica de Nougé es sutil e insidiosa, pues al obrar sobre el inconsciente del lector por la vía de la desviación de diferentes lugares comunes, remite paradójicamente a una voluntad deliberada, reclama cada vez más conciencia. En esta perspectiva, la reescritura se le presenta como el medio de acción más eficaz, y es la razón ética por la cual se aferra a ella callando su propia voz y evitando abandonarse a sus inclinaciones literarias, a pesar de todo muy reales. Estudiamos en esta tesis cómo se cruzan, se completan y se resuelven los tres grandes ejes que marcaron la trayectoria de Paul Nougé: el compromiso político, la ciencia y la poesía, los tres dominados por una poderosa ética revolucionaria que le hizo tomar el partido de la reescritura y de la escritura fragmentaria, de la discreción e incluso del anonimato. / Si Paul Nougé (1895-1967), chef de file du groupe surréaliste de Bruxelles, est peu connu, contrairement à son ami et complice René Magritte, c'est aussi qu'il a tout fait pour rester dans l'ombre. Ayant très peu publié de sa propre initiative, il a pris en outre le parti d'écrire à travers les mots des autres. L'ampleur que prend la réécriture dans ses interventions poétiques a de quoi surprendre. C'est le cas des écrits où il détourne l'un ou l'autre texte d'un auteur déterminé (les tracts de Correspondance, Le Dessous des cartes, Le Jeu des mots et du hasard, J. Vaché, Quelques écrits de Clarisse Juranville, La Parole est à Baudelaire, Un miroir exemplaire de Maupassant, pour ne citer que ceux que nous avons étudiés). L'analyse génétique des « entreprises » nougéennes n'avait guère été développée jusqu'ici (à l'exception des tracts de Correspondance et d'Un portrait d'après nature), même dans le cas où les hypotextes étaient bien connus. La mise en regard du texte de Nougé et de son hypotexte est révélatrice, tant des procédés mis en αuvre que de l'orientation éthique et antilittéraire conférée par la réécriture, que l'on peut à juste titre qualifier de détournement. Par ailleurs, on trouve chez Nougé une série de textes brefs, fausses réclames, aphorismes, et autres locutions incluses dans des poèmes où résonne un écho polyphonique. Une ressemblance, parfois vague, parfois précise, titille la mémoire du lecteur, le pousse à s'arrêter, à identifier cette réminiscence. Nougé reprend en effet les mots des autres, les mots de tout le monde ou « lieux-communs », pour leur assigner une autre destination et toucher le lecteur au plus profond de sa langue et de sa culture, au cαur de son identité. Nous soumettons un corpus constitué d'une sélection de ces textes à une analyse visant à répertorier les procédés utilisés. Qui dit procédés dit moyens, et, dans ce cas, moyens d'action mis en αuvre en fonction d'une « fin supérieure ». L'engagement communiste de Nougé est connu, mais ses textes n'étant nullement militants ni propagandistes et encore moins réalistes socialistes, la question ne s'est jamais posée du lien entre ses pratiques d'écriture (et plus particulièrement de réécriture) et ses convictions politiques. C'est néanmoins l'hypothèse que nous avons posée : la réécriture chez Nougé aurait une justification et une fin révolutionnaires. Du marxisme, Nougé tire une méthode, la méthode dialectique, et la combine à la méthode expérimentale qu'il a pratiquée tout au long de sa vie de scientifique pour l'appliquer rigoureusement à ses expériences d'écriture. Tout son travail d'écrivain vise à provoquer un effet bouleversant chez le lecteur de manière à pousser celui-ci à inventer sa vie tout en transformant le monde. La tactique de Nougé est subtile et insidieuse, car, agissant sur l'inconscient du lecteur par le biais du détournement de divers lieux communs, elle se réclame paradoxalement de la volonté délibérée, elle fait appel à toujours plus de conscience. Dans cette optique, la réécriture lui apparaît comme le moyen d'action le plus efficace, et c'est la raison éthique pour laquelle il s'y est indéfectiblement tenu, faisant souvent taire sa propre voix et évitant de s'abandonner à ses penchants littéraires, pourtant bien réels. Nous examinons dans cette thèse comment se croisent, se complètent et se résolvent les trois grands axes qui ont marqué le cheminement de Paul Nougé : l'engagement politique, la science et la poésie, tous trois dominés par une puissante éthique révolutionnaire qui lui a fait adopter le parti de la réécriture et de l'écriture fragmentaire, de la discrétion et même de l'anonymat. / If Paul Nougé (1895-1967), leader of the Brussels surrealist group, is little known, unlike his friend and associate René Magritte, it is also because he has done everything possible to keep out of the limelight. He published very little on his own initiative and chose to write through other people's words. The scope of the rewriting in his poetic interventions is surprising. Such is the case of the pieces where he reroutes some text or other by a particular author (the pamphlets Correspondance, Le Dessous des cartes, Le Jeu des mots et du hasard, J. Vaché, Quelques écrits de Clarisse Juranville, La Parole est à Baudelaire or Un miroir exemplaire de Maupassant, to mention only the ones we have studied). There had scarcely been any genetic analysis of Nougé's "ventures" until now (except for the pamphlets Correspondance and Un portrait d'après nature), even in the cases where the hypotexts were well known. Examining Nougé's texts and the hypotext is revealing, of both the procedures used and the ethical, anti-literary orientation provided by the rewriting, which we might reasonably call "détournement" (rerouting). Moreover, in Nougé we find a series of short texts, fake advertisements, aphorisms, and other locutions included in the poems where a polyphonic echo resounds. A sometimes vague, sometimes precise, resemblance titillates the reader's memory, impels him to stop, to identify that reminiscence. Nougé takes up other people's words, everyone's words or "commonplaces", assigns them another destination and touches the reader in the deepest places of his language and culture, at the heart of his identity. We submit a corpus made up of a selection of these texts to an analysis whose purpose is to make an inventory of the procedures used. Procedures is another way of saying means and, in this case, means of action activated according to a "higher end". Nougé's commitment to communism is well known, but since his texts are not at all militant or propagandistic and still less socialist realist, no-one ever wonders about the link between his writing practices (and particularly his rewriting practices) and his political convictions. This, nevertheless, is the hypothesis we have put forward: Nougé's rewriting has a revolutionary justification and purpose. From marxism, Nougé takes a method, the dialectical method, and combines it with the experimental method he has used all his life as a scientist to apply it rigorously to his writing experiments. The aim of all his work as a writer is to have an overwhelming effect on the reader so as to compel him to invent his life while transforming the world. His tactic is subtle and insidious since, acting on the reader's unconscious through the rerouting of different commonplaces, it paradoxically demands a deliberate will, calls for even more awareness. From this point of view, he sees rewriting as the most effective form of action, and that is the ethical reason for which he has unfailingly turned to it, often silencing his own voice and refusing to succumb to his literary preferences, which are nonetheless very real. In this thesis we examine the way in which the three great lines that have marked Nougé's path intertwine, complement and resolve one another: political commitment, science and poetry, all three dominated by a powerful revolutionary ethic which has led him to opt for rewriting and fragmentary writing, discretion and even anonymity.

Cette recherche propose de rendre compte de l'invention des Appalaches en tant que région « étrange et particulière ». Les écrivains « couleur locale » du dix-neuvième siècle ont contribué à ancrer dans la conscience nationale l'image oxymorique de l'Appalachien à la fois bon sauvage, mais surtout hillbilly dégénéré. A partir de l'entre-deux-guerres, puis à la fin des années 60 lors de la « Renaissance Appalachienne », des écrivains autochtones, parmi lesquels Mary Lee Settle, Lee Smith, Denise Giardina, se sont dressés pour réfuter cette identité prescrite. Ces trois voix singulières sont celles de femmes rebelles liées par un même combat : dans une démarche de type postcolonial, elles ont revisité l'histoire régionale afin de faire voler en éclats un siècle de représentations essentialistes et de dénoncer la destruction environnementale infligée aux montagnes appalachiennes par l'industrie houillère / The aim of this research is to look into the invention of Appalachia as a « strange and peculiar » region. Nineteenth-century « local color » writers contributed to etching the oxymoronic image of the Appalachian as – the good savage, but mostly as the degenerate hillbilly – in the national consciousness. Starting in the interwar period, then in the late 1960s during the « Appalachian Renaissance », native writers rose up to reject this prescribed identity, among whom Mary Lee Settle, Lee Smith and Denise Giardina. These three singular voices belong to rebel women united in a common fight: using a postcolonial approach, they have revisited the regional history to shatter century-old essentialist representations and to denounce the MTR devastation caused by the coalmining industry in the Appalachian Mountains

Cette thèse traite des métamorphoses de Jinsuo ji, roman d’Eileen Chang publié à Shanghai en 1943. Il s’agit d’abord d’une double réécriture translingue par l’écrivaine elle-même, exilée aux États-Unis depuis 1955. L’analyse des procédés de réécriture dans ces deux romans jumeaux, l’un en anglais intitulé The Rouge of the North (1967), l’autre en chinois Yuannü (1966), permet de faire la lumière sur les stratégies d’écriture bilingue et l’évolution stylistique de l’auteur face à deux lectorats distincts. En 1971, l’auto-traduction stricto sensu de Jinsuo ji est parue sous le titre The Golden Cangue. La publication de cette version littéralisante dans le cercle universitaire américain nous conduit à nous interroger par ailleurs sur l’identité d’une œuvre et sur le statut littéraire de sa traduction, auctoriale ou non. Cela nous permet d’une part de proposer un autre regard sur la réception inégale des écrits d’Eileen Chang en deux langues, et d’autre part, de percevoir, à travers son exemple, un espace « trans-littéraire » qui reste à construire via la traduction, afin qu’une œuvre littéraire puisse entrer en contact avec un nouveau public et dévoiler ainsi sa pluralité. En suivant ce trajet vers l’autre, nos réflexions se prolongent jusqu’aux réécritures non auctoriales de Jinsuo ji. Depuis les années 1980, l’œuvre s’est métamorphosée dans le monde sinophone en film, pièce de théâtre, opéra chinois et série télévisée : ces dernières métamorphoses ne traduisent pas seulement l’engouement toujours vif du public sinophone pour les œuvres d’Eileen Chang, mais elles nous permettent aussi d'observer l’image en devenir de l’écrivaine au fil de leurs réceptions différentes. / This thesis focuses on the metamorphosis of Eileen Chang’s novelette, Jinsuo ji, first published in Shanghai in 1943. In the 1960s, the author, who had been living in the United States since 1955, rewrote this work into an English-language novel, The Rouge of the North, and published almost simultaneously a Chinese version, Yuannü. Through the analysis of her translingual rewriting, an attempt will be made to explore the differences between these versions, in order to shed light on the strategies of rewriting and the evolution of Eileen Chang’s style vis-à-vis two different readerships. Moreover, in 1971, her self-translation of Jinsuo ji, The Golden Cangue, was published in the American academic circle. The study of this English version leads us to reconsider the “identity” of a literary work and the “literary status” of its translation, be it authorial or not. More precisely, the different reception of two versions of a work in Eileen Chang’s case is re-examined from a “trans-literary” perspective: in order to bring a literary work to its new public, thus revealing its plurality, it seems that an interspace between literatures remains to be constructed through translation. By tracing the trajectory of a work towards the other, our reflections will be eventually extended to a number of contemporary adaptations of Jinsuo ji and Yuannü. Since the 1980s, these two works have been adapted into film, theater, Chinese opera and TV series in the Sinophone world. These cross-field rewritings not only reveal the Sinophone public’s passion for Eileen Chang’s works, but also allow us to observe the changing image of the writer in the process of their different receptions.

Dans cette thèse, nous présentons des applications de la réécriture à l'étude de problèmes issus de la catégorification et de la théorie des représentations. En particulier, nous appliquons les méthodes de réécriture aux problèmes de cohérence dans les catégories linéaires et au calcul de décatégorifications. Des méthodes de réécriture ont été développées pour obtenir des résultats de cohérence dans les monoïdes et les catégories monoïdales présentés par des systèmes de réécriture nommés polygraphes. Ces constructions basées sur des résultats de Squier permettent en particulier de calculer des présentations cohérentes de catégories de dimension supérieure à partir des diagrammes de confluence de polygraphes convergents. Dans ce mémoire, nous étendons ces constructions pour obtenir des résultats de cohérence dans les catégories linéaires de dimension supérieure. Nous introduisons les polygraphes linéaires afin de présenter les catégories linéaires de dimension supérieure par des systèmes de réécriture. Nous étudions ensuite les propriétés de réécriture de ces systèmes. Nous donnons une description polygraphique du calcul de décatégorification de Grothendieck. Nous généralisons également la procédure de Knuth-Bendix appliquée aux polygraphes de dimension supérieure. Cette procédure permet de compléter des présentations de catégories de dimension supérieure n'admettant pas nécessairement d'ordre de terminaison induit par une orientation des règles. De plus, nous étudions des problèmes de cohérence dans les catégories de dimension supérieure. Etant donné un polygraphe confluent et quasi-terminant, nous introduisons une notion de complétion de Squier de ce polygraphe composée de diagrammes de décroissance. Nous prouvons que cette complétion rend asphérique la catégorie de dimension supérieure libre sur ce polygraphe. Ce résultat généralise un résultat de Squier au cas des présentations quasi-terminantes. Nous présentons enfin les applications des propriétés des polygraphes linéaire à l'étude de la catégorie AOB définie par Brundan, Comes, Nash et Reynolds. Nous retrouvons par des méthodes de réécriture les bases des espaces de morphismes de AOB exhibées par Brundan, Comes, Nash and Reynolds / In this thesis, we study applications of rewriting theory to categorification problems and representation theory. We apply rewriting methods to coherence problems in linear categories and computation of decategorifications.Proofs of coherence results for monoids and monoidal categories by rewriting methods are well known. In particular, several constructions based on Squier's results lead to the computation of coherent presentations of higher-dimensional categories from the confluence diagrams of convergent rewriting systems. In this memoir, we extend those constructions to coherence results for higher-dimensional linear categories.We introduce linear polygraphs to present higher-dimensional linear categories by rewriting systems. We then develop the main rewriting properties of these systems. We focus next on the applications of those properties to the study of categorification problems such that the computation of Grothendieck decategorification by rewriting methods. Another result we obtain on higher-dimensional polygraphs is a generalization of the Knuth-Bendix procedure to higher-dimensional polygraphs. This new procedure allows us to complete presentations of higher-dimensional categories which do not necessarily admit a termination order induced by any orientation of rules.We also study general coherence problems. Given a confluent and quasi-terminating polygraph, we define a globular extension of this polygraph called decreasing Squier's completion. We prove that this extension makes aspherical the free higher-dimensional category over the given polygraph. This result generalizes a result of Squier to the case of non terminating presentations.Finally, we focus on the applications of those properties to higher-dimensional linear categories such that the category AOB defined by Brundan, Comes, Nash and Reynolds. We find by rewriting methods the bases of the morphisms spaces of AOB that Brundan, Comes, Nash and Reynolds exhibited

Ces dernières années, on a assisté au développement du<br />calcul de réécriture, encore appelé rho-calcul, qui intègre de<br />façon uniforme la réécriture de premier ordre et le lambda-calcul.<br />Cette thèse est dédiée à l'étude des capacités d'expression du calcul de réécriture, avec un intérêt particulier pour la réécriture d'ordre supérieur et la possibilité de manipuler des graphes.<br /><br />Dans la première partie de cette thèse, la relation entre le calcul de réécriture et la réécriture d'ordre supérieur, en particulier les Combinatory Reduction Systems (CRSs), est étudiée.<br />Nous présentons d'abord un algorithme de filtrage original<br />pour les CRSs qui utilise une traduction des termes CRS en<br />lambda-termes et le filtrage d'ordre supérieur classique du lambda-calcul. Nous proposons ensuite un encodage des CRSs dans le rho-calcul<br />basé sur la traduction de chaque réduction CRS<br />en une réduction correspondante dans le rho-calcul.<br />Dans la deuxième partie, nous présentons une extension du rho-calcul,<br />appelé calcul de réécriture de graphes (ou Rg-calcul),<br />qui gère des termes avec partage et cycles.<br />Le calcul sur les termes est généralisé de manière naturelle en utilisant des contraintes d'unification en plus des contraintes de filtrage standard du rho-calcul.<br /><br />Le Rg-calcul est alors montré confluent sur des classes<br />d'équivalence de termes, sous certaines restrictions de linéarité sur les motifs, et assez<br />expressif pour simuler la réécriture de termes graphes et le<br />lambda-calcul cyclique.

L’analyse d’accessibilité est une des composantes de l’analyse de modèles. Elle consiste à modéliser un système complexe par trois ensembles : le langage initial, le langage des configurations indésirables et un système de réécriture. Le langage initial et le langage des configurations indésirables sont des ensembles de termes. Un terme est un mot mais construit à partir de symboles d’arités supérieures à 1. Le système de réécriture représente la dynamique du système complexe. C’est un ensemble de règles qui permettent d’obtenir un nouveau terme à partir d’un terme original. Pour effectuer une analyse d’accessibilité à partir de cette modélisation, on peut calculer l’ensemble des configurations accessibles. Cet ensemble aussi appelé ensemble des descendants est obtenu en appliquant le système de réécriture sur le langage initial jusqu’à ne plus obtenir de nouveaux termes. Une fois l’ensemble des descendants calculé, il reste à faire l’intersection entre celui-ci et l’ensemble des configurations indésirables. Si cette intersection est vide, alors il n’y a pas de configuration indésirable accessible, sinon les configurations présentes dans cette intersection sont accessibles. Cependant, l’ensemble des descendants n’est pas calculable dans le cas général. Pour contourner ce problème, nous calculons une sur-approximation des descendants. Ainsi, si l’intersection est vide, cela signifie toujours qu’aucune configuration indésirable n’est accessible. A contrario, s’il existe un terme dans l’intersection, il n’est pas possible de déterminer s’il s’agit d’un faux positif ou d’une configuration indésirable accessible. La précision de la sur-approximation est alors déterminante. / Reachability analysis is part of model checking. It consists to model complex systems by three sets : initial language, unwanted configurations and rewrite system. The initial language and the unwanted configurations language are sets of terms. Terms are words which are construct with symbols that have an arity that can be greater than 1. The rewrite system represent the dynamic of the complex system. It is a set of rules that permit from a initial term to obtain a new term. One of the approaches to analyze reachability from this modelling is to compute the set of reachable configurations. This set which is called set of descendants is obtained by applying the rewrite system on the initial language until obtaining no more new terms. After the set of descendants is computed, we need to compute the intersection between this set and the unwanted configurations set. If this intersection is empty then there is no unwanted configuration reachable, else the configurations in this intersection are reachable. However, the set of descendants is not computable in the general case. To bypass this problem, we compute an over-approximation of descendants.Now, if the intersection is empty, we keep proving that no unwanted configuration is reachable. Nevertheless, if the intersection is not empty, it is not possible to know if it comes from false-positives or form unwanted reachable configurations. So, the precision of the over-approximation is decisive.