Confluence of extensional and non-extensional λ-calculi with explicit substitutions
Identifieur interne : 009D57 ( Main/Exploration ); précédent : 009D56; suivant : 009D58Confluence of extensional and non-extensional λ-calculi with explicit substitutions
Auteurs : Delia Kesner [France]Source :
- Theoretical Computer Science [ 0304-3975 ] ; 2000.
English descriptors
- Teeft :
- Basic conditions, Basic substitution calculus, Beta, Beta rule, Bruijn, Calculus, Cient, Clos, Closure, Combinatory reduction systems, Computer science, Conditional rule, Conf, Curien, Erent, Expansion rule, Explicit substitutions, Extensional, Free variables, Functional programming, Fvarlift1, Generalized interpretation method, Hardin, Induction hypothesis, Internat, Interpretation method, Kesner, Lambda, Lambda calculi, Lecture notes, Liftn, Natural number, Natural numbers, Normal form, Normal forms, Normalization, Open terms, Proc, Pure term, Pure terms, Reduction relation, Reduction rule, Reduction rules, Resp, Same time, Shiftcons, Springer, Strong normalization, Substitution, Substitution calculus, Substitution language, Substitution signature, Uence, Uent, Universit.
Abstract
Abstract: This paper studies confluence of extensional and non-extensional λ-calculi with explicit substitutions, where extensionality is interpreted by η-expansion. For that, we propose a scheme for explicit substitutions which describes those abstract properties that are sufficient to guarantee confluence. Our method makes it possible to treat at the same time many well-known calculi such as λσ,λσ⇑,λφ,λs,λv,λf,λd and λdn.
Url:
DOI: 10.1016/S0304-3975(98)00166-2
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002B00
- to stream Istex, to step Curation: 002A63
- to stream Istex, to step Checkpoint: 002010
- to stream Main, to step Merge: 00A338
- to stream Main, to step Curation: 009D57
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Confluence of extensional and non-extensional λ-calculi with explicit substitutions</title><author><name sortKey="Kesner, Delia" sort="Kesner, Delia" uniqKey="Kesner D" first="Delia" last="Kesner">Delia Kesner</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B5E008CDB904067980D3A92F42F66EF5FAF00277</idno><date when="2000" year="2000">2000</date><idno type="doi">10.1016/S0304-3975(98)00166-2</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-MVBHBTR6-R/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002B00</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002B00</idno><idno type="wicri:Area/Istex/Curation">002A63</idno><idno type="wicri:Area/Istex/Checkpoint">002010</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002010</idno><idno type="wicri:doubleKey">0304-3975:2000:Kesner D:confluence:of:extensional</idno><idno type="wicri:Area/Main/Merge">00A338</idno><idno type="wicri:Area/Main/Curation">009D57</idno><idno type="wicri:Area/Main/Exploration">009D57</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">Confluence of extensional and non-extensional λ-calculi with explicit substitutions</title><author><name sortKey="Kesner, Delia" sort="Kesner, Delia" uniqKey="Kesner D" first="Delia" last="Kesner">Delia Kesner</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Univ. de Paris-Sud (Paris XI), Centre de Orsay, Lab. de Recherche en Informatique, CNRS U.R.a. 410, Bât. 490, F-91405 Orsay Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Orsay</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Theoretical Computer Science</title><title level="j" type="abbrev">TCS</title><idno type="ISSN">0304-3975</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="2000">2000</date><biblScope unit="volume">238</biblScope><biblScope unit="issue">1–2</biblScope><biblScope unit="page" from="183">183</biblScope><biblScope unit="page" to="220">220</biblScope></imprint><idno type="ISSN">0304-3975</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0304-3975</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Basic conditions</term><term>Basic substitution calculus</term><term>Beta</term><term>Beta rule</term><term>Bruijn</term><term>Calculus</term><term>Cient</term><term>Clos</term><term>Closure</term><term>Combinatory reduction systems</term><term>Computer science</term><term>Conditional rule</term><term>Conf</term><term>Curien</term><term>Erent</term><term>Expansion rule</term><term>Explicit substitutions</term><term>Extensional</term><term>Free variables</term><term>Functional programming</term><term>Fvarlift1</term><term>Generalized interpretation method</term><term>Hardin</term><term>Induction hypothesis</term><term>Internat</term><term>Interpretation method</term><term>Kesner</term><term>Lambda</term><term>Lambda calculi</term><term>Lecture notes</term><term>Liftn</term><term>Natural number</term><term>Natural numbers</term><term>Normal form</term><term>Normal forms</term><term>Normalization</term><term>Open terms</term><term>Proc</term><term>Pure term</term><term>Pure terms</term><term>Reduction relation</term><term>Reduction rule</term><term>Reduction rules</term><term>Resp</term><term>Same time</term><term>Shiftcons</term><term>Springer</term><term>Strong normalization</term><term>Substitution</term><term>Substitution calculus</term><term>Substitution language</term><term>Substitution signature</term><term>Uence</term><term>Uent</term><term>Universit</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper studies confluence of extensional and non-extensional λ-calculi with explicit substitutions, where extensionality is interpreted by η-expansion. For that, we propose a scheme for explicit substitutions which describes those abstract properties that are sufficient to guarantee confluence. Our method makes it possible to treat at the same time many well-known calculi such as λσ,λσ⇑,λφ,λs,λv,λf,λd and λdn.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Île-de-France</li></region><settlement><li>Orsay</li></settlement></list><tree><country name="France"><region name="Île-de-France"><name sortKey="Kesner, Delia" sort="Kesner, Delia" uniqKey="Kesner D" first="Delia" last="Kesner">Delia Kesner</name></region><name sortKey="Kesner, Delia" sort="Kesner, Delia" uniqKey="Kesner D" first="Delia" last="Kesner">Delia Kesner</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 009D57 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 009D57 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:B5E008CDB904067980D3A92F42F66EF5FAF00277
|texte= Confluence of extensional and non-extensional λ-calculi with explicit substitutions
}}
| This area was generated with Dilib version V0.6.33. |  |