On the confluence of λ-calculus with conditional rewriting
Identifieur interne :
000380 ( PascalFrancis/Corpus );
précédent :
000379;
suivant :
000381
On the confluence of λ-calculus with conditional rewriting
Auteurs : Frédéric Blanqui ;
Claude Kirchner ;
Colin RibaSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2006.
RBID : Pascal:07-0534058
Descripteurs français
English descriptors
Abstract
The confluence of untyped A-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of A-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
| pA |
| A01 | 01 | 1 | | @0 0302-9743 |
|---|
| A05 | | | | @2 3921 |
|---|
| A08 | 01 | 1 | ENG | @1 On the confluence of λ-calculus with conditional rewriting |
|---|
| A09 | 01 | 1 | ENG | @1 Foundations of software science and computation structures : 9th international conference, FOSSACS 2006, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006 : proceedings |
|---|
| A11 | 01 | 1 | | @1 BLANQUI (Frédéric) |
|---|
| A11 | 02 | 1 | | @1 KIRCHNER (Claude) |
|---|
| A11 | 03 | 1 | | @1 RIBA (Colin) |
|---|
| A12 | 01 | 1 | | @1 ACETO (Luca) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 ANNA INGOLFSDOTTIR @9 ed. |
|---|
| A14 | 01 | | | @1 INRIA & LORIA @3 INC @Z 1 aut. @Z 2 aut. |
|---|
| A14 | 02 | | | @1 INPL & LORIA @3 INC @Z 3 aut. |
|---|
| A20 | | | | @1 382-397 |
|---|
| A21 | | | | @1 2006 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-33045-3 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000153603170260 |
|---|
| A44 | | | | @0 0000 @1 © 2007 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 23 ref. |
|---|
| A47 | 01 | 1 | | @0 07-0534058 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 DEU |
|---|
| A66 | 02 | | | @0 USA |
|---|
| C01 | 01 | | ENG | @0 The confluence of untyped A-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of A-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules. |
|---|
| C02 | 01 | X | | @0 001D02B09 |
|---|
| C03 | 01 | X | FRE | @0 Développement logiciel @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Software development @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Desarrollo logicial @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Lambda calcul @5 06 |
|---|
| C03 | 02 | X | ENG | @0 Lambda calculus @5 06 |
|---|
| C03 | 02 | X | SPA | @0 Lambda cálculo @5 06 |
|---|
| C03 | 03 | X | FRE | @0 Orthogonalité @5 07 |
|---|
| C03 | 03 | X | ENG | @0 Orthogonality @5 07 |
|---|
| C03 | 03 | X | SPA | @0 Ortogonalidad @5 07 |
|---|
| C03 | 04 | X | FRE | @0 Confluence @5 18 |
|---|
| C03 | 04 | X | ENG | @0 Confluence @5 18 |
|---|
| C03 | 04 | X | SPA | @0 Confluencia @5 18 |
|---|
| C03 | 05 | X | FRE | @0 Réécriture @5 19 |
|---|
| C03 | 05 | X | ENG | @0 Rewriting @5 19 |
|---|
| C03 | 05 | X | SPA | @0 Reescritura @5 19 |
|---|
| C03 | 06 | X | FRE | @0 Rho calcul @5 23 |
|---|
| C03 | 06 | X | ENG | @0 Rho calculus @5 23 |
|---|
| C03 | 06 | X | SPA | @0 Rho cálculo @5 23 |
|---|
| C03 | 07 | X | FRE | @0 Modularité @4 CD @5 96 |
|---|
| C03 | 07 | X | ENG | @0 Modularity @4 CD @5 96 |
|---|
| C03 | 07 | X | SPA | @0 Modularidad @4 CD @5 96 |
|---|
| N21 | | | | @1 344 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 FOSSACS 2006 @2 9 @3 Vienna AUT @4 2006 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 07-0534058 INIST |
|---|
| ET : | On the confluence of λ-calculus with conditional rewriting |
|---|
| AU : | BLANQUI (Frédéric); KIRCHNER (Claude); RIBA (Colin); ACETO (Luca); ANNA INGOLFSDOTTIR |
|---|
| AF : | INRIA & LORIA/Inconnu (1 aut., 2 aut.); INPL & LORIA/Inconnu (3 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2006; Vol. 3921; Pp. 382-397; Bibl. 23 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | The confluence of untyped A-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of A-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules. |
|---|
| CC : | 001D02B09 |
|---|
| FD : | Développement logiciel; Lambda calcul; Orthogonalité; Confluence; Réécriture; Rho calcul; Modularité |
|---|
| ED : | Software development; Lambda calculus; Orthogonality; Confluence; Rewriting; Rho calculus; Modularity |
|---|
| SD : | Desarrollo logicial; Lambda cálculo; Ortogonalidad; Confluencia; Reescritura; Rho cálculo; Modularidad |
|---|
| LO : | INIST-16343.354000153603170260 |
|---|
| ID : | 07-0534058 |
|---|
Links to Exploration step
Pascal:07-0534058
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">On the confluence of λ-calculus with conditional rewriting</title>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA & LORIA</s1>
<s3>INC</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA & LORIA</s1>
<s3>INC</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Riba, Colin" sort="Riba, Colin" uniqKey="Riba C" first="Colin" last="Riba">Colin Riba</name>
<affiliation><inist:fA14 i1="02"><s1>INPL & LORIA</s1>
<s3>INC</s3>
<sZ>3 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">07-0534058</idno>
<date when="2006">2006</date>
<idno type="stanalyst">PASCAL 07-0534058 INIST</idno>
<idno type="RBID">Pascal:07-0534058</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000380</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">On the confluence of λ-calculus with conditional rewriting</title>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA & LORIA</s1>
<s3>INC</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA & LORIA</s1>
<s3>INC</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Riba, Colin" sort="Riba, Colin" uniqKey="Riba C" first="Colin" last="Riba">Colin Riba</name>
<affiliation><inist:fA14 i1="02"><s1>INPL & LORIA</s1>
<s3>INC</s3>
<sZ>3 aut.</sZ>
</inist:fA14><series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2006">2006</date>
</imprint><seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Confluence</term>
<term>Lambda calculus</term>
<term>Modularity</term>
<term>Orthogonality</term>
<term>Rewriting</term>
<term>Rho calculus</term>
<term>Software development</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Développement logiciel</term>
<term>Lambda calcul</term>
<term>Orthogonalité</term>
<term>Confluence</term>
<term>Réécriture</term>
<term>Rho calcul</term>
<term>Modularité</term>
</keywords><front><div type="abstract" xml:lang="en">The confluence of untyped A-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of A-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>3921</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>On the confluence of λ-calculus with conditional rewriting</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>Foundations of software science and computation structures : 9th international conference, FOSSACS 2006, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006 : proceedings</s1>
</fA09><fA11 i1="01" i2="1"><s1>BLANQUI (Frédéric)</s1>
</fA11><fA11 i1="02" i2="1"><s1>KIRCHNER (Claude)</s1>
</fA11><fA11 i1="03" i2="1"><s1>RIBA (Colin)</s1>
</fA11><fA12 i1="01" i2="1"><s1>ACETO (Luca)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>ANNA INGOLFSDOTTIR</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>INRIA & LORIA</s1>
<s3>INC</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</fA14><fA14 i1="02"><s1>INPL & LORIA</s1>
<s3>INC</s3>
<sZ>3 aut.</sZ>
</fA14><fA20><s1>382-397</s1>
</fA20><fA21><s1>2006</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-33045-3</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000153603170260</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2007 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>23 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>07-0534058</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64><fA66 i1="01"><s0>DEU</s0>
</fA66><fA66 i1="02"><s0>USA</s0>
</fA66><fC01 i1="01" l="ENG"><s0>The confluence of untyped A-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of A-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02B09</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Développement logiciel</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Software development</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Desarrollo logicial</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Lambda calcul</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Lambda calculus</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Lambda cálculo</s0>
<s5>06</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Orthogonalité</s0>
<s5>07</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Orthogonality</s0>
<s5>07</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Ortogonalidad</s0>
<s5>07</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Confluence</s0>
<s5>18</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Confluence</s0>
<s5>18</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Confluencia</s0>
<s5>18</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Réécriture</s0>
<s5>19</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Rewriting</s0>
<s5>19</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Reescritura</s0>
<s5>19</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Rho calcul</s0>
<s5>23</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Rho calculus</s0>
<s5>23</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Rho cálculo</s0>
<s5>23</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Modularité</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Modularity</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Modularidad</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fN21><s1>344</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>FOSSACS 2006</s1>
<s2>9</s2>
<s3>Vienna AUT</s3>
<s4>2006</s4>
</fA30><server><NO>PASCAL 07-0534058 INIST</NO>
<ET>On the confluence of λ-calculus with conditional rewriting</ET>
<AU>BLANQUI (Frédéric); KIRCHNER (Claude); RIBA (Colin); ACETO (Luca); ANNA INGOLFSDOTTIR</AU>
<AF>INRIA & LORIA/Inconnu (1 aut., 2 aut.); INPL & LORIA/Inconnu (3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2006; Vol. 3921; Pp. 382-397; Bibl. 23 ref.</SO>
<LA>Anglais</LA>
<EA>The confluence of untyped A-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of A-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.</EA>
<CC>001D02B09</CC>
<FD>Développement logiciel; Lambda calcul; Orthogonalité; Confluence; Réécriture; Rho calcul; Modularité</FD>
<ED>Software development; Lambda calculus; Orthogonality; Confluence; Rewriting; Rho calculus; Modularity</ED>
<SD>Desarrollo logicial; Lambda cálculo; Ortogonalidad; Confluencia; Reescritura; Rho cálculo; Modularidad</SD>
<LO>INIST-16343.354000153603170260</LO>
<ID>07-0534058</ID>
</server>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000380 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000380 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Corpus
|type= RBID
|clé= Pascal:07-0534058
|texte= On the confluence of λ-calculus with conditional rewriting
}}
| This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 |  |
