Sur l'$\eta$-expansion infinie

Curien, Pierre-Louis

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

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 : $𝒜{\widehat{⪯}}_{\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: $𝒜{\widehat{⪯}}_{\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.

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

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

[3] Hyland, M. 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] Nakajima, R. Infinite normal forms for the λ-calculus, Proc. Symposium on λ-Calculus and Computer Science, Roma, Lect. Notes in Comput. Sci., 37, Springer-Verlag, 1975

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

[7] Wadsworth, C. 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