Calcul de réécriture : fondements et applications
Identifieur interne : 002B74 ( Crin/Curation ); précédent : 002B73; suivant : 002B75Calcul de réécriture : fondements et applications
Auteurs : Horatiu CirsteaSource :
English descriptors
- KwdEn :
Abstract
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.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002B74
Links to Exploration step
CRIN:cirstea00eLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="-93">Calcul de réécriture : fondements et applications</title></titleStmt><publicationStmt><idno type="RBID">CRIN:cirstea00e</idno><date when="2000" year="2000">2000</date><idno type="wicri:Area/Crin/Corpus">002B74</idno><idno type="wicri:Area/Crin/Curation">002B74</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">002B74</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Calcul de réécriture : fondements et applications</title><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>lambda-calculus</term><term>matching</term><term>non-determinism</term><term>rewriting</term><term>rewriting calculus</term><term>rule based language</term><term>strategy</term><term>substitution</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr" wicri:score="-5160">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.</div></front></TEI><BibTex type="phdthesis"><ref>cirstea00e</ref><crinnumber>A00-T-277</crinnumber><category>9</category><equipe>PROTHEO</equipe><author><e>Cirstea, Horatiu</e></author><title>Calcul de réécriture : fondements et applications</title><school>Université Henri Poincaré</school><year>2000</year><type>Thèse d'université</type><month>Oct</month><keywords><e>rewriting calculus</e><e>rewriting</e><e>non-determinism</e><e>strategy</e><e>matching</e><e>substitution</e><e>lambda-calculus</e><e>rule based language</e></keywords><abstract>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.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002B74 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/biblio.hfd -nk 002B74 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Curation
|type= RBID
|clé= CRIN:cirstea00e
|texte= Calcul de réécriture : fondements et applications
}}
| This area was generated with Dilib version V0.6.33. |  |