Sur l’η-expansion infinie

Pierre-Louis Curien (CNRS – Université Paris 7)

July 1, 2000

1 Introduction

Dans cette note, nous analysons et comparons plusieurs caractérisations de l’ordre sur les arbres de Böhm correspondant au modèle D_{∞} de Scott. Nous montrons un tableau d’équivalences

M ≤_{obs} N  ⇐  [[M]] ≤ [[N]]
⇓  ⇑
BT (M) ⪯_{∞}^{J} BT (N) ⇔ BT (M) ⪯_{∞} BT (N) ⇒ BT (M) ˆ⪯_{∞}BT (N)

A la première ligne de ce tableau et à gauche, on trouve l’ordre observationnel: M ≤_{obs} N signifie que N passe tous les tests que M passe, un test positif consistant à plonger le terme observé dans un contexte donné et à calculer le tout jusqu’à obtention d’une forme normale de tête. A la première ligne et à droite, on trouve l’ordre dans le modèle D_{∞}. Nous utilisons ici la version “logique” du modèle D_{∞}, pour laquelle [[M]] ≤ [[N]] signifie que tout type de M est aussi un type de N.

Les trois symboles ⪯_{∞}^{J}, ⪯_{∞} et ˆ⪯_{∞} désignent tous les trois le même ordre. La première formulation ⪯_{∞} est proche des définitions utilisées par Nakajima, Wadsworth, Hyland, Barendregt et Lévy (voir section 6). La définiton de ⪯_{∞}^{J}, qui est une contribution de cette note (section 5), est en termes de jeux. Informellement, si A_{1} et A_{2} sont des arbres de Böhm, A_{1} ⪯_{∞}^{J} A_{2} si A_{2} bat tout adversaire fini que A_{1} bat, et le bat de la même manière. Ici, “battre” veut dire “ne pas être plus petit modulo un nombre fini d’η-égalités”, et “de la même manière” veut dire que la différence observée est localisée au même endroit (en termes de jeux, la partie qui se déroule est identique si l’on remplace A_{1} par A_{2}).

Notre principale contribution est concentrée dans la définition de ˆ⪯_{∞} (et la preuve de l’implication de la seconde ligne tu tableau), qui formalise une propriété de continuité de l’η-expansion infinie. Informellement, si A et B sont des arbres de Böhm, A ˆ⪯_{∞}B si pour tout approximant fini A de A, il existe un approximant fini B de B tel que A est un sous-arbre de B, modulo une η-égalité finie et modulo un nombre fini d’η-expansions infinies de variables.

2 λ-calcul et types avec intersections (rappels)

On renvoie à [Barendregt84] pour les définitions de base du λ-calcul. On rappelle seulement ici qu’un λ-terme a l’une des deux formes suivantes:

\begin{matrix}M = λx_{1} ⋯ x_{m}.(λx.M_{0})M_{1} ⋯ M_{n} & (n ≥ 1) \\ M = λx_{1} ⋯ x_{m}.xM_{1} ⋯ M_{n} & (n ≥ 0) . \end{matrix}

Dans le second cas, on dit que M est une forme normale de tête (fnt). On note FV (M) l’ensemble des variables libres de M. On rappelle aussi les axiomes de β et η-réduction:

(β) (λx.M)N →_{β} M[x ← N]
(η) λx.Mx →_{η} M  (si x n’est pas libre dans M)

On dit que M a une fnt s’il existe une fnt N telle que M →_{β}^{⋆} N, i.e., M se réduit sur N en un nombre k ≥ 0 d’étapes de (fermeture par congruence de) β. Un approximant est un terme A écrit avec la syntaxe suivante:

A ::= Ω || λx_{1} ⋯ x_{m}.xA_{1} ⋯ A_{n} (m ≥ 0, n ≥ 0) .

Si u est une suite d’entiers naturels strictement positifs, on définit A/u, quand il existe, par (ϵ étant la suite vide): A/ϵ = A et λx_{1} ⋯ x_{m}.xA_{1} ⋯ A_{n}/iu = A_{i}/u si i ≤ n; et on dit que l’occurrence u est définie dans A. Si A ≤ B, A/u = Ω et B/u ≠ Ω, on écrit A <_{u} B. On note |u| la longueur d’une occurrence u.

On ordonne les approximants comme suit: Ω est le plus petit approximant, et λx_{1} ⋯ x_{m}.xA_{1} ⋯ A_{n} ≤ B si et seulement si B = λx_{1} ⋯ x_{m}.xB_{1} ⋯ B_{n}, où A_{i} ≤ B_{i} pour tout i. (On considèrera aussi une autre relation entre approximants dans la section 3.). La complétion par idéaux de l’ensemble des approximants est un ensemble d’arbres finis et infinis, appelès arbres de Böhm. On garde les lettres A, B, … pours les arbres finis, et on utilise A, B, … pour les arbres finis ou infinis. On peut étendre la notation A/u aux arbres infinis comme suit: A/u est défini si et seulement s’il existe A ≤ A tel que A/u est défini, et A/u est la borne supérieure de {A/u | A/u est défini et A ≤ A}.

L’approximation immédiate ω(M) d’un terme M est définie comme suit:

\begin{matrix}ω(λx_{1} ⋯ x_{m}.(λx.M_{0})M_{1} ⋯ M_{n}) = Ω \\ ω(λx_{1} ⋯ x_{m}.xM_{1} ⋯ M_{n}) = λx_{1} ⋯ x_{m}.xω(M_{1}) ⋯ ω(M_{n}) . \end{matrix}

