Expressing combinatory reduction systems derivations in the rewriting calculus
Identifieur interne : 005791 ( Main/Merge ); précédent : 005790; suivant : 005792Expressing combinatory reduction systems derivations in the rewriting calculus
Auteurs : Clara Bertolissi [France] ; Horatiu Cirstea [France] ; Claude Kirchner [France]Source :
- Higher-order and symbolic computation [ 1388-3690 ] ; 2006.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
The last few years have seen the development of the rewriting calculus (also called rho-calculus or p-calculus) that uniformly integrates first-order term rewriting and the λ-calculus. The combination of these two latter formalisms has been already handled either by enriching first-order rewriting with higher-order capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to the λ-calculus algebraic features. The various higher-order rewriting systems and the rewriting calculus share similar concepts and have similar applications, and thus, it is important to compare these formalisms to better understand their respective strengths and differences. We show in this paper that we can express Combinatory Reduction Systems derivations in terms of rewriting calculus derivations. The approach we present is based on a translation of each possible CRS-reduction into a corresponding p-reduction. Since for this purpose we need to make precise the matching used when evaluating CRS, the second contribution of the paper is to present an original matching algorithm for CRS terms that uses a simple term translation and the classical matching of lambda terms.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000403
- to stream PascalFrancis, to step Curation: 000630
- to stream PascalFrancis, to step Checkpoint: 000386
Links to Exploration step
Pascal:07-0067715Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Expressing combinatory reduction systems derivations in the rewriting calculus</title><author><name sortKey="Bertolissi, Clara" sort="Bertolissi, Clara" uniqKey="Bertolissi C" first="Clara" last="Bertolissi">Clara Bertolissi</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101</s1><s2>54602 Villers-lès-Nancy 54506</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-lès-Nancy 54506</settlement></placeName></affiliation></author><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101</s1><s2>54602 Villers-lès-Nancy 54506</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-lès-Nancy 54506</settlement></placeName></affiliation></author><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101</s1><s2>54602 Villers-lès-Nancy 54506</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-lès-Nancy 54506</settlement></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">07-0067715</idno><date when="2006">2006</date><idno type="stanalyst">PASCAL 07-0067715 INIST</idno><idno type="RBID">Pascal:07-0067715</idno><idno type="wicri:Area/PascalFrancis/Corpus">000403</idno><idno type="wicri:Area/PascalFrancis/Curation">000630</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000386</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000386</idno><idno type="wicri:doubleKey">1388-3690:2006:Bertolissi C:expressing:combinatory:reduction</idno><idno type="wicri:Area/Main/Merge">005791</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Expressing combinatory reduction systems derivations in the rewriting calculus</title><author><name sortKey="Bertolissi, Clara" sort="Bertolissi, Clara" uniqKey="Bertolissi C" first="Clara" last="Bertolissi">Clara Bertolissi</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101</s1><s2>54602 Villers-lès-Nancy 54506</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-lès-Nancy 54506</settlement></placeName></affiliation></author><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101</s1><s2>54602 Villers-lès-Nancy 54506</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-lès-Nancy 54506</settlement></placeName></affiliation></author><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101</s1><s2>54602 Villers-lès-Nancy 54506</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-lès-Nancy 54506</settlement></placeName></affiliation></author></analytic><series><title level="j" type="main">Higher-order and symbolic computation</title><title level="j" type="abbreviated">Higher-order symb. comput.</title><idno type="ISSN">1388-3690</idno><imprint><date when="2006">2006</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Higher-order and symbolic computation</title><title level="j" type="abbreviated">Higher-order symb. comput.</title><idno type="ISSN">1388-3690</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithm</term><term>Combinatory reduction system</term><term>Matching task</term><term>Rewriting calculus</term><term>Symbolic computation</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Tâche appariement</term><term>Algorithme</term><term>Calcul symbolique</term><term>Calcul lambda</term><term>Term rewriting systems</term><term>Système réécriture terme</term><term>Système réduction combinatoire</term><term>Calcul réécriture</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">The last few years have seen the development of the rewriting calculus (also called rho-calculus or p-calculus) that uniformly integrates first-order term rewriting and the λ-calculus. The combination of these two latter formalisms has been already handled either by enriching first-order rewriting with higher-order capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to the λ-calculus algebraic features. The various higher-order rewriting systems and the rewriting calculus share similar concepts and have similar applications, and thus, it is important to compare these formalisms to better understand their respective strengths and differences. We show in this paper that we can express Combinatory Reduction Systems derivations in terms of rewriting calculus derivations. The approach we present is based on a translation of each possible CRS-reduction into a corresponding p-reduction. Since for this purpose we need to make precise the matching used when evaluating CRS, the second contribution of the paper is to present an original matching algorithm for CRS terms that uses a simple term translation and the classical matching of lambda terms.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Villers-lès-Nancy 54506</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Bertolissi, Clara" sort="Bertolissi, Clara" uniqKey="Bertolissi C" first="Clara" last="Bertolissi">Clara Bertolissi</name></region><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name></country></tree></affiliations></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 005791 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 005791 | 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é= Pascal:07-0067715
|texte= Expressing combinatory reduction systems derivations in the rewriting calculus
}}
| This area was generated with Dilib version V0.6.33. |  |