Confluence of Pattern-Based Calculi
Identifieur interne : 004C85 ( Main/Exploration ); précédent : 004C84; suivant : 004C86Confluence of Pattern-Based Calculi
Auteurs : Horatiu Cirstea [France] ; Germain Faure [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Different pattern calculi integrate the functional mechanisms from the λ-calculus and the matching capabilities from rewriting. Several approaches are used to obtain the confluence but in practice the proof methods share the same structure and each variation on the way pattern-abstractions are applied needs another proof of confluence. We propose here a generic confluence proof where the way pattern-abstractions are applied is axiomatized. Intuitively, the conditions guarantee that the matching is stable by substitution and by reduction. We show that our approach directly applies to different pattern calculi, namely the lambda calculus with patterns, the pure pattern calculus and the rewriting calculus. We also characterize a class of matching algorithms and consequently of pattern-calculi that are not confluent.
Url:
DOI: 10.1007/978-3-540-73449-9_8
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001F82
- to stream Istex, to step Curation: 001F56
- to stream Istex, to step Checkpoint: 001070
- to stream Hal, to step Corpus: 001830
- to stream Hal, to step Curation: 001830
- to stream Hal, to step Checkpoint: 003998
- to stream Main, to step Merge: 004E19
- to stream Main, to step Curation: 004C85
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Confluence of Pattern-Based Calculi</title><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name></author><author><name sortKey="Faure, Germain" sort="Faure, Germain" uniqKey="Faure G" first="Germain" last="Faure">Germain Faure</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:8978A7519D649A77C88F385530744FF431D79950</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/978-3-540-73449-9_8</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-P909SSDW-V/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001F82</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001F82</idno><idno type="wicri:Area/Istex/Curation">001F56</idno><idno type="wicri:Area/Istex/Checkpoint">001070</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001070</idno><idno type="wicri:doubleKey">0302-9743:2007:Cirstea H:confluence:of:pattern</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00185882</idno><idno type="url">https://hal.inria.fr/inria-00185882</idno><idno type="wicri:Area/Hal/Corpus">001830</idno><idno type="wicri:Area/Hal/Curation">001830</idno><idno type="wicri:Area/Hal/Checkpoint">003998</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003998</idno><idno type="wicri:Area/Main/Merge">004E19</idno><idno type="wicri:Area/Main/Curation">004C85</idno><idno type="wicri:Area/Main/Exploration">004C85</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Confluence of Pattern-Based Calculi</title><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Université Nancy 2 & Université Henri Poincaré & LORIA, BP 239, F-54506 Vandoeuvre-lès-Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Faure, Germain" sort="Faure, Germain" uniqKey="Faure G" first="Germain" last="Faure">Germain Faure</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Université Nancy 2 & Université Henri Poincaré & LORIA, BP 239, F-54506 Vandoeuvre-lès-Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</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: Different pattern calculi integrate the functional mechanisms from the λ-calculus and the matching capabilities from rewriting. Several approaches are used to obtain the confluence but in practice the proof methods share the same structure and each variation on the way pattern-abstractions are applied needs another proof of confluence. We propose here a generic confluence proof where the way pattern-abstractions are applied is axiomatized. Intuitively, the conditions guarantee that the matching is stable by substitution and by reduction. We show that our approach directly applies to different pattern calculi, namely the lambda calculus with patterns, the pure pattern calculus and the rewriting calculus. We also characterize a class of matching algorithms and consequently of pattern-calculi that are not confluent.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name></region><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name><name sortKey="Faure, Germain" sort="Faure, Germain" uniqKey="Faure G" first="Germain" last="Faure">Germain Faure</name><name sortKey="Faure, Germain" sort="Faure, Germain" uniqKey="Faure G" first="Germain" last="Faure">Germain Faure</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004C85 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004C85 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:8978A7519D649A77C88F385530744FF431D79950
|texte= Confluence of Pattern-Based Calculi
}}
| This area was generated with Dilib version V0.6.33. |  |