L’arbre de Böhm BT (M) d’un terme M est l’arbre éventuellement infini borne supérieure dirigée de {ω(N) | M →_{β}^{⋆} N}. Un contexte est un terme C construit avec une constante supplémentaire [ ]. On note C[M] le résultat du remplacement de toutes les occurrences de [ ] par M (ces remplacements peuvent capturer des variables, i.e., transformer des variables libres en variables liées, par exemple, si C = λx.[ ], alors C[x] = λx.x). Les contextes et les arbres de Böhm commutent:

Théorème 2.1 (de continuité syntaxique [Welch75, Lévy76]) Pour tout terme M et pour tout contexte C, si B ≤ BT (C[M]), alors il existe A ≤ BT (M) tel que B ≤ BT (C[A]) (c’est-à-dire: il existe N tel que C[A] →_{β}^{⋆} N et B ≤ ω(N)).

Preuve (indication). On peut montrer que si C[M] →_{β}^{⋆} N, alors il existe P tel que C[M] →_{β}^{⋆} C[P] et C[P] →_{β}^{⋆} N où la dernière réduction ne réduit jamais de (résidu de) radical de P. Donc cette réduction se fait essentiellement à partir de C[ω(P)]. Voir par exemple [Amadio+98, section 2.3] pour une preuve détaillée. □

On rappelle maintenant les notions de types avec intersection (originellement introduits en 1978 par Sallé). On renvoie pour plus de détails à [Coppo+84], [Krivine91] ou [Amadio+98, chapitre 3]. On considère la syntaxe de types suivante:

σ ::= κ || ω || σ_{1} ∧ σ_{2} || σ_{1} → σ_{2} .

Le système suivant spécifie un ordre sur les types.

σ ≤ σ σ ≤ ω \begin{matrix}σ_{1} ≤ σ_{2} σ_{2} ≤ σ_{3} \\ σ_{1} ≤ σ_{3} \end{matrix}

σ ∧ τ ≤ σ σ ∧ τ ≤ τ σ ≤ σ ∧ σ \begin{matrix}σ ≤ σ′ τ ≤ τ′ \\ (σ ∧ τ) ≤ (σ′ ∧ τ′) \end{matrix}

.

(σ → τ_{1}) ∧ (σ → τ_{2}) ≤ σ → (τ_{1} ∧ τ_{2}) \begin{matrix}σ′ ≤ σ τ ≤ τ′ \\ (σ → τ) ≤ (σ′ → τ′) \end{matrix}
ω ≤ ω → ω κ ≤ ω → κ ω → κ ≤ κ

On définit ensuite des règles de typage comme suit:

\begin{matrix}x : σ ∈ Γ \\ Γ ⊢ x : σ \end{matrix}  \begin{matrix}Γ ⊢ M : σ → τ Γ ⊢ N : σ \\ Γ ⊢ MN : τ \end{matrix} \begin{matrix}Γ, x : σ ⊢ M : τ \\ Γ ⊢ λx.M : σ → τ \end{matrix}

Γ ⊢ M : ω \begin{matrix}Γ ⊢ M : σ Γ ⊢ M : τ \\ Γ ⊢ M : σ ∧ τ \end{matrix}  \begin{matrix}Γ ⊢ M : σ σ ≤ τ \\ Γ ⊢ M : τ \end{matrix}

On pose [[M]] ≤ [[N]] si

∀ Γ, σ (Γ ⊢ M : σ ⇒ Γ ⊢ N : σ) .

Nous renvoyons à [Coppo+84] et [Amadio+98, chapitre 3] pour une preuve de ce que le modèle ainsi construit est isomorphe au modèle D_{∞} construit comme limite de la suite D_{0} = {⊥, ⊤}, …, D_{n+1} = D_{n} → D_{n}, …, définie dans une catégorie de fonctions appropriées appelées plongements ou paires d’injection-projection (le plongement initial étant λxy.x : D_{0} → D_{1}). Les types σ représentent les éléments compacts de D_{∞}.

Théorème 2.2 (des approximations) Si Γ ⊢ M : σ, alors il existe A ≤ BT (M) tel que Γ ⊢ A : σ.

Ce théorème peut se montrer par la technique de réalisabilité ou calculabilité [Ronchi96] (voir aussi [Amadio+98, exercice 3.5.19]).

Proposition 2.3 Un terme clos (i.e., sans variables libres) M a une fnt si et seulement si M a un type non trivial, i.e., un type σ tel que ω ≤ σ n’est pas prouvable.

Preuve. Si M a un type σ non trivial, alors par le théorème 2.2 il existe un approximant A ≤ BT (M) de type non trivial. Comme Ω ne peut être typé que par un type ≥ ω (il n’y a aucune règle de typage spécifique pour Ω), A est différent de Ω. Soit N tel que M →_{β}^{⋆} N et A ≤ ω(N). Alors a fortiori N est une fnt. Donc M a une fnt. Réciproquement, il est facile de voir que toute fnt close a un type non trivial (par exemple κ). On conclut grâce à la propriété suivante, qui se démontre sans difficulté: si Γ ⊢ N : σ et si M →_{β} N, alors Γ ⊢ M : σ. □

3 Semi-séparation d’approximants finis

On définit un préordre sur les approximants:

Ω ⪯ A \begin{matrix}x = y m = n A_{1} ⪯ B_{1} ⋯ A_{n} ⪯ B_{n} \\ xA_{1} ⋯ A_{m} ⪯ yB_{1} ⋯ B_{n} \end{matrix}  \begin{matrix}A ⪯ B \\ λx.A ⪯ λx.B \end{matrix}

\begin{matrix}A ⪯ yB_{1} ⋯ B_{n}x x ∉ FV (yB_{1} ⋯ B_{n}) \\ λx.A ⪯ yB_{1} ⋯ B_{n} \end{matrix} \begin{matrix}yB_{1} ⋯ B_{n}x ⪯ A x ∉ FV (yB_{1} ⋯ B_{n}) \\ yB_{1} ⋯ B_{n} ⪯ λx.A \end{matrix}

