Confluence of Pattern-Based Calculi
Identifieur interne : 004E19 ( Main/Merge ); précédent : 004E18; suivant : 004E20Confluence 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
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
Links to Exploration step
ISTEX:8978A7519D649A77C88F385530744FF431D79950Le 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></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><double doi="10.1007/978-3-540-73449-9_8"><HAL><TEI><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><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno><orgName>Constraints, automatic deduction and software properties proofs</orgName><orgName type="acronym">PROTHEO</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/protheo</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Faure, Germain" sort="Faure, Germain" uniqKey="Faure G" first="Germain" last="Faure">Germain Faure</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno><orgName>Constraints, automatic deduction and software properties proofs</orgName><orgName type="acronym">PROTHEO</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/protheo</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00185882</idno><idno type="halId">inria-00185882</idno><idno type="halUri">https://hal.inria.fr/inria-00185882</idno><idno type="url">https://hal.inria.fr/inria-00185882</idno><idno type="doi">10.1007/978-3-540-73449-9_8</idno><date when="2007-06-26">2007-06-26</date><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></publicationStmt><sourceDesc><biblStruct><analytic><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><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno><orgName>Constraints, automatic deduction and software properties proofs</orgName><orgName type="acronym">PROTHEO</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/protheo</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Faure, Germain" sort="Faure, Germain" uniqKey="Faure G" first="Germain" last="Faure">Germain Faure</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno><orgName>Constraints, automatic deduction and software properties proofs</orgName><orgName type="acronym">PROTHEO</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/protheo</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation><relation active="#struct-2496" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author></analytic><idno type="DOI">10.1007/978-3-540-73449-9_8</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Different pattern calculi integrate the functional mechanisms from the lambda-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></HAL><ISTEX><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></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></ISTEX></double></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004E19 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 004E19 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= ISTEX:8978A7519D649A77C88F385530744FF431D79950
|texte= Confluence of Pattern-Based Calculi
}}
| This area was generated with Dilib version V0.6.33. |  |