Sur l'$ \mathbf{\eta }$-expansion infinie

Pierre-Louis Curien

doi:10.1016/S1631-073X(02)02095-2

Sur l'

η

-expansion infinie

Pierre-Louis Curien ¹

¹ PPS, case 7014, CNRS & Université Paris-7, 2, place Jussieu, 75251 Paris cedex 05, France

Comptes Rendus. Mathématique, Volume 334 (2002) no. 1, pp. 77-82.

Résumé
Abstract

Nous donons deux caractérisations de l'ordre sur les arbres de Böhm induit par le modèle D_∞, dont l'une est nouvelle et formalise une propriété de continuité de l'η-expansion infinie : $𝒜 {\hat{⪯}}_{\infty} ℬ$ si pour tout approximant fini A de $𝒜$ , il existe un approximant fini B de $ℬ$ tel que A est un sous-arbre de B, modulo une η-égalité finie et modulo un nombre fini d'η-expansions infinies de variables.

We give two characterizations of the ordering on Böhm trees induced by the D_∞ model, one of which formalizes a continuity property of infinite η-expansion: $𝒜 {\hat{⪯}}_{\infty} ℬ$ if for any finite approximant A of $𝒜$ there exists a finite approximant B of $ℬ$ such that A is a sub-tree of B, modulo finitely many η-equalities and finitely many infinite η-expansions of variables.

Reçu le : 2001-07-17
Accepté le : 2001-07-28
Publié le : 2002-01-01

DOI : 10.1016/S1631-073X(02)02095-2

Affiliations des auteurs :

Pierre-Louis Curien ¹

¹ PPS, case 7014, CNRS & Université Paris-7, 2, place Jussieu, 75251 Paris cedex 05, France

@article{CRMATH_2002__334_1_77_0,
     author = {Pierre-Louis Curien},
     title = {Sur l'$ \mathbf{\eta }$-expansion infinie},
     journal = {Comptes Rendus. Math\'ematique},
     pages = {77--82},
     publisher = {Elsevier},
     volume = {334},
     number = {1},
     year = {2002},
     doi = {10.1016/S1631-073X(02)02095-2},
     language = {fr},
}

TY  - JOUR
AU  - Pierre-Louis Curien
TI  - Sur l'$ \mathbf{\eta }$-expansion infinie
JO  - Comptes Rendus. Mathématique
PY  - 2002
SP  - 77
EP  - 82
VL  - 334
IS  - 1
PB  - Elsevier
DO  - 10.1016/S1631-073X(02)02095-2
LA  - fr
ID  - CRMATH_2002__334_1_77_0
ER  -

%0 Journal Article
%A Pierre-Louis Curien
%T Sur l'$ \mathbf{\eta }$-expansion infinie
%J Comptes Rendus. Mathématique
%D 2002
%P 77-82
%V 334
%N 1
%I Elsevier
%R 10.1016/S1631-073X(02)02095-2
%G fr
%F CRMATH_2002__334_1_77_0

Pierre-Louis Curien. Sur l'$ \mathbf{\eta }$-expansion infinie. Comptes Rendus. Mathématique, Volume 334 (2002) no. 1, pp. 77-82. doi : 10.1016/S1631-073X(02)02095-2. https://comptes-rendus.academie-sciences.fr/mathematique/articles/10.1016/S1631-073X(02)02095-2/

Bibliographie
Cité par

[1] R. Amadio; P.-L. Curien Domains and Lambda-Calculi, Cambridge University Press, 1998

[2] H. Barendregt The Lambda Calculus; Its Syntax and Semantics, North-Holland, 1984

[3] M. Hyland A syntactic characterization of the equality in some models of lambda calculus, J. London Math. Soc., Volume 2 (1976), pp. 361-370

[4] Lévy J.-J., Propriétés syntaxiques du λ-Calcul, Rapport Technique LITP 79-11, Université Paris-7, 1979

[5] R. Nakajima Infinite normal forms for the λ-calculus, Proc. Symposium on λ-Calculus and Computer Science, Roma, Lect. Notes in Comput. Sci., 37, Springer-Verlag, 1975

[6] S. Ronchi della Rocca Basic lambda-calculus, Course Notes for a Summer School in Chambéry, 1996

[7] C. Wadsworth The relation between computational and denotational properties for Scott's D-infinity models of the lambda-calculus, SIAM J. Comput., Volume 5 (1976), pp. 488-521

Pierre-Louis Curien Definability and full abstraction, Computation, meaning, and logic. Articles dedicated to Gordon Plotkin., Amsterdam: Elsevier, 2007, pp. 301-310 | DOI:10.1016/j.entcs.2007.02.011 | Zbl:1277.68120
Mariangiola Dezani-Ciancaglini; Elio Giovannetti From Böhm's Theorem to Observational Equivalences, Electronic Notes in Theoretical Computer Science, Volume 50 (2001) no. 2, p. 83 | DOI:10.1016/s1571-0661(04)00167-7

Cité par 2 documents. Sources : Crossref, zbMATH

Commentaires - Politique