Si on a établi A ⪯ B sans l’aide des deux dernières règles, on retrouve A ≤ B. Notons qu’il n’est pas immédiat d’après la définition ci-dessus que ⪯ est transitive. Cela se montre par récurrence (sur la taille des preuves) et par cas (élimination des coupures). La bonne fondation de la définition est immédiate par récurrence sur la notion de taille suivante: taille(x) = taille(Ω) = 0, taille(λx.A) = taille(A)+1 et taille(xA_{1} ⋯ A_{n}) = Σ_{i=1}^{i=n}taille(A_{i}) + 1 (n ≥ 1).

Remarque 3.1 Si l’on a établi A ⪯ B sans l’aide de la première règle, i.e., si A ⪯ B et A est un λ-terme (sans occurrences d’Ω), alors A =_{η} B, et B est aussi un λ-terme. Si A = x, on a même B →_{η}^{⋆} x.

La négation de l’ordre que nous venons de définir peut être spécifiée comme suit,

λx_{1} ⋯ x_{n}xA_{1} ⋯ A_{m} ⪯̸_{ϵ,f} Ω

\begin{matrix}A ⪯̸_{u,△} B \\ λx.A ⪯̸_{u,△} λx.B \end{matrix} \begin{matrix}A ⪯̸_{u,△} yB_{1} ⋯ B_{n}x \\ λx.A ⪯̸_{u,△} yB_{1} ⋯ B_{n} \end{matrix}  \begin{matrix}yB_{1} ⋯ B_{n}x ⪯̸_{u,△} A \\ yB_{1} ⋯ B_{n} ⪯̸_{u,△} λx.A \end{matrix}

(x ≠ y) xA_{1} ⋯ A_{m} ⪯̸_{ϵ,r} yB_{1} ⋯ B_{n}  (m ≠ n) xA_{1} ⋯ A_{m} ⪯̸_{ϵ,r} xB_{1} ⋯ B_{n}

\begin{matrix}A_{j} ⪯̸_{u,△} B_{j} \\ xA_{1} ⋯ A_{m} ⪯̸_{ju,△} xB_{1} ⋯ B_{m} \end{matrix}

Les décorations u et △ fournissant des indications utiles: u désigne l’occurrence commune à (l’expansion de) A et (l’expansion de) B où la différence est observée, et △ est une marque f ou r (voir remarque 3.5 pour la signification de ces lettres).

Proposition 3.2 Pour tous A, B, on a A ⪯̸ B si et seulement il existe u tel que A ⪯̸_{u,△} B. De plus, si A ⪯̸_{u,△} B et A ⪯ A′, alors A′ ⪯̸_{u,△} B.

Preuve. La première partie de l’ènoncé est conséquence de l’observation suivante. Chacune des règles définissant ⪯ peut se lire à l’envers, puisque pour un coupe donné A, B, selon la forme de A et de B, au plus une des règles peut s’appliquer. Par exemple, si xA_{!} ⋯ A_{m} ⪯̸ yB_{1} ⋯ B_{n}, c’est aue x ≠ y, ou x = y et m ≠ n, ou x = y, m = n et (∃ j A_{j} ⪯̸ B_{j}): on retrouve les trois dernières règles ci-dessus. Les décorations u, Δ en indice ne font que noter des informations, elles n’affectent pas la dérivabilité de A ⪯̸ B. La seconde partie de l’ènoncè se montre par récurrence sur la taille de la preuve de A ⪯̸_{u,△} B, en regroupant les trois règles qui concernent λ. □

Lemme 3.3 Pour tous A, B, si A ⪯̸_{u,△} B, alors A/u est défini ou B/u est défini.

Preuve. Le passage de u à ju se fait via la dernière règle, précédée d’un nombre adéquat d’applications des deuxième, troisième et quatrième règles, qui permettent de passer d’un couple de termes

λx_{1} ⋯ x_{m}.xA_{1} ⋯ A_{n}, λx_{1} ⋯ x_{p}.xB_{1} ⋯ B_{q}

tels que m−n = p−q et, disons m ≤ p, au couple de termes xA_{1} ⋯ A_{n}x_{m+1} ⋯ x_{p}, xB_{1} ⋯ B_{q}. On a alors j ≤ q. Et symétriquement, si p ≤ m, alors j ≤ n. □

On définit un système formel pour la déduction d’expressions A , B ⟹^{u,△} C qui construit un contexte C associé à deux approximants A, B tels que A ⪯̸_{u,△} B. Ce système, tiré de [Ronchi96], formalise la technique de semi-séparation dûe à Wadsworth [Wadsworth76] (et aussi Hyland [Hyland76], indépendamment), et adaptée de la technique de séparation de Böhm [Böhm68]. On pose:

π_{n}^{m} = λx_{1} ⋯ x_{m}.x_{n} (n ≤ m) α_{n} = λz_{1} ⋯ z_{n}z.zz_{1} ⋯ z_{n} .

On utilise une syntaxe adaptée pour les contextes: ce sont des listes dont chaque élément est une variable ou une substitution [M/x]. La correspondance avec les contextes habituels est donnée par:

