InforLorV4, PascalFrancis, Corpus, bibRecord, 000403

Expressing combinatory reduction systems derivations in the rewriting calculus

Identifieur interne : 000403 ( PascalFrancis/Corpus ); précédent : 000402; suivant : 000404

Expressing combinatory reduction systems derivations in the rewriting calculus

Auteurs : Clara Bertolissi ; Horatiu Cirstea ; Claude Kirchner

Source :

Higher-order and symbolic computation [ 1388-3690 ] ; 2006.

RBID : Pascal:07-0067715

Descripteurs français

Pascal (Inist)
- Tâche appariement, Algorithme, Calcul symbolique, Calcul lambda, Term rewriting systems, Système réécriture terme, Système réduction combinatoire, Calcul réécriture.

English descriptors

KwdEn :
- Algorithm, Combinatory reduction system, Matching task, Rewriting calculus, Symbolic computation.

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.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 1388-3690`
A03		`1`		`@0 Higher-order symb. comput.`
A05				`@2 19`
A06				`@2 4`
A08	`01`	`1`	`ENG`	`@1 Expressing combinatory reduction systems derivations in the rewriting calculus`
A11	`01`	`1`		`@1 BERTOLISSI (Clara)`
A11	`02`	`1`		`@1 CIRSTEA (Horatiu)`
A11	`03`	`1`		`@1 KIRCHNER (Claude)`
A14	`01`			`@1 LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101 @2 54602 Villers-lès-Nancy 54506 @3 FRA @Z 1 aut. @Z 2 aut. @Z 3 aut.`
A20				`@1 345-376`
A21				`@1 2006`
A23	`01`			`@0 ENG`
A43	`01`			`@1 INIST @2 21729 @5 354000159710060010`
A44				`@0 0000 @1 © 2007 INIST-CNRS. All rights reserved.`
A45				`@0 28 ref.`
A47	`01`	`1`		`@0 07-0067715`
A60				`@1 P`
A61				`@0 A`
A64	`01`	`1`		`@0 Higher-order and symbolic computation`
A66	`01`			`@0 DEU`
C01	`01`		`ENG`	@0 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.
C02	`01`	`X`		`@0 001A02A01B`
C02	`02`	`X`		`@0 001D02A07`
C02	`03`	`X`		`@0 001D02A05`
C03	`01`	`X`	`FRE`	`@0 Tâche appariement @5 17`
C03	`01`	`X`	`ENG`	`@0 Matching task @5 17`
C03	`01`	`X`	`SPA`	`@0 Tarea apareamiento @5 17`
C03	`02`	`X`	`FRE`	`@0 Algorithme @5 18`
C03	`02`	`X`	`ENG`	`@0 Algorithm @5 18`
C03	`02`	`X`	`SPA`	`@0 Algoritmo @5 18`
C03	`03`	`X`	`FRE`	`@0 Calcul symbolique @5 19`
C03	`03`	`X`	`ENG`	`@0 Symbolic computation @5 19`
C03	`03`	`X`	`SPA`	`@0 Cálculo simbólico @5 19`
C03	`04`	`X`	`FRE`	`@0 Calcul lambda @4 INC @5 70`
C03	`05`	`X`	`FRE`	`@0 Term rewriting systems @4 INC @5 74`
C03	`06`	`X`	`FRE`	`@0 Système réécriture terme @4 INC @5 75`
C03	`07`	`X`	`FRE`	`@0 Système réduction combinatoire @4 CD @5 96`
C03	`07`	`X`	`ENG`	`@0 Combinatory reduction system @4 CD @5 96`
C03	`08`	`X`	`FRE`	`@0 Calcul réécriture @4 CD @5 97`
C03	`08`	`X`	`ENG`	`@0 Rewriting calculus @4 CD @5 97`
N21				`@1 043`

Format Inist (serveur)

NO :	PASCAL 07-0067715 INIST
ET :	Expressing combinatory reduction systems derivations in the rewriting calculus
AU :	BERTOLISSI (Clara); CIRSTEA (Horatiu); KIRCHNER (Claude)
AF :	LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101/54602 Villers-lès-Nancy 54506/France (1 aut., 2 aut., 3 aut.)
DT :	Publication en série; Niveau analytique
SO :	Higher-order and symbolic computation; ISSN 1388-3690; Allemagne; Da. 2006; Vol. 19; No. 4; Pp. 345-376; Bibl. 28 ref.
LA :	Anglais
EA :	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.
CC :	001A02A01B; 001D02A07; 001D02A05
FD :	Tâche appariement; Algorithme; Calcul symbolique; Calcul lambda; Term rewriting systems; Système réécriture terme; Système réduction combinatoire; Calcul réécriture
ED :	Matching task; Algorithm; Symbolic computation; Combinatory reduction system; Rewriting calculus
SD :	Tarea apareamiento; Algoritmo; Cálculo simbólico
LO :	INIST-21729.354000159710060010
ID :	07-0067715

Links to Exploration step

Pascal:07-0067715

Le 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><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>
</affiliation>
</author>
<author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name>
<affiliation><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>
</affiliation>
</author>
<author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation><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>
</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>
</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><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>
</affiliation>
</author>
<author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name>
<affiliation><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>
</affiliation>
</author>
<author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation><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>
</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>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>1388-3690</s0>
</fA01>
<fA03 i2="1"><s0>Higher-order symb. comput.</s0>
</fA03>
<fA05><s2>19</s2>
</fA05>
<fA06><s2>4</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>Expressing combinatory reduction systems derivations in the rewriting calculus</s1>
</fA08>
<fA11 i1="01" i2="1"><s1>BERTOLISSI (Clara)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>CIRSTEA (Horatiu)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>KIRCHNER (Claude)</s1>
</fA11>
<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>
</fA14>
<fA20><s1>345-376</s1>
</fA20>
<fA21><s1>2006</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>21729</s2>
<s5>354000159710060010</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2007 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>28 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>07-0067715</s0>
</fA47>
<fA60><s1>P</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Higher-order and symbolic computation</s0>
</fA64>
<fA66 i1="01"><s0>DEU</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>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.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001A02A01B</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02A07</s0>
</fC02>
<fC02 i1="03" i2="X"><s0>001D02A05</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Tâche appariement</s0>
<s5>17</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Matching task</s0>
<s5>17</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Tarea apareamiento</s0>
<s5>17</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Algorithme</s0>
<s5>18</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Algorithm</s0>
<s5>18</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Algoritmo</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Calcul symbolique</s0>
<s5>19</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Symbolic computation</s0>
<s5>19</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Cálculo simbólico</s0>
<s5>19</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Calcul lambda</s0>
<s4>INC</s4>
<s5>70</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Term rewriting systems</s0>
<s4>INC</s4>
<s5>74</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Système réécriture terme</s0>
<s4>INC</s4>
<s5>75</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Système réduction combinatoire</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Combinatory reduction system</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Calcul réécriture</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Rewriting calculus</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fN21><s1>043</s1>
</fN21>
</pA>
</standard>
<server><NO>PASCAL 07-0067715 INIST</NO>
<ET>Expressing combinatory reduction systems derivations in the rewriting calculus</ET>
<AU>BERTOLISSI (Clara); CIRSTEA (Horatiu); KIRCHNER (Claude)</AU>
<AF>LORIA & INRIA, UHP, University Nancy II, 615, rue du Jardin Botanique, BP-101/54602 Villers-lès-Nancy 54506/France (1 aut., 2 aut., 3 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>Higher-order and symbolic computation; ISSN 1388-3690; Allemagne; Da. 2006; Vol. 19; No. 4; Pp. 345-376; Bibl. 28 ref.</SO>
<LA>Anglais</LA>
<EA>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.</EA>
<CC>001A02A01B; 001D02A07; 001D02A05</CC>
<FD>Tâche appariement; Algorithme; Calcul symbolique; Calcul lambda; Term rewriting systems; Système réécriture terme; Système réduction combinatoire; Calcul réécriture</FD>
<ED>Matching task; Algorithm; Symbolic computation; Combinatory reduction system; Rewriting calculus</ED>
<SD>Tarea apareamiento; Algoritmo; Cálculo simbólico</SD>
<LO>INIST-21729.354000159710060010</LO>
<ID>07-0067715</ID>
</server>
</inist>
</record>

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 000403 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000403 | 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-0067715
   |texte=   Expressing combinatory reduction systems derivations in the rewriting calculus
}}

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

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Expressing combinatory reduction systems derivations in the rewriting calculus

Expressing combinatory reduction systems derivations in the rewriting calculus

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri