Modeling sharing and recursion for weak reduction strategies using explicit substitution
Identifieur interne :
000C95 ( PascalFrancis/Corpus );
précédent :
000C94;
suivant :
000C96
Modeling sharing and recursion for weak reduction strategies using explicit substitution
Auteurs : Z.-E.-A. Benaissa ;
P. Lescanne ;
K. H. RoseSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 1996.
RBID : Pascal:97-0023506
Descripteurs français
English descriptors
Abstract
We present the λσwa-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how λσwa can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely weak reduction strategies, recursion, space leaks, recursive data structures, and parallel evaluation. We use λσwa to give a unified model of several computational aspects. First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing λ-graph-reduction vs. environment-based evaluation. Second, we show how to add constructors and explicit recursion to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of space leaks in λσwa and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the "trimming" performed by the STG machine does not leak space. In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages.
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 1140 |
|---|
| A08 | 01 | 1 | ENG | @1 Modeling sharing and recursion for weak reduction strategies using explicit substitution |
|---|
| A09 | 01 | 1 | ENG | @1 PLILP '96 : programming languages : implementations, logics, and programs : Aachen, September 24-27, 1996 |
|---|
| A11 | 01 | 1 | | @1 BENAISSA (Z.-E.-A.) |
|---|
| A11 | 02 | 1 | | @1 LESCANNE (P.) |
|---|
| A11 | 03 | 1 | | @1 ROSE (K. H.) |
|---|
| A12 | 01 | 1 | | @1 KUCHEN (Herbert) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 SWIERSTRA (S. Doaitse) @9 ed. |
|---|
| A14 | 01 | | | @1 INRIA Lorraine & CRIN @2 Nancy @3 FRA @Z 1 aut. @Z 2 aut. |
|---|
| A14 | 02 | | | @1 BRICSD, Aarhus University @3 DNK @Z 3 aut. |
|---|
| A20 | | | | @1 393-407 |
|---|
| A21 | | | | @1 1996 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000063989040270 |
|---|
| A44 | | | | @0 0000 @1 © 1997 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 16 ref. |
|---|
| A47 | 01 | 1 | | @0 97-0023506 |
|---|
| 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 We present the λσwa-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how λσwa can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely weak reduction strategies, recursion, space leaks, recursive data structures, and parallel evaluation. We use λσwa to give a unified model of several computational aspects. First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing λ-graph-reduction vs. environment-based evaluation. Second, we show how to add constructors and explicit recursion to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of space leaks in λσwa and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the "trimming" performed by the STG machine does not leak space. In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages. |
|---|
| C02 | 01 | X | | @0 001D02B09 |
|---|
| C02 | 02 | X | | @0 001D02A05 |
|---|
| C02 | 03 | X | | @0 001D02B03 |
|---|
| C03 | 01 | X | FRE | @0 Modélisation @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Modeling @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Modelización @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Partage @5 02 |
|---|
| C03 | 02 | X | ENG | @0 Sharing @5 02 |
|---|
| C03 | 02 | X | SPA | @0 Partición @5 02 |
|---|
| C03 | 03 | X | FRE | @0 Récursivité @5 03 |
|---|
| C03 | 03 | X | ENG | @0 Recursivity @5 03 |
|---|
| C03 | 03 | X | SPA | @0 Recursividad @5 03 |
|---|
| C03 | 04 | X | FRE | @0 Fonction récursive @5 04 |
|---|
| C03 | 04 | X | ENG | @0 Recursive function @5 04 |
|---|
| C03 | 04 | X | SPA | @0 Función recursiva @5 04 |
|---|
| C03 | 05 | X | FRE | @0 Programmation fonctionnelle @5 05 |
|---|
| C03 | 05 | X | ENG | @0 Functional programming @5 05 |
|---|
| C03 | 05 | X | SPA | @0 Programación funcional @5 05 |
|---|
| C03 | 06 | X | FRE | @0 Lambda calcul @5 06 |
|---|
| C03 | 06 | X | ENG | @0 Lambda calculus @5 06 |
|---|
| C03 | 06 | X | SPA | @0 Lambda cálculo @5 06 |
|---|
| C03 | 07 | X | FRE | @0 Substitution @5 07 |
|---|
| C03 | 07 | X | ENG | @0 Substitution @5 07 |
|---|
| C03 | 07 | X | GER | @0 Substitution @5 07 |
|---|
| C03 | 07 | X | SPA | @0 Substitución @5 07 |
|---|
| N21 | | | | @1 006 |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 Programming languages : implementations, logics, and programs. International symposium @2 8 @3 Aachen DEU @4 1996-09-24 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 97-0023506 INIST |
|---|
| ET : | Modeling sharing and recursion for weak reduction strategies using explicit substitution |
|---|
| AU : | BENAISSA (Z.-E.-A.); LESCANNE (P.); ROSE (K. H.); KUCHEN (Herbert); SWIERSTRA (S. Doaitse) |
|---|
| AF : | INRIA Lorraine & CRIN/Nancy/France (1 aut., 2 aut.); BRICSD, Aarhus University/Danemark (3 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1996; Vol. 1140; Pp. 393-407; Bibl. 16 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | We present the λσwa-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how λσwa can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely weak reduction strategies, recursion, space leaks, recursive data structures, and parallel evaluation. We use λσwa to give a unified model of several computational aspects. First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing λ-graph-reduction vs. environment-based evaluation. Second, we show how to add constructors and explicit recursion to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of space leaks in λσwa and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the "trimming" performed by the STG machine does not leak space. In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages. |
|---|
| CC : | 001D02B09; 001D02A05; 001D02B03 |
|---|
| FD : | Modélisation; Partage; Récursivité; Fonction récursive; Programmation fonctionnelle; Lambda calcul; Substitution |
|---|
| ED : | Modeling; Sharing; Recursivity; Recursive function; Functional programming; Lambda calculus; Substitution |
|---|
| GD : | Substitution |
|---|
| SD : | Modelización; Partición; Recursividad; Función recursiva; Programación funcional; Lambda cálculo; Substitución |
|---|
| LO : | INIST-16343.354000063989040270 |
|---|
| ID : | 97-0023506 |
|---|
Links to Exploration step
Pascal:97-0023506
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Modeling sharing and recursion for weak reduction strategies using explicit substitution</title>
<author><name sortKey="Benaissa, Z E A" sort="Benaissa, Z E A" uniqKey="Benaissa Z" first="Z.-E.-A." last="Benaissa">Z.-E.-A. Benaissa</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA Lorraine & CRIN</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Lescanne, P" sort="Lescanne, P" uniqKey="Lescanne P" first="P." last="Lescanne">P. Lescanne</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA Lorraine & CRIN</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Rose, K H" sort="Rose, K H" uniqKey="Rose K" first="K. H." last="Rose">K. H. Rose</name>
<affiliation><inist:fA14 i1="02"><s1>BRICSD, Aarhus University</s1>
<s3>DNK</s3>
<sZ>3 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">97-0023506</idno>
<date when="1996">1996</date>
<idno type="stanalyst">PASCAL 97-0023506 INIST</idno>
<idno type="RBID">Pascal:97-0023506</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000C95</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Modeling sharing and recursion for weak reduction strategies using explicit substitution</title>
<author><name sortKey="Benaissa, Z E A" sort="Benaissa, Z E A" uniqKey="Benaissa Z" first="Z.-E.-A." last="Benaissa">Z.-E.-A. Benaissa</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA Lorraine & CRIN</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Lescanne, P" sort="Lescanne, P" uniqKey="Lescanne P" first="P." last="Lescanne">P. Lescanne</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA Lorraine & CRIN</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Rose, K H" sort="Rose, K H" uniqKey="Rose K" first="K. H." last="Rose">K. H. Rose</name>
<affiliation><inist:fA14 i1="02"><s1>BRICSD, Aarhus University</s1>
<s3>DNK</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="1996">1996</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>Functional programming</term>
<term>Lambda calculus</term>
<term>Modeling</term>
<term>Recursive function</term>
<term>Recursivity</term>
<term>Sharing</term>
<term>Substitution</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Modélisation</term>
<term>Partage</term>
<term>Récursivité</term>
<term>Fonction récursive</term>
<term>Programmation fonctionnelle</term>
<term>Lambda calcul</term>
<term>Substitution</term>
</keywords><front><div type="abstract" xml:lang="en">We present the λσ<sub>w</sub>
<sup>a</sup>
-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how λσ<sub>w</sub>
<sup>a</sup>
can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely weak reduction strategies, recursion, space leaks, recursive data structures, and parallel evaluation. We use λσ<sub>w</sub>
<sup>a</sup>
to give a unified model of several computational aspects. First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing λ-graph-reduction vs. environment-based evaluation. Second, we show how to add constructors and explicit recursion to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of space leaks in λσ<sub>w</sub>
<sup>a</sup>
and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the "trimming" performed by the STG machine does not leak space. In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages.</div><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>1140</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Modeling sharing and recursion for weak reduction strategies using explicit substitution</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>PLILP '96 : programming languages : implementations, logics, and programs : Aachen, September 24-27, 1996</s1>
</fA09><fA11 i1="01" i2="1"><s1>BENAISSA (Z.-E.-A.)</s1>
</fA11><fA11 i1="02" i2="1"><s1>LESCANNE (P.)</s1>
</fA11><fA11 i1="03" i2="1"><s1>ROSE (K. H.)</s1>
</fA11><fA12 i1="01" i2="1"><s1>KUCHEN (Herbert)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>SWIERSTRA (S. Doaitse)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>INRIA Lorraine & CRIN</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</fA14><fA14 i1="02"><s1>BRICSD, Aarhus University</s1>
<s3>DNK</s3>
<sZ>3 aut.</sZ>
</fA14><fA20><s1>393-407</s1>
</fA20><fA21><s1>1996</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000063989040270</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 1997 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>16 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>97-0023506</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>We present the λσ<sub>w</sub>
<sup>a</sup>
-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how λσ<sub>w</sub>
<sup>a</sup>
can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely weak reduction strategies, recursion, space leaks, recursive data structures, and parallel evaluation. We use λσ<sub>w</sub>
<sup>a</sup>
to give a unified model of several computational aspects. First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing λ-graph-reduction vs. environment-based evaluation. Second, we show how to add constructors and explicit recursion to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of space leaks in λσ<sub>w</sub>
<sup>a</sup>
and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the "trimming" performed by the STG machine does not leak space. In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages.</s0><fC02 i1="01" i2="X"><s0>001D02B09</s0>
</fC02><fC02 i1="02" i2="X"><s0>001D02A05</s0>
</fC02><fC02 i1="03" i2="X"><s0>001D02B03</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Modélisation</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Modeling</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Modelización</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Partage</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Sharing</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Partición</s0>
<s5>02</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Récursivité</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Recursivity</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Recursividad</s0>
<s5>03</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Fonction récursive</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Recursive function</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Función recursiva</s0>
<s5>04</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Programmation fonctionnelle</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Functional programming</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Programación funcional</s0>
<s5>05</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Lambda calcul</s0>
<s5>06</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Lambda calculus</s0>
<s5>06</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Lambda cálculo</s0>
<s5>06</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Substitution</s0>
<s5>07</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Substitution</s0>
<s5>07</s5>
</fC03><fC03 i1="07" i2="X" l="GER"><s0>Substitution</s0>
<s5>07</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Substitución</s0>
<s5>07</s5>
</fC03><fN21><s1>006</s1>
</fN21><pR><fA30 i1="01" i2="1" l="ENG"><s1>Programming languages : implementations, logics, and programs. International symposium</s1>
<s2>8</s2>
<s3>Aachen DEU</s3>
<s4>1996-09-24</s4>
</fA30><server><NO>PASCAL 97-0023506 INIST</NO>
<ET>Modeling sharing and recursion for weak reduction strategies using explicit substitution</ET>
<AU>BENAISSA (Z.-E.-A.); LESCANNE (P.); ROSE (K. H.); KUCHEN (Herbert); SWIERSTRA (S. Doaitse)</AU>
<AF>INRIA Lorraine & CRIN/Nancy/France (1 aut., 2 aut.); BRICSD, Aarhus University/Danemark (3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1996; Vol. 1140; Pp. 393-407; Bibl. 16 ref.</SO>
<LA>Anglais</LA>
<EA>We present the λσ<sub>w</sub>
<sup>a</sup>
-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how λσ<sub>w</sub>
<sup>a</sup>
can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely weak reduction strategies, recursion, space leaks, recursive data structures, and parallel evaluation. We use λσ<sub>w</sub>
<sup>a</sup>
to give a unified model of several computational aspects. First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing λ-graph-reduction vs. environment-based evaluation. Second, we show how to add constructors and explicit recursion to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of space leaks in λσ<sub>w</sub>
<sup>a</sup>
and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the "trimming" performed by the STG machine does not leak space. In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages.</EA><CC>001D02B09; 001D02A05; 001D02B03</CC>
<FD>Modélisation; Partage; Récursivité; Fonction récursive; Programmation fonctionnelle; Lambda calcul; Substitution</FD>
<ED>Modeling; Sharing; Recursivity; Recursive function; Functional programming; Lambda calculus; Substitution</ED>
<GD>Substitution</GD>
<SD>Modelización; Partición; Recursividad; Función recursiva; Programación funcional; Lambda cálculo; Substitución</SD>
<LO>INIST-16343.354000063989040270</LO>
<ID>97-0023506</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 000C95 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000C95 | 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:97-0023506
|texte= Modeling sharing and recursion for weak reduction strategies using explicit substitution
}}
| 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 |  |