xC  C[[ ]x]  (“appliquer à x, puis C”)
[M/x]C C[(λx.[ ]] (“substituer M à x, puis C”) .

Les règles du système formel sont les suivantes:

λx_{1} ⋯ x_{n}xA_{1} ⋯ A_{m} , Ω ⟹^{ϵ,f} [π_{m+1}^{m+1}/x]x_{1} ⋯ x_{n}

\begin{matrix}A , B ⟹^{u,△} C \\ λx.A , λx.B ⟹^{u,△} xC \end{matrix} \begin{matrix}A , yB_{1} ⋯ B_{n}x ⟹^{u,△} C \\ λx.A , yB_{1} ⋯ B_{n} ⟹^{u,△} xC \end{matrix} \begin{matrix}yB_{1} ⋯ B_{n}x , A ⟹^{u,△} C \\ yB_{1} ⋯ B_{n} , λx.A ⟹^{u,△} xC \end{matrix}

(x ≠ y) xA_{1} ⋯ A_{m} , yB_{1} ⋯ B_{n} ⟹^{ϵ,r} [π_{m+1}^{m+1}/x][Ω/y]

(m < n) \begin{matrix}zA_{1}^{∗} ⋯ A_{m}^{∗}z_{m+1} ⋯ z_{n} , z_{m+1}B_{1}^{∗} ⋯ B_{n}^{∗}z_{m+2} ⋯ z_{n}z ⟹^{ϵ,r} C \\ xA_{1} ⋯ A_{m} , xB_{1} ⋯ B_{n} ⟹^{ϵ,r} [α_{n}/x]z_{m+1} ⋯ z_{n}zC \end{matrix}

(m > n) \begin{matrix}z_{n+1}A_{1}^{∗} ⋯ A_{m}^{∗}z_{n+2} ⋯ z_{m}z , zB_{1}^{∗} ⋯ B_{n}^{∗}z_{n+1} ⋯ z_{m} ⟹^{ϵ,r} C \\ xA_{1} ⋯ A_{m} , xB_{1} ⋯ B_{n} ⟹^{ϵ,r} [α_{m}/x]z_{n+1} ⋯ z_{m}zC \end{matrix}

x ∉ FV (A_{j}) ∪ FV (B_{j}) \begin{matrix}A_{j} ⪯̸ B_{j} A_{j} , B_{j} ⟹^{u,△} C \\ xA_{1} ⋯ A_{m} , xB_{1} ⋯ B_{m} ⟹^{ju,△} [π_{j}^{m}/x]C \end{matrix}

x ∈ FV (A_{j}) ∪ FV (B_{j}) \begin{matrix}A_{j} ⪯̸ B_{j} A_{j}^{∗} , B_{j}^{∗} ⟹^{u,△} C \\ xA_{1} ⋯ A_{m} , xB_{1} ⋯ B_{m} ⟹^{ju,△} [α_{q}/x]z_{m+1} ⋯ z_{q}z[π_{j}^{q}/z]C \end{matrix}

Dans la dernière règle, on choisit q ≥ m et q ≥ le maximum d’arguments que peut prendre x dans A_{j} et B_{j}, et A_{j}^{∗} désigne la forme normale de A_{j}[x ← α_{q}], qui est obtenue de manière “administrative” du fait que l’on a pris q assez grand. Il faut vérifier que A_{j} ⪯̸ B_{j} implique A_{j}^{∗} ⪯̸ B_{j}^{∗}, ce qui est encore aisé à vérifier en utilisant de même le fait que q est assez grand. On fait aussi usage de la règle ΩM = Ω (qui, avec λx.Ω = Ω est implicite dans la définition de ω(λx_{1} ⋯ x_{n}.ΩA_{1} ⋯ A_{m}) = Ω).

Proposition 3.4 Si A ⪯̸_{u,△} B, alors il existe C tel que A , B ⟹^{u,△} C. On a

A , B ⟹^{u,△} C ⇒ (C[A] →_{β}^{⋆} I et C[B] →_{β}^{⋆} Ω) .

De plus, on a les propriétés suivantes.

1. si △ = r et si B′ ≥ B, alors A , B′ ⟹^{u,r} C.

2. Si △ = f et si B′ ≥ B et B′/u = Ω, alors A , B′ ⟹^{u,f} C.

Preuve (indication). On note que les règles qui font passer de u à ju procèdent essentiellement par extraction de sous-termes. On renvoie pour les détails à [Ronchi96] ou [Barendregt84]. (La mécanique précise utilisée pour cette extraction de contexte ne sert pas dans la suite de cet article.) Pour (1), noter de plus que le Ω vient du contexte. □

Remarque 3.5 La terminologie employée est inspirée des propriétés (1) et (2) ci-dessus: r comme rigide, f comme flexible.

4 Des approximants aux arbres de Böhm

Dans cette section, nous démontrons la chaîne d’implications donnée dans l’introduction, et nous introduisons en chemin les relations d’ordre ⪯_{∞} et ˆ⪯_{∞}.

Définition 4.1 On pose M ≤_{obs} N si

∀ C (C[M], C[N] clos et C[M] a une fnt ⇒ C[N] a une fnt) .

Définition 4.2 Si A et B sont des arbres de Böhm, on pose A ⪯_{∞} B si

∀ A ≤ A, B ≤ B A ⪯̸ B ⇒ ∀ u (A ⪯̸_{u,△} B ⇒ △ = f et B/u ≠ Ω) .

Preuve de (M ≤_{obs} N) ⇒ (BT (M) ⪯_{∞} BT (N)). Supposons que BT (M) ⪯̸_{∞} BT (N). Il existe donc A ≤ BT (M), B ≤ BT (N) et u tels que A , B ⟹^{u,r} C, ou A , B ⟹^{u,f} C et B/u = Ω. Nous allons montrer que C[M] →_{β}^{⋆} I (et a donc une fnt) et que C[N] n’a pas de fnt. Soit M′ tel que M →_{β}^{⋆} M′ et A ≤ ω(M′). De C[A] →_{β}^{⋆} I, on déduit C[ω(M′)] →_{β}^{⋆} I, et donc C[M] →_{β}^{⋆} C[M′] →_{β}^{⋆} I. Pour N, on raisonne par l’absurde. Si C[N] a une fnt, alors par continuité syntaxique il existe B′ ≤ BT (N) tel que C[B′] a une fnt. Soit B′′ un majorant commun de B et B′, alors d’une part C[B′′] a une fnt puisque B′′ ≥ B′, et d’autre part C[B′′] →_{β}^{⋆} Ω par la proposition 3.4 (cas (1) ou (2) selon que Δ est r ou f, en notant dans le second cas que l’hypothèse B/u = Ω implique a fortiori B′′/u = Ω): contradiction. □

Définition 4.3 Un arbre de Böhm A est appelé expansion infinie de x, et on note x ∞A si

∀ A ≤ A (x ⪯̸ A et ∀ u (x ⪯̸_{u,△} A) ⇒ (△ = f et A/u ≠ Ω)) .

On définit la relation ˆ⪯_{∞} sur les arbres de Böhm comme suit: A ˆ⪯_{∞}B si et seulement si pour tout approximant fini A de A il existe un approximant fini B de B tel que A ⪯ B̂, où B̂ est un terme obtenu à partir de B en remplaçant éventuellement des occurrences u de Ω par une variable x si B/u est une expansion infinie de x. On dit que B̂ est une variante de B.

Lemme 4.4 Si x ∞B, alors B = λy_{1} ⋯ y_{n}.xB_{1} ⋯ B_{n} (n ≥ 1), où pour chaque i l’une des propriétés suivantes est vérifiée: y_{i} ∞B_{i}, ou B_{i} est fini et dans ce cas B_{i} →_{η}^{⋆} y_{i}.

Preuve. Il est d’abord clair, par définition de ∞, que B ≠ Ω. Donc B est de la forme λy_{1} ⋯ y_{m}.yB_{1} ⋯ B_{n}. Si l’on avait y ≠ x ou m ≠ n, on aurait

x ⪯̸_{ϵ,r} λy_{1} ⋯ y_{m}.yΩ ⋯ Ω ,

mais ceci contredit x ∞B. Donc y = x et m = n. Il faut ensuite montrer (cf. remarque 3.1) que si y_{i} ∞̸ B_{i}, alors il existe B_{i} ≤ B_{i} tel que y_{i} ⪯ B_{i}. Par définition de ∞, l’hypothèse y_{i} ∞̸ B_{i} signifie qu’il existe B_{i} ≤ B_{i} tel que y_{i} ⪯ B_{i}, ou y_{i} ⪯̸_{u,r} B_{i}, ou y_{i} ⪯̸_{u,f} B_{i} et B_{i}/u = Ω. Mais y_{i} ⪯̸_{u,r} B_{i} est exclu car on aurait alors x ⪯̸_{iu,r} B, ce qui contredit x ∞B. On exclut de même le dernier cas. il ne reste donc plus que le premier, i.e., y_{i} ⪯ B_{i}. □

Lemme 4.5 Si A ⪯_{∞} B, alors pour tous A ≤ A, B ≤ B et B̂ variante de B:

A ⪯̸ B̂ ⇒ (∀ u A ⪯̸_{u,△} B̂ ⇒ △ = f et B/u ≠ Ω) .

Preuve. Soient A ≤ A, B ≤ B et B̂ = B[x_{1}/u_{1}, …, x_{n}/u_{n}], et supposons que A ⪯̸ B̂. Soit u tel que A ⪯̸_{u,△} B̂. Si aucun des u_{j} n’est préfixe de u, alors il est facile de voir que le remplacement des occurrences u_{j} de Ω dans B par des variables dans B̂ n’affecte pas le parcours u, et que l’on a donc aussi A ⪯̸_{u,△} B, d’où △ = f et B/u = Ω. Autrement, il existe j tel que u = u_{j}v. Nous montrons par récurrence sur la longueur de v que ce cas ne peut pas se présenter. On remarque d’abord qu’au-delà de u_{j} il n’y a plus que des η-expansions de B̂, et donc qu’on ne tombe plus à droite que sur des variables, ce qui impose △ = r. Par le lemme 4.4 appliqué à x_{j} et B/u_{j}, on a B/u_{j} = λy_{1} ⋯ y_{n}.x_{j}B_{1} ⋯ B_{n}. Si u = u_{j}, alors A ⪯̸_{u,r} B[λy_{1} ⋯ y_{n}.x_{j}Ω ⋯ Ω/u_{j}], ce qui contredit A ⪯_{∞} B. Si u > u_{j}, on pose B̂′ = B̂[λy_{1} ⋯ y_{n}.x_{j}B̂_{1} ⋯ B̂_{n}/u_{j}], où, pour chaque i, B̂_{i} = B_{i} si B_{i} est fini et B̂_{i} = y_{i} sinon. Alors B̂′ est une variante de B′ = B[λy_{1} ⋯ y_{n}.x_{j}B_{1} ⋯ B_{n}/u_{j}], où, pour chaque i, B_{i} = B_{i} si B_{i} est fini et B_{i} = Ω sinon. Soient w et i tels que v = iw. Si B_{i} est fini, alors on a A ⪯̸_{u,r} B[λy_{1} ⋯ y_{n}.x_{j}Ω ⋯ B_{i} ⋯ Ω/u_{j}], ce qui est à nouveau une contradiction. Si y_{i} ∞B_{i}, alors on applique la récurrence à w, A, B′ et B̂′. □

Définition 4.6 Pour tous A, B, la frontière F r(A, B) de A relativement à B est définie comme suit:

\begin{aligned}F r(A, B) & = & \{ui | A/u = λx_{1} ⋯ x_{m}.xA_{1} ⋯ A_{n}, B/u = λx_{1} ⋯ x_{p}.xB_{1} ⋯ B_{q}, \\ & & m − n = p − q et n < i ≤ q\} . \end{aligned}

Il est facile de voir que si B ≤ B et u sont tels que A ⪯̸_{u,△} B et A/u n’est pas défini, alors u passe par la frontière, i.e., u a un préfixe v (unique) dans F r(A, B).

Preuve de (A ⪯_{∞} B) ⇒ (A ˆ⪯_{∞}B). Supposons que A ⪯_{∞} B et A ˆ⪯̸_{∞}B. On choisit A qui “témoigne” contre tous les B̂, i.e., A ⪯̸ B̂ pour toute variante B̂ d’un approximant de B. On définit deux suites infinies B_{1}, …, B_{n}, … et u_{1}, …, u_{n}, …, telles que B_{n} ≤ B et u_{n} est une occurrence dans B pour tout n. On choisit B_{1} ≤ B arbitrairement. Si B_{n} a été construit, on choisit u_{n} tel que A ⪯̸_{u_{n},f} B_{n}, puis on choisit B_{n+1} minimal tel que B_{n} ≤ B_{n+1} ≤ B et B_{n} <_{u} B_{n+1} (ce qui est possible puisque par hypothèse B/u_{n} ≠ Ω).. On note U_{n} = {u | B_{n}/u = Ω}. On a donc u_{n} ∈ U_{n}. On note aussi que U_{n+1} est obtenu à partir de U_{n} en remplaçant un élément (en l’occurrence u_{n}) par un ensemble fini d’occurrences de longueur > |u_{n}|. On montre qu’il y a dans ⋃ U_{n} des u arbitrairement longs. Supposons que non: alors la relation u R v si et seulement si |u| > |v| est bien fondée dans ⋃ U_{n} (i.e., n’admet pas de suite infinie w_{1}, …, w_{n}, … telle que w_{n+1} R w_{n} pour tout n). Mais on a par construction U_{n+1} < U_{n} pour l’extension multiset de la relation R. Or l’extension multiset d’une relation bien fondée est bien fondée. Contradiction, puisque la suite des U_{n} est infinie. On montre maintenant qu’il y a des u_{n} arbitrairement longs. Supposons que non, et soit L tel que L ≥ |u_{n}| pour tout n, et soit L′ = max(max{|u| | u ∈ U_{1}}, L + 1). On montre par récurrence que (u ∈ U_{n}) ⇒ (|u| ≤ L′), ce qui constituera une contradiction. L’implication est vraie pour n = 1 par définition de L′. Pour le pas de récurrence, il suffit d’observer que les éléments de U_{n+1} sont des éléments de U_{n} ou sont de longueur |u_{n}| + 1 (par minimalité de B_{n+1}).

L’arbre T formé par les u_{n} a donc des branches arbitrairement longues. Par ailleurs, le lemme 3.3 permet de conclure que T est aussi à branchement fini. Par le lemme de König, l’arbre T possède alors une branche infinie. Soit u le préfixe de cette branche tel que u ∈ F r(A, B). Soit V = {v | ∃ n uv = u_{n}}, qui est un arbre infini. Il existe x tel que x ⪯̸_{v,f} B_{n}/u pour tout v ∈ V. Chaque v est une occurrence de B/u (les η-expansions ne crèent pas d’Ω). Donc B/u est un arbre infini. Ceci exclut qu’il existe B′ ≤ B/u tel que x ⪯ B′ (cf. remarque 3.1). Donc tout approximant B′ de B/u est tel que x ⪯̸ B′, et si x ⪯̸_{w,△} B′, alors A ⪯̸_{uw,△} B_{n}[B′/u], ce qui implique △ = f et (B/u)/w = B/uw ≠ Ω. Nous avons monté que x ∞B/u.

On refait alors la construction ci-dessus en partant cette fois de B̂_{1} tel que B̂_{1}/u = x. Par le lemme 4.5, pour tout B̂ et tout u tel que A ⪯̸_{u,△} B̂, on a △ = f et B/u ≠ Ω. Notre raisonnement s’applique donc aussi bien à la nouvelle suitede termes. On épuise ainsi progressivement tous les éléments de F r(A, B), qui est fini. Ce qui donne une contradiction: la branche infinie que l’on construit alors ne peut pas exister car elle devrait passer par la frontière devenue vide. □

Preuve de (BT (M) ˆ⪯_{∞}BT (N)) ⇒ ([[M]] ≤ [[N]]). Supposons que BT (M) ˆ⪯_{∞} BT (N) et Γ ⊢ M : σ. Soit par le théorème 2.2 A ≤ BT (M) tel que Γ ⊢ A : σ. et soit B ≤ BT (N) et B̂ tel que A ⪯ B̂. Alors Γ ⊢ B̂ : σ, et pour ce faire on se sert de la stabilité du typage par η-égalités, que garantit pour les types de base l’égalité entre κ et ω → κ. L’objectif est de prouver qu’il existe B′ ≤ BT (N) tel que Γ ⊢ B′ : σ, car alors Γ ⊢ N : σ, grâce à la stabilité du typage par β-expansion. On ne peut pas forcément prendre B′ = B. Soit u telle que B/u = Ω et B̂/u = x, et donc telle que x ∞BT (N)/u. Il est trop brutal de remplacer un x qui peut avoir un type précis par un Ω qui ne peut avoir que le type ω. Mais, comme x remplace une η-expansion infinie dans BT (N), on peut remplacer x par une approximation suffisante pour que lui soit attribué le type voulu. L’argument est formalisé par le lemme suivant.

Lemme 4.7 Si x ∞B, alors, pour tout σ, il existe B ≤ B tel que x : σ ⊢ B : σ.

Preuve. On a B = λy_{1} ⋯ y_{n}.xB_{1} ⋯ B_{n} (avec n ≥ 1) par le lemme 4.4. On procède par récurrence sur la taille de σ. Si σ = ω, B = Ω convient. Si σ = κ, alors B = λy_{1} ⋯ y_{n}.xΩ ⋯ Ω convient, car on peut attribuer le type κ à xΩ ⋯ Ω grâce à l’inégalité κ ≤ ω → κ, puis le type κ à B grâce à l’inégalité ω → κ ≤ κ. Si σ = σ_{1} → ⋯ → σ_{m} → κ, on peut écrire σ sous la forme σ_{1} → ⋯ → σ_{n} → τ, en utilisant le cas échéant κ = ω → κ. Chacun des σ_{i} (i ≤ n) est donc soit de taille plus petite que celle de σ, soit égal à ω. Il suffit de montrer que l’on peut donner le type σ_{i} à une approximation B_{i} de B_{i} (sous l’hypothèse y_{i} : σ_{i}), pour chaque i. Ceci est évident si σ_{i} = ω. C’est également clair si B_{i} est une η-expansion finie de y_{i}. Il reste le cas où σ_{i} ≠ ω et y_{i} ∞B_{i}: alors on trouve B_{i} par hypothèse de récurrence. □

Preuve de ([[M]] ≤ [[N]]) ⇒ (M ≤_{obs} N). Cette implication est une conséquence simple de la proposition 2.3.

5 Une interprétation en termes de jeux

On peut considérer une dérivation A ⪯̸_{u,△} B comme le déroulement d’une partie entre A et B, dans laquelle l’objectif pour A est d’affirmer sa différence par rapport à B. On peut étendre cette interprétation à un arbre de Böhm A, et définir un ordre observationnel “ludique” comme suit.

Définition 5.1 On pose A ⪯̸_{u,△} B s’il existe A ≤ A tel que A ⪯̸_{u,△} B. On pose A_{1} ⪯_{∞}^{J} A_{2} si

∀ B (A_{1} ⪯̸_{u,△} B) ⇒ (A_{2} ⪯̸_{u,△} B) .

Proposition 5.2 Les ordres ⪯_{∞} et ⪯_{∞}^{J} coïncident.

Preuve. Supposons d’abord que A_{1} ⪯_{∞} A_{2}. Soit B un approximant quelconque et soit A_{1} ≤ A_{1} tel que A_{1} ⪯̸_{u,△} B. On distingue deux cas. S’il existe A_{2} ⪯ A_{2} tel que A_{1} ⪯ A_{2}, alors A_{2} ⪯̸_{u,△} B par la proposition 3.2, donc A_{2} ⪯̸_{u,△} B. Si A_{1} ⪯̸ A_{2} pour tout A_{2} ≤ A_{2}, on procède comme dans la preuve du lemme 4.5. On pose A_{2}^{0} = Ω. Si A_{1} = λy_{1} ⋯ y_{m}.xA′_{1} ⋯ A′_{n}, alors A_{2} a un approximant A_{2}^{1} = λy_{1} ⋯ y_{p}.xΩ ⋯ Ω (le nombre de Ω étant égal à p − m + n). Si u = ϵ, alors A_{2}^{1} fait aussi bien l’affaire que A_{1} contre B. Si u = iv, alors A_{1} ⪯̸_{u,△} B implique a fortiori que A_{1}/i ≠ Ω. On a donc A_{1} ⪯̸_{i,f} A_{2}^{1}, d’où l’on déduit que A_{2} a un approximant A_{2}^{2} = λy_{1} ⋯ y_{p}.xΩ ⋯ (λz⃗.tΩ⃗) ⋯ Ω obtenu par remplacement du i-ème Ω de A_{2}^{1}. Si u = i, alors A_{2}^{2} fait l’affaire. Si u > i, on poursuit la construction d’approximants A_{2}^{3}, …, A_{2}^{|u|+1} tels que pour chaque k ≤ |u| on a A_{1} ⪯̸_{u_{k},f} A_{2}^{k}, où u_{k} est le préfixe de u de longueur k − 1, et A_{2}^{|u|+1} fait l’affaire..

Réciproquement, si A_{1} ⪯_{∞}^{J} A_{2}, si A_{1} ≤ A_{1} et A_{2} ≤ A_{2} sont tels que A_{1} ⪯̸ A_{2}, et si A_{1} ⪯̸_{u,△} A_{2} alors il existe A′_{2} ≤ A_{2} tel que A′_{2} ⪯̸_{u,△} A_{2}. On a A_{2}/u ≠ Ω car A′_{2}/u ≠ Ω. Il reste à montrer △ = f. Soit A′′_{2} un majorant commun de A_{2} et A′_{2}. Alors A′′_{2} ⪯̸_{u,△} A_{2} par la proposition 3.2. Si l’on avait △ = r, on aurait alors A′′_{2} ⪯̸_{u,△} A′′_{2} par la proposition 3.4: contradiction. □

6 Comparaison avec les travaux classiques

La définition suivante est directement dérivée du travail de Hyland [Hyland76] (voir aussi [Wadsworth76, section 7]). On spécifie des relations ⪯_{k} (k entier naturel) comme suit.

\begin{matrix}Ω ⪯_{k} A & A ⪯_{0} B \\ \begin{matrix}x = y m = n A_{1} ⪯_{k} B_{1} ⋯ A_{n} ⪯_{k} B_{n} \\ xA_{1} ⋯ A_{m} ⪯_{k+1} yB_{1} ⋯ B_{n} \end{matrix} & \begin{matrix}A ⪯_{k} B \\ λx.A ⪯_{k} λx.B \end{matrix} \\ \begin{matrix}A ⪯_{k} yB_{1} ⋯ B_{n}x \\ λx.A ⪯_{k} yB_{1} ⋯ B_{n} \end{matrix} & \begin{matrix}yB_{1} ⋯ B_{n}x ⪯_{k} A \\ yB_{1} ⋯ B_{n} ⪯_{k} λx.A \end{matrix} \end{matrix}

Dans la première règle, k est quelconque, dans la deuxième, A et B sont quelconques. On pose A ⪯_{∞}^{H} B si

∀ A ≤ A, k ∃ B ≤ B A ⪯_{k} B .

Wadsworth et Hyland ont montré les équivalences suivantes.

(M ≤_{obs} N) ⇔ (BT (M) ⪯_{∞}^{H} BT (N)) ⇔ ([[M]] ≤ [[N]]) .

Mais il n’est pas difficile de prouver directement que ⪯_{∞} et ⪯_{∞}^{H} coïncident.

L’η-expansion infinie est abordée dans [Wadsworth76, section 7], à partir des termes I = λx.x et J = Y (λfxy.x(fy)) (où Y est un combinateur de point fixe, par exemple Y = λf.(λx.f(xx))(λx.f(xx))). Wadsworth compare l’égalité I = J à l’égalité 3 = 2, 9999 ⋯, et à celle entre λn.n et

Y (λfn. if n = 0 then 0 else f(n − 1) + 1) .

Dans notre terminologie, il est facile de vérifier que l’on a x ∞BT (Jx).

La définition de Nakajima [Nakajima75] (voir aussi [Barendregt84, exercice 19.4.4]) est très proche de notre caractérisation en termes de jeux. Nakajima associe à tout terme un arbre potentiellement infini verticalement et infini aussi horizontalement. Il est obtenu comme limite de toutes les η-expansions possibles de A. L’ordre est alors simplement l’ordre habituel entre les arbres ainsi associés. Les noeuds de l’arbre de Nakajima d’un terme M correspondent exactement à l’ensemble {u | ∃ B BT (M) ⪯̸_{u,△} B} de toutes les “parties gagnantes” de BT (M).

La définition de Barendregt évite le branchement horizontal infini. Si A est un arbre de Böhm et X est un arbre d’occurrences à branchement fini qui étend l’arbre d’occurrences sous-jacent à A (sans jamais prolonger un chemin menant à Ω dans A), alors X détermine une η-expansion infinie (A; X) de A (voir [Barendregt84, définition 10.2.10] pour la construction précise, par récurrence sur les occurrences). Barendregt pose que A est plus petit que B s’il existe X qui étend à la fois A et B tel que (A; X) est un sous-arbre de (B; X). Il n’est pas difficile de montrer que la définition de Barendregt est équivalente à celle de Nakajima.

Enfin, Lévy [Lévy79] a observé que l’ordre ⪯_{∞}=⪯_{∞}^{J}= ˆ⪯_{∞} correspond à une complétion (dite par idéaux fermés) dûe à Courcelle et Raoult [Courcelle+80] qui respecte les bornes supérieures dirigées existantes. L’observation de base est que I est la borne supérieure au sens de ⪯ de BT (J) considéré comme l’ensemble de ses approximants finis. Si A est un arbre de Böhm, on pose ↓_{⪯} A = {A′ | ∃ A ≤ A A′ ⪯ A}, puis on considère l’ensemble Cl(↓_{⪯} A) de tous les approximants A′′ tels que A′′ est au sens de ⪯ la borne supérieure d’un sous-ensemble dirigé au sens de ⪯ de ↓_{⪯} A. Cet ensemble comprend tous les approximants de A, mais peut contenir aussi d’autres approximants. Par exemple, on a I ∈ Cl(↓_{⪯} BT (J)). Alors A est plus petit que B si et seulement si Cl(↓_{⪯} B) contient Cl(↓_{⪯} A). On peut prouver sans grandes difficultés que cette formulation se ramène à l’ordre ⪯_{∞}^{J} (ou de Nakajima).

References

[Amadio+98] Amadio, R., et Curien, P.-L., Domains and Lambda-calculi, Cambridge University Press (1998).

[Barendregt77] Barendregt, H., The type-free lambda calculus, in Handbook of Mathematical Logic, J. Barwise editor, p.1092-1132 North Holland (1977).

[Barendregt84] Barendregt, H., The lambda calculus; its syntax and semantics, North-Holland, (1984).

[Böhm68] Böhm, C., Alcune proprietà delle formeβ − η−normali del λ − K−calcolo, Publicazione del’ Istituto per le Applicazioni del Calcolo 696, Roma (1968).

[Coppo+84] Coppo, M., Dezani, M., Honsell, F., et Longo, G., Extended type structures and filter lambda models, Proc. Logic Coll., Lolli et al. (ed.), North-Holland, (1982).

[Courcelle+80] Courcelle, B., Raoult, J.-C., Completions of ordered magmas, Fundamentae Informaticae 3, p. 105-116 (1980).

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

[Krivine91] Krivine, J.-L, Lambda-calcul, types et modèles, Masson (1991).

[Lévy76] Lévy, J.-J., An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus, Theoretical Computer Science 2, 97-114 (1976).

[Lévy79] Lévy, J.-J., Propriétés syntaxiques du λ-calcul, Notes de cours de DEA, Rapport Technique LITP 79-11, Université Paris 7 (1979).

[Nakajima75] Nakajima R., Infinite normal forms for the λ-calculus, Proc. Symposium on λ-calculus and Computer Science, Roma, Lecture Notes in Computer Science 37, Springer (1975).

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

[Wadsworth76] Wadsworth, C., The relation between computational and denotational properties for Scott’s D-infinity models of the lambda-calculus, SIAM J. of Computing 5, p. 488-521 (1976).

[Welch75] Welch, P., Continuous semantics and inside-out reductions, in Proc. of the Symp. “λ-calculus and Computer Science Theory”, Rome, March 1975, Lecture Notes in Computer Science 37, Springer (1975).