Confluent and coherent equational term rewriting systems application to proofs in abstract data types
Identifieur interne : 003833 ( Istex/Checkpoint ); précédent : 003832; suivant : 003834Confluent and coherent equational term rewriting systems application to proofs in abstract data types
Auteurs : Jean-Pierre JouannaudSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The well known Knuth and Bendix completion procedure computes a convergent term rewriting system from a given set of equational axioms. We describe here an abstract model of computation to handle the case where some axioms cannot be treated as rewrite rules without loosing the required termination property. We call Equational Term Rewriting Systems such mixted sets of rules and equations. We show that two abstract properties, namely E-confluence and E-coherence are both necessary and sufficient ones to compute with these models. These abstract properties can be checked on critical pairs yielding Huet's classical results on “confluence modulo” as well as a more general version of Peterson and Stickel's without any linearity hypothesis on the equations. These results are finally used to check consitency of an algebraic specification of data type.
Url:
DOI: 10.1007/3-540-12727-5_16
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
ISTEX:759672B02CF829A1ADCA71CEFD613A6D48E1F3B1Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Confluent and coherent equational term rewriting systems application to proofs in abstract data types</title><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:759672B02CF829A1ADCA71CEFD613A6D48E1F3B1</idno><date when="1983" year="1983">1983</date><idno type="doi">10.1007/3-540-12727-5_16</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-7C41DQNS-V/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001B06</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001B06</idno><idno type="wicri:Area/Istex/Curation">001A86</idno><idno type="wicri:Area/Istex/Checkpoint">003833</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003833</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Confluent and coherent equational term rewriting systems application to proofs in abstract data types</title><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name><affiliation><wicri:noCountry code="subField">Cedex</wicri:noCountry></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The well known Knuth and Bendix completion procedure computes a convergent term rewriting system from a given set of equational axioms. We describe here an abstract model of computation to handle the case where some axioms cannot be treated as rewrite rules without loosing the required termination property. We call Equational Term Rewriting Systems such mixted sets of rules and equations. We show that two abstract properties, namely E-confluence and E-coherence are both necessary and sufficient ones to compute with these models. These abstract properties can be checked on critical pairs yielding Huet's classical results on “confluence modulo” as well as a more general version of Peterson and Stickel's without any linearity hypothesis on the equations. These results are finally used to check consitency of an algebraic specification of data type.</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name></noCountry></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003833 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 003833 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Checkpoint
|type= RBID
|clé= ISTEX:759672B02CF829A1ADCA71CEFD613A6D48E1F3B1
|texte= Confluent and coherent equational term rewriting systems application to proofs in abstract data types
}}
| This area was generated with Dilib version V0.6.33. |  |