DM: Quelques modèles de graphes du 𝜆-calcul

DM de $𝜆$-calcul

Younesse Kaddar.

• Énoncé

• Version PDF

• http://younesse.net/Lambda-calcul/DM_LambdaCalcul/

I. Les modèles de graphes

1.

Soit $(B_i)_{i∈I} ∈ ℙ(D)^I$ une famille dirigée telle que

\[B ≝ \bigcup\limits_{i∈I} B_i\]

et $E ≝ \lbrace e_j \rbrace_{j∈⟦1,n⟧}⊆B$ une partie finie de $D$.

Comme $E⊆B$, pour tout $j∈⟦1,n⟧$, il existe $i_j∈I$ tel que

\[e_j ∈ B_{i_j}\]

Or comme $(B_i)_{i∈I}$ est dirigée et $\lbrace B_{i_j} \rbrace_{j∈⟦1,n⟧}$ est finie, il existe $i∈I$ tel que

\[B_i \; \text{ majore } \; \lbrace B_{i_j} \rbrace_{j∈⟦1,n⟧}\]

i.e :

\[∀j∈⟦1, n⟧, \; B_{i_j} ⊆ B_i\]

Par suite :

\[E ≝ \lbrace e_j \rbrace_{j∈⟦1,n⟧} ⊆ \bigcup\limits_{j∈⟦1, n⟧} B_{i_j} ⊆ B_i\]

On a donc montré que :

Il existe un $i∈I$ tel que

\[E⊆B_i\]

2.

Soit $A∈ℙ(D)$.

Montrons que

$i_D(A) : ℙ(D) ⟶ ℙ(D)$ est Scott-continue

1. Elle est monotone :

   Si $B, B’ ∈ ℙ(D)$ sont telles que $B ⊆ B’$ :

   \[\begin{align*} i_D(A)(B) &≝ \; \lbrace d ∈ D \mid ∃E ∈ ℙ_{fin}(D); \; E ⊆ B \text{ et } (E ⟶_D d) ∈ A\rbrace \\ &⊆ \lbrace d ∈ D \mid ∃E ∈ ℙ_{fin}(D); \; E ⊆ B' \supseteq B \text{ et } (E ⟶_D d) ∈ A\rbrace = i_D(A)(B') \end{align*}\]

2. Elle préserve les sups dirigés :

   Soit $(B_i)_{i∈I} ∈ ℙ(D)^I$ une famille dirigée.

   • \(\bigcup\limits_{i∈I} i_D(A)(B_i) ≤ i_D(A) \Big(\bigcup\limits_{i∈I} B_i\Big)\) vient du fait que : $∀i∈I, \; i_D(A)(B_i) ≤ i_D(A)(\bigcup\limits_{i∈I} B_i)$, par monotonie de $i_D(A)$

   • \[\begin{align*} i_D(A) \Big(\bigcup\limits_{i∈I} B_i\Big) & = \Big\lbrace d ∈ D \mid ∃E ∈ ℙ_{fin}(D); \; E ⊆ \bigcup\limits_{i∈I} B_i \text{ et } (E ⟶_D d) ∈ A\Big\rbrace \\ & = \Big\lbrace d ∈ D \mid ∃E ∈ ℙ_{fin}(D); \; ∃i∈I; \; E ⊆ B_i \text{ et } (E ⟶_D d) ∈ A\Big\rbrace &&\text{(par I.1))}\\ & = \Big\lbrace d ∈ D \mid∃i∈I; \; ∃E ∈ ℙ_{fin}(D); \; E ⊆ B_i \text{ et } (E ⟶_D d) ∈ A\Big\rbrace \\ & ⊆ \bigcup\limits_{i∈I} \Big\lbrace d ∈ D \mid ∃E ∈ ℙ_{fin}(D); \; E ⊆ B_i \text{ et } (E ⟶_D d) ∈ A\Big\rbrace \\ & = \bigcup\limits_{i∈I} i_D(A)(B_i) \end{align*}\]

     Donc \(\bigcup\limits_{i∈I} i_D(A)(B_i) = i_D(A) \Big(\bigcup\limits_{i∈I} B_i\Big)\)

---

---

• $i_D$ elle-même est Scott-continue de $ℙ(D)$ vers $[ℙ(D) ⟶ ℙ(D)]$

• $r_D$ est Scott-continue

• $i_D \circ r_D = id_{ℙ(D)}$

---

• $D⟦x⟧𝜌 = 𝜌(x)$

• $D⟦uv⟧𝜌 = i_D(D⟦u⟧𝜌)(D⟦v⟧𝜌)$

• $D⟦𝜆x. u⟧𝜌 = r_D(A \mapsto D⟦u⟧(𝜌[x := A]))$

• pour tous $𝜆$-termes $u, v$ $𝛽$-équivalents, pour tout environnement $𝜌$, $D⟦u⟧𝜌 = D⟦v⟧𝜌$

• $ℙ_{fin}(D) ∋ A \mapsto D ⟦u⟧ (𝜌[x := A])$, pour n’importe quel terme $u$ et n’importe quel environnement $𝜌$, est Scott-continue.

---

---

3.

Soient $x, y$ deux variables distinctes.

\[\begin{align*} D⟦𝜆x.x⟧ & = r_D(A \mapsto \underbrace{D⟦x⟧(x\mapsto A)}_{ = A}) \\ & = \lbrace E ⟶_D d \mid E∈ℙ_{fin}(D), \; d∈ E \rbrace \\ \end{align*}\] \[\begin{align*} D⟦𝜆x, y.xy⟧ & = r_D\Big(A \mapsto \underbrace{D⟦𝜆y. xy⟧(x\mapsto A)}_{ = \; r_D\big(B \mapsto D ⟦xy⟧ (x \mapsto A, \, y \mapsto B)\big)}\Big) \\ & = r_D\Big(A \mapsto r_D\big(B \mapsto \underbrace{D ⟦xy⟧ (x \mapsto A, \, y \mapsto B)}_{ =\; i_D(A)(B)} \big)\Big) \\ & = r_D (A \mapsto r_D \circ i_D(A)) \\ & = \lbrace E ⟶_D d \mid E∈ℙ_{fin}(D), \; d∈ r_D\circ i_D (E) \rbrace \end{align*}\]

Or, $∀E∈ℙ_{fin}(D)$ :

\[\begin{align*} r\circ i_D (E) & = \lbrace E' ⟶_D d' \mid E'∈ℙ_{fin}(D), \; d'∈ i_D(E)(E') \rbrace \\ & = \Big\lbrace E' ⟶_D d' \mid E'∈ℙ_{fin}(D), \; d'∈ \lbrace d'' ∈ D \mid ∃E'' ∈ ℙ_{fin}(D); \; E'' ⊆ E' \text{ et } (E'' ⟶_D d'') ∈ E\rbrace \Big\rbrace \\ & = \Big\lbrace E' ⟶_D d' \mid E'∈ℙ_{fin}(D), \; d'∈ D; \;∃E'' ⊆ E' ;\; (E'' ⟶_D d') ∈ E \Big\rbrace \\ \end{align*}\]

Donc

\[\begin{align*} D⟦𝜆x, y.xy⟧ & = \Big\lbrace E ⟶_D (E' ⟶_D d') \mid E, E'∈ℙ_{fin}(D), \; d'∈ D; \;∃E'' ⊆ E' \text{ et } (E'' ⟶_D d') ∈ E \Big\rbrace \\ \end{align*}\]

Comme $⟶_D : ℙ_{fin}(D) × D ⟶ D$ est injective et $D$ est non vide, $D$ est infini, et il existe deux élément $d, d’∈D$ tels que $d ≠ d’$.

Il vient alors que :

\[\big\lbrace \lbrace d \rbrace ⟶_D d \big\rbrace ⟶_D (\lbrace d, d' \rbrace ⟶_D d) ∈ D⟦𝜆x, y.xy⟧ \backslash D⟦𝜆x.x⟧\]

puisque

• $\lbrace d \rbrace ⊆ \lbrace d, d’ \rbrace$ et $\lbrace d \rbrace ⟶_D d ∈ \big\lbrace \lbrace d \rbrace ⟶_D d \big\rbrace$
• mais $\lbrace d, d’ \rbrace ⟶_D d ∉ \big\lbrace \lbrace d \rbrace ⟶_D d \big\rbrace$

On a donc montré que

aucun modèle de graphe $(D, ⟶_D)$ ne valide la $𝜂$-règle

4.

\[\begin{align*} D⟦𝜆x. xx⟧ & = r_D\Big(A \mapsto \underbrace{D⟦xx⟧(x\mapsto A)}_{ = \; i_D(A)(A)}\Big) \\ & = \lbrace E' ⟶_D d' \mid E'∈ℙ_{fin}(D), \; d'∈ i_D (E')(E') \rbrace \\ & = \Big\lbrace E' ⟶_D d' \mid E'∈ℙ_{fin}(D), \; d'∈ \lbrace d'' ∈ D \mid ∃E'' ⊆ E' \text{ et } (E'' ⟶_D d'') ∈ E'\rbrace \Big\rbrace \\ & = \lbrace E' ⟶_D d' \mid E'∈ℙ_{fin}(D), \; d'∈ D; \; ∃E'' ⊆ E' \text{ et } (E'' ⟶_D d') ∈ E' \rbrace \\ \end{align*}\]

Et

\[\begin{align*} D⟦𝛺⟧ & = i_D(D⟦𝜆x. xx⟧)(D⟦𝜆x. xx⟧) \\ & = \lbrace d ∈ D \mid ∃E ∈ℙ_{fin}(D);\; E⊆ D⟦𝜆x. xx⟧ \text{ et } (E ⟶_D d) ∈ D⟦𝜆x. xx⟧\rbrace \end{align*}\]

Supposons qu’il existe $d∈D⟦𝛺⟧$.

Il existe alors $E_0 ∈ℙ_{fin}(D)$ tel que

$E_0⊆ D⟦𝜆x. xx⟧$ et

\[\hspace{15em}\underbrace{(E_0 ⟶_D d) ∈ D⟦𝜆x. xx⟧}_{\large{\text{d'où l'existence d'un } E_1⊆E_0⊆D⟦𝜆x. xx⟧ \text{ tel que } \underbrace{(E_1 ⟶_D d) ∈ E_0⊆ D⟦𝜆x. xx⟧}_{\llap{\LARGE{\text{d'où l'existence d'un } E_2⊆E_1⊆D⟦𝜆x. xx⟧ \text{ tel que } \underbrace{(E_2 ⟶_D d) ∈ E_1⊆D⟦𝜆x. xx⟧}_{\llap{\LARGE{\text{ d'où l'existence d'un } E_3⊆E_2⊆D⟦𝜆x. xx⟧ \text{ tel que } \underbrace{(E_3 ⟶_D d) ∈ E_2⊆ D⟦𝜆x. xx⟧}_{\hspace{4.9em}\vdots \\\hspace{10em}\llap{\text{d'où l'existence d'un } E_{n+1}⊆E_n⊆D⟦𝜆x. xx⟧ \text{ tel que } (E_{n+1} ⟶_D d) ∈ E_n⊆ D⟦𝜆x. xx⟧}}}}}}}}}}\]

On peut ainsi construire une suite décroissante $(E_n)_{n∈ℕ} ∈ D⟦𝜆x. xx⟧^ℕ$ tel que $∀n∈ℕ$ :

\[(E_{n+1} ⟶_D d) ∈ E_n \qquad ⊛\]

Comme $(E_n)_{n∈ℕ}$ décroît et $E_0$ est finie, $(E_n)_{n∈ℕ}$ stationne en une partie $E_∞ ⊆ E_0∈ℙ_{fin}(D)$ qui vérifie, par $⊛$ :

\[(E_∞ ⟶_D d) ∈ E_∞\]

On a donc montré que :

si $d∈d∈D⟦𝛺⟧$, alors il existe $E_∞ ∈ℙ_{fin}(D)$ tel que

\[(E_∞ ⟶_D d) ∈ E_∞\]

5.

---

NB : Pour tout arbre $d∈{\cal E}_C$, on notera $size(d)$ la taille de $d$, c’est-à-dire son nombre de noeuds (noeuds internes et feuilles).

---

S'il existait $d∈{\cal E}_C ⟦𝛺⟧≠∅$, par I.4), il existerait un $E∈ℙ_{fin}({\cal E}_C)$ tel que l’arbre fini $E ⟶ d$ appartiendrait à son fils gauche $E$, ce qui est absurde puisqu’alors :

\[\begin{align*} size(E ⟶ d) & = 1 + size(d) + \sum\limits_{ d' ∈ E } size(d') \\ & = 1 + \underbrace{size(d) + \sum\limits_{ d' ∈ E\backslash \lbrace E ⟶ d \rbrace } size(d')}_{≥0} + size(E ⟶ d)\\ \end{align*}\]

On a donc montré que

\[{\cal E}_C ⟦𝛺⟧=∅\]

6.

Supposons qu’il existe un test de normalisabilité de tête $t$.

Par II.5) :

\[{\cal E}_C ⟦𝛺⟧ = ∅ ⊆ {\cal E}_C⟦𝜆x.x⟧\]

donc par monotonie de $i_{ {\cal E}_C}({\cal E}_C ⟦t⟧)$ :

\[{\cal E}_C ⟦t𝛺⟧ = i_{ {\cal E}_C}({\cal E}_C ⟦t⟧)({\cal E}_C ⟦𝛺⟧) ⊆ i_{ {\cal E}_C}({\cal E}_C ⟦t⟧)({\cal E}_C⟦𝜆x.x⟧) = {\cal E}_C ⟦t(𝜆x.x)⟧ \quad⊛\]

Or, $𝛺$ n’a pas de forme normale de tête.

• en effet : on a vu en cours qu’on peut écrire tout $𝜆$-terme $u$ de façon unique sous la forme de tête

  \[𝜆x_1,\ldots, x_n . \underbrace{h}_{\text{tête de } u} u_1 ⋯ u_m\]

  où

  • $h u_1 \ldots u_m$ n’est pas une abstraction
  • $h$ n’est pas une application
  • $n, m≥0$

  Or, la forme de tête de $𝛺$ :

  \[\underbrace{\underbrace{(𝜆x. xx)}_{\text{tête de } 𝛺}(𝜆x. xx)}_{\text{rédex de tête de } u}\]

  n’est pas une forme normale de tête (le tête n’est pas une variable).

Par suite,

• comme $t𝛺$ et $\mathbf{F}$ sont $𝛽$-équivalents, ${\cal E}_C ⟦t𝛺⟧ = {\cal E}_C ⟦\mathbf{F}⟧$

• de même, ${\cal E}_C ⟦t(𝜆x.x)⟧ = {\cal E}_C ⟦\mathbf{V}⟧$ ($𝜆x.x$ est déjà en forme normale de tête)

Donc, par $⊛$ :

\[{\cal E}_C ⟦\mathbf{F}⟧ ⊆ {\cal E}_C ⟦\mathbf{V}⟧\]

On a montré que :

S’il existe un test de normalisabilité de tête $t$, alors

\[{\cal E}_C ⟦\mathbf{F}⟧ ⊆ {\cal E}_C ⟦\mathbf{V}⟧\]

7.

Supposons qu’il existe un test de normalisabilité de tête, ce qui implique, par II.6), que ${\cal E}_C ⟦\mathbf{F}⟧ ⊆ {\cal E}_C ⟦\mathbf{V}⟧$.

Alors pour toutes variables $x$ et $y$ :

\[{\cal E}_C ⟦\mathbf{F}x⟧ = i_{ {\cal E}_C}({\cal E}_C ⟦\mathbf{F}⟧)(⟦x⟧) ⊆ i_{ {\cal E}_C}({\cal E}_C ⟦\mathbf{V}⟧)(⟦x⟧) = {\cal E}_C ⟦\mathbf{V}x⟧ \\ ⟹ {\cal E}_C ⟦\mathbf{F}xy⟧ = i_{ {\cal E}_C}({\cal E}_C ⟦\mathbf{F}x⟧)(⟦y⟧) ⊆ i_{ {\cal E}_C}({\cal E}_C ⟦\mathbf{V}x⟧)(⟦y⟧) = {\cal E}_C ⟦\mathbf{V}xy⟧ \quad ⊛\]

par monotonie de $i_{ {\cal E}_C}$ (l’ordre sur $[ℙ({\cal E}_C) ⟶ ℙ({\cal E}_C)]$ étant l’ordre point à point).

Or, pour tout environnement $𝜌$ non constant, il existe deux variables $x$ et $y$ telles que :

\[\left.\begin{cases} 𝜌(y) \not⊆ 𝜌(x) \\ {\cal E}_C ⟦\mathbf{F}xy⟧ = {\cal E}_C ⟦y⟧ = 𝜌(y) &&\text{(car } \mathbf{F}xy =_𝛽 y \text{ )}\\ {\cal E}_C ⟦\mathbf{V}xy⟧ = {\cal E}_C ⟦x⟧ = 𝜌(x) &&\text{(car } \mathbf{V}xy =_𝛽 x \text{ )} \end{cases}\right)⊛⊛\]

Et comme il existe un environnement non constant (car ${\cal E}_C$ est infini, comme on l’a vu en I.3)), $⊛⊛$ contredit $⊛$.

On a donc montré qu’il n’existe pas de test de normalisabilité de tête.

8.

Soit $t$ un terme qui a une forme normale de tête.

\[t =_𝛽 \underbrace{𝜆x_1,\ldots, x_n . \underbrace{h}_{\text{variable de tête}} u_1 ⋯ u_m}_{\text{forme normale de tête}}\]

Remarquons que si $t$ n’est pas clos, le terme $𝜆y_1, \ldots, y_k. t$, où $\lbrace y_1 , ⋯, y_k \rbrace = fv(t)$, a encore une forme normale de tête :

\[𝜆y_1, \ldots, y_k t =_𝛽 𝜆y_1, \ldots, y_k, x_1,\ldots, x_n . h u_1 ⋯ u_m\]

Donc quitte à considérer $𝜆y_1, \ldots, y_k. t$ (d’après la définition de la résolubilité d’un terme non clos), on peut supposer que $t$ est clos.

Comme $t$ est clos, $𝜆 x_1,\ldots, x_n . h u_1 ⋯ u_m$ est clos, puisque les $𝛽$-réductions ne font pas apparaître de nouvelles variables libres.

• en effet :

  Si

  • $(𝜆x. u)v ⟶_𝛽 u[x := v]$
  • et $fv\big((𝜆x. u)v\big) ≝ \big(fv(u)\backslash \lbrace x \rbrace\big) ∪ fv(v) = ∅$

  alors $fv(u[x := v]) = ∅$

  Preuve : par induction structurelle sur $u$ :

  • si $u = x$ :

    $u[x := v] = v$ et on a bien $fv(u[x := v]) = fv(v) = ∅$

  • si $u$ est une variable $y≠x$ :

    $u[x := v] = y = u$, d’où

    \[\begin{align*} fv(u[x := v]) & = fv(u) \\ & = \lbrace y \rbrace \\ & = \lbrace y \rbrace \backslash \lbrace x \rbrace \\ & = fv(u)\backslash \lbrace x \rbrace \\ & = ∅ \end{align*}\]

  • si $u = u_1 u_2$

    $\underbrace{fv(u)}_{\rlap{= \, fv(u_1) ∪ fv(u_2)}}\backslash \lbrace x \rbrace = ∅$ implique que

    • $fv(u_1)\backslash \lbrace x \rbrace=∅$
    • $fv(u_2)\backslash \lbrace x \rbrace=∅$

    donc, comme $fv(v)=∅$ :

    • $\big(fv(u_1)\backslash \lbrace x \rbrace \big)∪ fv(v)=∅$
    • $\big(fv(u_2)\backslash \lbrace x \rbrace \big) ∪ fv(v)=∅$

    et par hypothèse de récurrence sur $u_1$ et $u_2$ :

    \[fv(u_1 [x := v]) = ∅ = fv(u_2 [x := v])\]

    donc, comme $u[x := v] = (u_1 [x := v])(u_2 [x := v])$ :

    \[fv(u[x := v]) = fv(u_1 [x := v]) ∪ fv(u_2 [x := v]) = ∅\]

  • si $u = 𝜆y. u’$ :

    $u[x := v] = 𝜆y. (u’ [x := v])$, et :

    \[fv(u[x := v]) = fv(u' [x := v])\backslash \lbrace y \rbrace = ∅\]

    par hypothèse de récurrence sur $u’$, puisque

    \[\big(\underbrace{fv(u')}_{⊆ fv(u)}\backslash \lbrace x \rbrace \big) ∪ fv(v) ⊆ \big(fv(u)\backslash \lbrace x \rbrace \big) ∪ fv(v) = ∅\]

Donc $h$ est nécessairement l’un des $x_i$ : $h ≝ x_i$

Il vient alors que

\[\begin{align*} t \; \underbrace{x_1 ⋯ x_{i-1} (𝜆y_1, \ldots, y_m. \mathbf{I}) x_{i+1} ⋯ x_n}_{≝ \, \overrightarrow{u}} & =_𝛽 \overbrace{\bigg( \Big( 𝜆 x_1. \big(𝜆 x_2, \ldots, x_n . x_i u_1 ⋯ u_m \big) \Big) x_1 \bigg)}^{⟶_𝛽 \; 𝜆 x_2, \ldots, x_n . \; x_i u_1 ⋯ u_m} \; x_2 ⋯ x_{i-1} (𝜆y_1, \ldots, y_m. \mathbf{I}) x_{i+1} ⋯ x_n \\ & =_𝛽 \overbrace{\bigg( \Big( 𝜆 x_2. \big(𝜆 x_3, \ldots, x_n . x_i u_1 ⋯ u_m \big) \Big) x_2 \bigg)}^{⟶_𝛽 \; 𝜆 x_3, \ldots, x_n . \; x_i u_1 ⋯ u_m} \; x_3 ⋯ x_{i-1} (𝜆y_1, \ldots, y_m. \mathbf{I}) x_{i+1} ⋯ x_n \\ & \vdots \\ & =_𝛽 \overbrace{\bigg( \Big( 𝜆 x_{i-2}. \big(𝜆 x_{i-1}, \ldots, x_n . x_i u_1 ⋯ u_m \big) \Big) x_{i-2} \bigg)}^{⟶_𝛽 \; 𝜆 x_{i-1}, \ldots, x_n . \; x_i u_1 ⋯ u_m} \; x_{i-1} (𝜆y_1, \ldots, y_m. \mathbf{I}) x_{i+1} ⋯ x_n \\ & =_𝛽 \overbrace{\bigg( \Big( 𝜆 x_{i-1}. \big(𝜆 x_i, \ldots, x_n . x_i u_1 ⋯ u_m \big) \Big) x_{i-1} \bigg)}^{⟶_𝛽 \; 𝜆 x_{i}, \ldots, x_n . \; x_i u_1 ⋯ u_m} \; (𝜆y_1, \ldots, y_m. \mathbf{I}) x_{i+1} ⋯ x_n \\ & =_𝛽 \bigg( \Big( 𝜆 x_{i}. \big(𝜆 x_{i+1}, \ldots, x_n . x_i u_1 ⋯ u_m \big) \Big) (𝜆y_1, \ldots, y_m. \mathbf{I}) \bigg) \; x_{i+1} ⋯ x_n \\ & =_𝛽 \bigg(𝜆 x_{i+1}, \ldots, x_n . \; \underbrace{(𝜆y_1, \ldots, y_m. \mathbf{I}) \big(u_1 [x_i := 𝜆y_1, \ldots, y_m. \mathbf{I}]\big) ⋯ \big(u_m [x_i := 𝜆y_1, \ldots, y_m. \mathbf{I}]\big)}_{⟶^m_𝛽 \; \mathbf{I}}\bigg) \; x_{i+1} ⋯ x_n \\ & =_𝛽 \Big(𝜆 x_{i+1}, \ldots, x_n . \; \mathbf{I} \Big) \; x_{i+1} ⋯ x_n \\ & =_𝛽 \; \mathbf{I} \end{align*}\]

On a donc montré que

Si un terme $t$ a une forme normale de tête, il est résoluble.

9.

Soit $t$ un terme clos résoluble, i.e il existe une suite $\overrightarrow{u}$ telle que $t \overrightarrow{u} =_𝛽 \mathbf{I}$.

Par l’absurde : Supposons que $D⟦t⟧=∅$.

Alors

\[i_D(D⟦t⟧) = i_D(∅) = \begin{cases} ℙ(D) &⟶ ℙ(D) \\ B &\mapsto \; \lbrace d ∈ D \mid ∃E ∈ ℙ_{fin}(D); \; E ⊆ B \text{ et } (E ⟶_D d) ∈ ∅\rbrace \\ & \qquad = ∅ \end{cases}\]

i.e :

\[i_D(D⟦t⟧) = ℙ(D) ⟶ ℙ(D), B \mapsto ∅ \qquad ⊛\]

Par ailleurs :

\[D⟦t \overrightarrow{u}⟧ = \begin{cases} D⟦\,\mathbf{I}\,⟧ = \lbrace E ⟶_D d \mid E∈ℙ_{fin}(D), \; d∈ E \rbrace\\ i_D(D⟦t⟧)(D⟦\overrightarrow{u}⟧) = ∅ &&\text{(par } ⊛ \text{)} \end{cases}\]

Donc $\lbrace E ⟶_D d \mid E∈ℙ_{fin}(D), \; d∈ E \rbrace = ∅ \quad ⊛⊛$.

Or, comme $D$ est non vide, il existe $d∈D$, d’où :

\[\lbrace d \rbrace ⟶ d ∈ \lbrace E ⟶_D d \mid E∈ℙ_{fin}(D), \; d∈ E \rbrace ≠ ∅\]

ce qui contredit $⊛⊛$.

On a donc montré que :

tout terme $t$ clos et résoluble vérifie

\[D⟦t⟧=∅\]

10.

$𝛺 ≝ (𝜆x. xx)(𝜆x. xx)$ n’est pas résoluble.

en effet :

Méthode 1 :

On a montré en III. 9) que, pour tout terme $t$ : si $t$ est résoluble, alors pour tout modèle de graphes $(D, ⟶_D)$, $D⟦t⟧≠∅$.

Par contraposée, pour tout terme $t$ : s’il existe un modèle de graphes $(D, ⟶_D)$ tel que $D⟦t⟧=∅$, alors $t$ n’est pas résoluble.

Or, par II.5) : ${\cal E}_C⟦𝛺⟧ = ∅$. Donc $𝛺$ n’est pas résoluble.

Méthode 2 :

S'il existait une suite $\overrightarrow{u}$ telle que $𝛺 \overrightarrow{u} =_𝛽 \mathbf{I}$, alors $𝛺 \overrightarrow{u}$ serait faiblement normalisant, et d’après le théorème de standardisation, la réduction gauche $⟶_{g}^\ast$ calculerait la forme normale de $𝛺 \overrightarrow{u}$ (c’est-à-dire $\mathbf{I}$) par une réduction finie.

Or, elle boucle indéfiniment :

\[\underline{(𝜆x. xx)(𝜆x. xx)} \overrightarrow{u} ⟶_{\text{lm}} \underline{(𝜆x. xx)(𝜆x. xx)} \overrightarrow{u} ⟶_{\text{lm}} ⋯\]

11.

Soit $S’$ un ensemble saturé.

Montrons que, pour tout ensemble $S$, $S⟹S’$ est saturé.

Soit $S$ un ensemble, soit $u[x := t]v_1 v_2 ⋯ v_n ∈ S⟹S’$.

Montrons que $(𝜆x. u) t v_1 v_2 ⋯ v_n ∈ S⟹S’$, i.e que pour tout $v∈S$, $(𝜆x. u) t v_1 v_2 ⋯ v_n v ∈ S’$.

Soit $v∈S$.

Comme $u[x := t]v_1 v_2 ⋯ v_n ∈ S⟹S’$ :

\[u[x := t]v_1 v_2 ⋯ v_n v ∈ S'\]

et comme $S’$ est saturé :

\[(𝜆x. u) t v_1 v_2 ⋯ v_n v ∈ S'\]

Le résultat est acquis.

On a montré que

Si $S’$ est saturé, $S⟹S’$ le reste pour tout ensemble $S$.

12.

Soient $t$ un $𝜆$-terme dont la réduction de tête

\[t ⟶_t t_1 ⟶_t t_2 ⟶_t ⋯\]

ne termine pas, et $x$ une variable.

Par l’absurde : supposons que la réduction de tête de $tx$ termine.

Alors nécessairement, l’un des $t_i$ est une $𝜆$-abstraction.

• car sinon : $tx$ a une réduction de tête infinie :

  \[tx ⟶_t t_1 x ⟶_t t_2 x ⟶_t ⋯\]

  puisqu’aucun $t_i x$ n’est un rédex qui se contracte.

Notons $i$ le plus petit indice tel que $t_i$ est une $𝜆$-abstraction :

\[t_i ≝ 𝜆 y. u\]

Alors

\[tx ⟶_t t_1 x ⟶_t ⋯ ⟶_t \underbrace{t_i}_{= 𝜆y. u} x ⟶_t u[y:=x]\]

où $u[y:=x]$ a une réduction de tête finie (puisque c’est le cas de $tx$).

Montrons que

le fait que $u[y:=x]$ ait une réduction de tête finie implique que $u$ a une réduction de tête finie.

Preuve :

Par l’absurde, si $u$ avait une réduction de tête infinie :

\[u ⟶_t u_1 ⟶_t u_2 ⟶_t ⋯\]

montrons que $u[y:=x]$ aurait la réduction de tête infinie :

\[u[y:=x] ⟶_t u_1[y:=x] ⟶_t u_2[y:=x] ⟶_t ⋯\]

• En effet : il suffit (le reste s’ensuit de manière immédiate) de montrer que :

  si $u ⟶_t u_1$, alors $u[y:=x] ⟶_t u_1[y:=x]$

  Preuve : supposons que

  \[u ≝ 𝜆x_1, \ldots, x_n. \underbrace{(𝜆z. v) u'_1}_{\text{rédex de tête}} ⋯ u'_m ⟶_t 𝜆x_1, \ldots, x_n. v[z := u'_1] u'_2 ⋯ u'_m ≝ u_1\]

  NB : $u$ n’est pas en forme normale de tête car sinon la réduction de tête s’arrête.

  Alors

  \[\begin{cases} u[y:=x] &= 𝜆x_1, \ldots, x_n. \overbrace{\big((𝜆z. v)[y:=x]\big)}^{≝ \, 𝜆z. (v[y:=x]) \quad ⊛} \, (u'_1[y:=x]) (u'_1[y:=x]) ⋯ (u'_m[y:=x]) \\ &⟶_t 𝜆x_1, \ldots, x_n. (v[y:=x])\Big[z:= u'_1[y:=x]\Big] \, (u'_2[y:=x]) ⋯ (u'_m[y:=x])\\ \\ u_1[y:=x] &= 𝜆x_1, \ldots, x_n. \big(v[z := u'_1] [y:=x]\big) \, (u'_2[y:=x]) ⋯ (u'_m[y:=x]) \end{cases}\]

  Or :

  \[v[y:=x]\big[z:= u'_1[y:=x]\big] = v[z := u'_1] [y:=x]\]

  • en effet : on suppose, modulo $𝛼$-renommage, que

    • $y$ est substituable par $x$ dans $𝜆z. v$ ($⊛$), i.e

      \[y, x∉ bv(v)∪ \lbrace z \rbrace\]

    • $y$ est substituable par $x$ dans $u’_1$, i.e

      \[y, x∉ bv(u'_1)\]

    • $z$ est substituable par $u’_1[y:=x]$ dans $v[y:=x]$, i.e

      \[z, fv(u'_1[y:=x])∉ bv(v[y:=x])\]

    • $z$ est substituable par $u’_1$ dans $v$, i.e

      \[z, fv(u'_1)∉ bv(v)\]

    • $y$ est substituable par $x$ dans $v[z := u’_1]$, i.e

      \[y, x∉ bv(v[z := u'_1])\]

    et on le montre par induction structurelle sur $v$ :

    • si $v$ est une variable $x’∉ \lbrace y, z \rbrace$ :

      \[\begin{cases} x'[y:=x]\big[z:= u'_1[y:=x]\big] = x' \\ x'[z := u'_1] [y:=x] = x' \end{cases}\]

    • si $v = y$ :

      \[\begin{cases} y[y:=x]\big[z:= u'_1[y:=x]\big] = x\big[z:= u'_1[y:=x]\big] = x &&\text{( } x≠z \text{)}\\ y[z := u'_1] [y:=x] = y[y:=x] = x &&\text{( } y≠z \text{)}\\ \end{cases}\]

    • si $v = z$ :

      \[\begin{cases} z[y:=x]\big[z:= u'_1[y:=x]\big] = z\big[z:= u'_1[y:=x]\big] = u'_1[y:=x] &&\text{( } z≠y \text{)}\\ z[z := u'_1] [y:=x] = u'_1[y:=x] \end{cases}\]

    • si $v = v_1 v_2$ :

      \[\begin{cases} (v_1 v_2)[y:=x]\big[z:= u'_1[y:=x]\big] = \Big(v_1[y:=x]\big[z:= u'_1[y:=x]\big]\Big) \Big(v_2[y:=x]\big[z:= u'_1[y:=x]\big]\Big) \\ (v_1 v_2)[z := u'_1] [y:=x] = \Big(v_1 [z := u'_1] [y:=x]\Big) \Big(v_2 [z := u'_1] [y:=x]\Big)\\ \end{cases}\]

      et on conclut avec

      \[\begin{cases} v_1[y:=x]\big[z:= u'_1[y:=x]\big] = v_1 [z := u'_1] [y:=x]\\ v_2[y:=x]\big[z:= u'_1[y:=x]\big] = v_2 [z := u'_1] [y:=x]\\ \end{cases}\]

      par hypothèse de récurrence, puisque

      \[\begin{cases} bv(v) = bv(v_1)∪bv(v_2) \\ bv(v[y:=x]) = bv(v_1[y:=x])∪ bv(v_2[y:=x])\\ bv(v[z := u'_1]) = bv(v_1[z := u'_1]) ∪ bv(v_2[z := u'_1]) \end{cases}\]

      d’où le fait que les hypothèses de “substituabilité” restent vérifiées

    • si $v = 𝜆z_1. v_1$ :

      \[\begin{cases} v[y:=x]\big[z:= u'_1[y:=x]\big] = 𝜆z_1. \Big(v_1[y:=x]\big[z:= u'_1[y:=x]\big]\Big) \\ v[z := u'_1] [y:=x] = 𝜆z_1. \Big(v_1 [z := u'_1] [y:=x]\Big)\\ \end{cases}\]

      et on conclut avec

      \[v_1[y:=x]\big[z:= u'_1[y:=x]\big] = v_1 [z := u'_1] [y:=x]\]

      par hypothèse de récurrence, puisque

      \[\begin{cases} bv(v) = bv(v_1)∪ \lbrace z \rbrace \\ bv(v[y:=x]) = bv(v_1[y:=x])∪ \lbrace z \rbrace\\ bv(v[z := u'_1]) = bv(v_1[z := u'_1]) ∪ \lbrace z \rbrace \end{cases}\]

      d’où le fait que les hypothèses de “substituabilité” restent vérifiées

  Donc

  \[\begin{align*} u[y:=x] &⟶_t 𝜆x_1, \ldots, x_n. \underline{(v[y:=x])\Big[z:= u'_1[y:=x]\Big]} \, (u'_2[y:=x]) ⋯ (u'_m[y:=x])\\ & \; = \; 𝜆x_1, \ldots, x_n. \underline{\big(v[z := u'_1] [y:=x]\big)} \, (u'_2[y:=x]) ⋯ (u'_m[y:=x]) \\ & \; = \; u_1[y:=x] \end{align*}\]

  et le résultat est acquis.

Comme $u[y:=x]$ a une réduction de tête finie, il vient donc que $u$ a une réduction de tête finie.

Par suite, $𝜆y. u = t_i$ a une réduction de tête finie.

• en effet : comme $u$ a une réduction de tête finie de la forme :

  \[u ⟶_t u_1 ⟶_t ⋯ ⟶_t u_n\]

  il s’ensuit que $𝜆y. u$ a la réduction de tête finie :

  \[𝜆y. u ⟶_t 𝜆y. u_1 ⟶_t ⋯ ⟶_t 𝜆y. u_n\]

Or, cela contredit le fait que $t$ ait une réduction de tête infinie, puisque

\[t ⟶_t t_1 ⟶_t t_2 ⟶_t t_i = 𝜆y.u\]

On a donc montré que

Si $t$ est un $𝜆$-terme dont la réduction de tête ne termine pas, et $x$ une variable, alors la réduction de tête de $tx$ ne termine pas non plus.

13.

Soit $S’$ un $K$-candidat, et $S$ un ensemble de $𝜆$-termes contenant au moins une variable.

Montrons que $S ⟹ S’$ est un $K$-candidat.

1. $S ⟹ S’$ est saturé

En effet : on applique IV. 11), puisque $S’$ est saturé (car $S’$ est un $K$-candidat).

2. $S_0 ⊆ S ⟹ S’$

Si $x \overrightarrow{u} ∈ S_0$, montrons que $x \overrightarrow{u} ∈ S ⟹ S’$.

Soit $v∈S$.

Montrons que $x \overrightarrow{u} v ∈ S’$.

C’est le cas puisque $S_0 ⊆ S’$ (car $S’$ est un $K$-candidat) et :

\[x \overrightarrow{u} v ∈ S_0 ⊆ S'\]

Donc $x \overrightarrow{u} ∈ S ⟹ S’$, et

\[S_0 ⊆ S ⟹ S'\]

3. $S ⟹ S’ ⊆ S_h$

Si $u∈S ⟹ S’$, montrons que $u∈S_h$.

Comme $u∈S ⟹ S’$ et $S’ ⊆ S_h$ (car $S’$ est un $K$-candidat) :

\[∀v∈S, uv∈S' ⊆ S_h\]

Par conséquent, pour toute variable $x∈S$ : $ux$ a une réduction de tête finie, ce qui implique, par contraposée de IV. 12), que $u$ aussi, c’est-à-dire que $u∈S_h$.

Or, il existe une variable $x∈S$ par hypothèse : donc

\[u∈S_h\]

et il en résulte que

\[S ⟹ S' ⊆ S_h\]

On a donc montré que

Si $S’$ est un $K$-candidat, et $S$ un ensemble de $𝜆$-termes contenant au moins une variable, $S ⟹ S’$ reste un $K$-candidat.

14.

Montrons, par induction structurelle sur le $𝜆$-terme $t$, que

Si $t$ est un $𝜆$-terme, et $𝜌, 𝜃, d$ tels que :

1. $𝜌 : \overbrace{Var}^{\text{variables}} ⟶ ℙ({\cal E}_C)$

2. $𝜃 ≝ [x_1 := v_1, ⋯ , x_n := v_n]$ est une substitution telle que $dom(𝜃) ≝ \lbrace x_1, \ldots, x_n \rbrace \supseteq fv(t)$

3. $∀i∈⟦1,n⟧, v_i ∈ I(𝜌(x_i))$

4. $d ∈ {\cal E}_C ⟦t⟧𝜌$

alors

\[t𝜃 ∈ I(d)\]

Si $t=x_1∈Var$

alors

• $d∈{\cal E}_C ⟦x_1⟧𝜌 = 𝜌(x_1)$
• $𝜃 ≝ [x_1 := v_1]$
• $v_1 ∈ I(𝜌(x_1))$

d’où :

\[\begin{align*} t𝜃 = v_1 & ∈ I(𝜌(x_1)) \\ & = \bigcap\limits_{d'∈𝜌(x_1)} I(d') \\ & = \bigcap\limits_{d'∈𝜌(x_1)\backslash \lbrace d \rbrace} I(d') ∩ I(d) \\ & ⊆ I(d) \end{align*}\]

et le résultat est acquis.

Si $t=uv$

Alors

• comme

  \[d∈{\cal E}_C ⟦uv⟧𝜌 = i_{\cal E_c}({\cal E}_C ⟦u⟧𝜌)({\cal E}_C ⟦v⟧𝜌) \\ = \big\lbrace d'∈ {\cal E}_C \mid ∃ E ∈ ℙ_{fin}({\cal E}_C); \; E⊆{\cal E}_C ⟦v⟧𝜌 \text{ et } E ⟶_{ {\cal E}_C} d'∈{\cal E}_C ⟦u⟧𝜌 \big\rbrace\]

  il existe $E ≝ \lbrace e_i \rbrace_{i∈⟦1, N⟧}∈ ℙ_{fin}({\cal E}_C)$ telle que

  • $E⊆{\cal E}_C ⟦v⟧𝜌$
  • et $E ⟶_{ {\cal E}_C} d∈{\cal E}_C ⟦u⟧𝜌$

• pour tout $i∈⟦1, N⟧$, $v𝜃 ∈ I(e_i)$ par hypothèse de récurrence sur $v$

  • qu’il est loisible d’appliquer puisque les conditions d’application 1., 2. et 3. restent vérifiées (comme $fv(v)⊆fv(t)$) et $e_i∈E⊆{\cal E}_C ⟦v⟧𝜌$

  Donc

  \[v𝜃 ∈ \bigcap\limits_{i=1}^N I(e_i) = I(E)\]

• comme

  • $E ⟶_{ {\cal E}_C} d∈{\cal E}_C ⟦u⟧𝜌$
  • les conditions d’application 1., 2. et 3. sont vérifiées pour $u$ (comme $fv(u)⊆fv(t)$)

  alors par hypothèse de récurrence sur $u$ :

  \[u𝜃 ∈ I(E⟶_{ {\cal E}_C} d) = I(E) ⟹ I(d)\]

Par suite :

\[t𝜃 = (u𝜃)(v𝜃) ∈ I(d)\]

puisque $u𝜃 ∈ I(E) ⟹ I(d)$ et $v𝜃 ∈ I(E)$.

Le résultat est acquis.

Si $t = 𝜆x.u$

Alors

• comme

  \[d∈{\cal E}_C ⟦𝜆x.u⟧𝜌 = r_{\cal E_c}(A \mapsto {\cal E}_C ⟦u⟧𝜌[x:=A])\\ = \big\lbrace E ⟶_{\cal E_c} d' \mid E ∈ ℙ_{fin}({\cal E}_C), \; d'∈{\cal E}_C ⟦u⟧𝜌[x:=E] \big\rbrace\]

  il existe $E∈ ℙ_{fin}({\cal E}_C), \; d’∈{\cal E}_C ⟦u⟧\overbrace{𝜌[x:=E]}^{≝ \, 𝜌’}$ tels que

  \[d = E ⟶_{\cal E_c} d'\]

• pour tout $e∈I(E)$, comme

  • $𝜌’ ≝ 𝜌[x:=E] : Var ⟶ ℙ({\cal E}_C)$
  • $𝜃_e ≝ 𝜃[x:=e]$ est une substitution telle que
  \[\begin{align*} dom(𝜃_e) & ≝ \lbrace x_1, \ldots, x_n, x \rbrace \\ & = \lbrace x_1, \ldots, x_n \rbrace ∪ \lbrace x \rbrace \\ & \supseteq fv(t) ∪ \lbrace x \rbrace \\ & = fv(u) \end{align*}\]

  • $e∈I(\overbrace{E}^{= \, 𝜌’(x)}) = I(𝜌’(x))$ et $∀i∈⟦1,n⟧, v_i ∈ I(𝜌(x_i))$

  • $d’∈{\cal E}_C ⟦u⟧𝜌’$

  alors par hypothèse de récurrence sur $u$ :

  \[u (𝜃 [x:=e]) = u 𝜃_e ∈ I(d') \quad ⊛\]

Montrons que

\[t𝜃 = 𝜆x. (u𝜃) ∈ I(d) = I(E)⟹I(d')\]

Soit $e∈I(E)$.

\[(t𝜃)e = (𝜆x. (u𝜃))e ⟶_t (u𝜃)[x:=e] = \underbrace{u(𝜃[x:=e])}_{∈ I(d') \text{ par } ⊛}\]

la dernière égalité venant du fait que $x ∉ \lbrace x_1, \ldots, x_n \rbrace ⊆ fv(t)$ et que $x$ n’est libre dans aucun $v_i$, modulo $𝛼$-renommage (cf. bas de la page 9 du cours, dans la démonstration de la terminaison de la $𝛽^\ast$-réduction).

Or, $I(d’)$ est clos par réduction de tête faible inverse (en tant que $K$-candidat), donc comme $(u𝜃)[x:=e] ∈ I(d’)$ :

\[(t𝜃)e = (𝜆x.(u𝜃))e ∈I(d')\]

Donc $t𝜃 ∈ I(E)⟹I(d’) = I(d)$, et le résultat est acquis.

15.

Soit $t$ un $𝜆$-terme tel qu’il existe un environnement $𝜌$ tel que ${\cal E}_C⟦t⟧ 𝜌 ≠ ∅$.

Montrons que la réduction de tête partant de $t$ termine, c’est-à-dire que $t∈S_h$.

On va utiliser le résultat de la question IV. 14) :

• il existe $d∈ {\cal E}_C⟦t⟧ 𝜌 ≠ ∅$, par hypothèse

• on peut prendre $𝜃 ≝ [x_1 := x’_1, ⋯ , x_n := x’_n]$

  • avec $\lbrace x_1, \ldots, x_n \rbrace = fv(t)$ et où les $x’_i$ sont des variables deux à deux distinctes, différentes des $x_i$ et n’apparaissant pas dans $t$

  puisque

  • $dom(𝜃) \supseteq fv(t)$

  • $∀i∈⟦1, n⟧, x’_i ∈ S_0 ⊆ I(𝜌(x_i))$ puisque $I(𝜌(x_i))$ est un $K$-candidat (d’où $S_0 ⊆I(𝜌(x_i))$).

    • en effet :

      • si $𝜌(x_i)≠∅$ : $I(𝜌(x_i)) = \bigcap\limits_{d’∈𝜌(x_i)≠∅} I(d’)$, et les $K$-candidats sont clos par intersection non vide
      • si $𝜌(x_i)=∅$ : $I(𝜌(x_i)) = \bigcap\limits_{d’∈∅} I(d’) = S_h$ est un $K$-candidat

donc, par IV. 14) :

\[t =_𝛼 t𝜃 ∈ I(d) ⊆ S_h\]

la dernière inclusion venant du fait que $I(d)$ est un $K$-candidat (d’où $I(d)⊆S_h$).

On a donc montré que :

Si $t$ est un $𝜆$-terme tel que ${\cal E}_C⟦t⟧ 𝜌 ≠ ∅$ pour un environnement $𝜌$, alors la réduction de tête partant de $t$ termine.

16.

Eléments stricts de ${\cal E}_C$ :

• $c ∈ C$
• ou $E ⟶ d$ où $E≠∅$ ne contient que des éléments stricts et $d$ est strict.

Montrons que, pour tout terme clos $t$ :

1. $t$ a une forme normale

2. ${\cal E}_C ⟦t⟧$ contient un élément strict

3. $t$ est normalisable par la gauche

sont des propriétés équivalentes.

$1. ⟹ 2.$

On prouve par induction structurelle sur $t∈𝛬$ :

Lemme : Si $t$ a une forme normale, il existe un environnement $𝜌$ tel que

• pour toute variable $x$, $𝜌(x)$ est fini et strict
• ${\cal E}_C ⟦t⟧𝜌$ contient un élément strict

• Cas de base : si $t=x∈Var$ :

  c’est trivial, en prenant $𝜌(y)≝ \lbrace c \rbrace$ pour toute variable $y$, et pour un $c∈C$ (il en existe un car $C≠∅$).

• Hérédité : si $t=uv$ ou $t = 𝜆x. u$ :

  On écrit $t$ sous la forme de tête

  \[t ≝ 𝜆x_1,\ldots, x_n . \underbrace{h}_{\text{tête de } t} u_1 ⋯ u_m\]

  Quitte à considérer la forme normale de $t’$ de $t$, qui vérifie ${\cal E}_C ⟦t’⟧𝜌 = {\cal E}_C ⟦t⟧𝜌$ pour tout environnement $𝜌$, on peut supposer que $t$ est sous forme normale, ce qui implique que $h$ est une variable de tête.

  En outre, pour tout $𝜌$ :

  \[\begin{align*} {\cal E}_C ⟦t⟧𝜌 &= r_{ {\cal E}_C}\big(A_1 \mapsto {\cal E}_C ⟦𝜆x_2,\ldots, x_n . h u_1 ⋯ u_m⟧𝜌[x_1 \mapsto A_1]\big) \\ & = \Big\lbrace E_1 ⟶ d_1 \mid E_1∈ℙ_{fin}({\cal E}_C), \; d_1∈ {\cal E}_C ⟦𝜆x_2,\ldots, x_n . h u_1 ⋯ u_m⟧𝜌[x_1 \mapsto E_1] \Big\rbrace \\ & = \bigg\lbrace E_1 ⟶ d_1 \mid E_1∈ℙ_{fin}({\cal E}_C), \; d_1∈ \Big\lbrace E_2 ⟶ d_2 \mid E_2∈ℙ_{fin}({\cal E}_C), \; d_2∈ {\cal E}_C ⟦𝜆x_3,\ldots, x_n . h u_1 ⋯ u_m⟧𝜌[x_1 \mapsto E_1, x_2 \mapsto E_2] \Big\rbrace \bigg\rbrace \\ & = \Big\lbrace E_1 ⟶ d_1 \mid E_1∈ℙ_{fin}({\cal E}_C), \; d_1∈ {\cal E}_C ⟦𝜆x_2,\ldots, x_n . h u_1 ⋯ u_m⟧𝜌[x_1 \mapsto E_1] \Big\rbrace \\ & = \bigg\lbrace E_1 ⟶ (E_2 ⟶ d_2) \mid E_1, E_2∈ℙ_{fin}({\cal E}_C), \; d_2∈ {\cal E}_C ⟦𝜆x_3,\ldots, x_n . h u_1 ⋯ u_m⟧𝜌[x_1 \mapsto E_1, x_2 \mapsto E_2] \Big\rbrace \\ & \vdots \\ & = \bigg\lbrace E_1 ⟶ (E_2 ⟶ ⋯ (E_n ⟶ d_n)⋯) \mid E_1, \ldots, E_n ∈ℙ_{fin}({\cal E}_C), \; d_n∈ \underbrace{ {\cal E}_C ⟦h u_1 ⋯ u_m⟧𝜌[x_1 \mapsto E_1, \ldots, x_n \mapsto E_n]}_{\llap{ = \; \lbrace d'_m ∈ D \; \mid \; ∃E'_m ∈ ℙ_{fin}(D); \; E'_m ⊆ {\cal E}_C⟦u_m⟧𝜌[x_1 \mapsto E_1, \ldots, x_n \mapsto E_n] \text{ et } (E'_m ⟶ d'_m) ∈{\cal E}_C⟦h u_1 ⋯ u_m⟧𝜌[x_1 \mapsto E_1, \ldots, x_n \mapsto E_n]\rbrace}} \Big\rbrace \\ & \vdots \\ & = \bigg\lbrace E_1 ⟶ ⋯ ⟶ E_n ⟶ d_n \mid E_1,\ldots, E_n ∈ℙ_{fin}({\cal E}_C), ∃ E'_m, \ldots, E'_1 ∈ℙ_{fin}({\cal E}_C); \; \\ & \qquad \; \quad \; ∀i∈⟦1, m⟧, \; E'_i ⊆ {\cal E}_C⟦u_i⟧𝜌[x_i \mapsto E_i]_{1≤i≤n} \\ & \qquad \; \text{ et } E'_1 ⟶ ⋯ ⟶ E'_m ⟶ d_n ∈ \underbrace{ {\cal E}_C ⟦h⟧𝜌[x_i \mapsto E_i]_{1≤i≤n}}_{ = 𝜌[x_i \mapsto E_i]_{1≤i≤n}(h)} \Big\rbrace \\ \end{align*}\]

  On veut construire un $𝜌$ pour lequel ${\cal E}_C ⟦t⟧𝜌$ contient un élément strict.

  Or, l’hypothèse d’induction appliquée aux $u_i$ nous fournit, pour tout $i∈⟦1, m⟧$, un environnement $𝜌_i$ tel que ${\cal E}_C ⟦u_i⟧𝜌_i$ contient un élément strict $d_i$.

  Soit $c∈C≠∅$.

  En notant $𝜌$ l’environnement défini par :

  \[\begin{cases} ∀x∈Var\backslash \lbrace h \rbrace, \; 𝜌(x) &≝ \bigcup\limits_{1≤i≤m} 𝜌_i (x) \\ 𝜌(h) &= \bigcup\limits_{1≤i≤m} 𝜌_i (h) \; ∪ \; \big\lbrace \underbrace{\lbrace d_1 \rbrace ⟶ ⋯ ⟶ \lbrace d_m \rbrace ⟶ c}_{\text{ strict}} \big\rbrace \end{cases}\]

  Pour tout $i∈⟦1, m⟧, 𝜌_i ≤ 𝜌$, donc par monotonie de $D⟦u’⟧(ρ’[x := \bullet])$ (pour tout $u’$ et $𝜌’$) :

  \[∀i∈⟦1, m⟧, \, d_i ∈ {\cal E}_C ⟦u_i⟧𝜌\]

  d’où

  \[∀i∈⟦1, m⟧, \, \lbrace d'_i \rbrace ⊆ {\cal E}_C ⟦u_i⟧𝜌\]

  Par conséquent :

  \[𝜌(x_1) ⟶ ⋯ ⟶ 𝜌(x_n) ⟶ c ∈ {\cal E}_C ⟦t⟧𝜌\]

  (avec $E’_i = \lbrace d’_i \rbrace$ dans la définition ensembliste précédente)

  Or, par hypothèse d’induction, pour tout $(i, j)∈⟦1, m⟧×⟦1, n⟧$, $𝜌_i(x_j)$ est fini et strict, donc par définition de $𝜌$, les $𝜌(x_j)$ sont finis et stricts, d’où :

  \[𝜌(x_1) ⟶ ⋯ ⟶ 𝜌(x_n) ⟶ c ∈ {\cal E}_C ⟦t⟧𝜌 \text{ est strict}\]

  Le résultat est acquis.

Enfin, si $t$ est un terme clos, on lui applique le lemme précédent : il existe un environnement $𝜌$ tel que ${\cal E}_C ⟦t⟧𝜌 = {\cal E}_C ⟦t⟧$ contient un élément strict, ce qui conclut.

$2. ⟹ 3.$

NB :

• la saturation est dès à présent entendue pour la réduction gauche.
• on notera $⟶_g$ la réduction gauche (et $⟶_g^\ast$ sa clôture réflexive transitive).
• notons que la réduction de tête est un cas particulier de réduction gauche.

Comme $S’_0$ est trivialement saturé et contient les variables, on a les mêmes résultats concernant l’ensemble des $K’$-candidats qu’en IV) (les démonstrations sont les quasiment les mêmes pour les résultats analogues aux questions 11) et 13) : les éléments nouveaux/modifiés y sont mis en gras) :

---

Résultat analogue à IV. 11) pour les $K’$-candidats :

Si $S’$ est saturé, $S⟹S’$ le reste pour tout ensemble $S$.

Soit $S’$ un ensemble saturé.

Montrons que, pour tout ensemble $S$, $S⟹S’$ est saturé.

Soit $S$ un ensemble, soient $u ∈ S⟹S’$ et $u’$ tel que $u’ ⟶_g u$.

Montrons que $u’ ∈ S⟹S’$, i.e que pour tout $v∈S$, $u’ v ∈ S’$.

Soit $v∈S$.

Comme $u ∈ S⟹S’$ :

\[u v ∈ S'\]

et comme $S’$ est saturé :

\[u' v ∈ S'\]

---

Résultat analogue à IV. 12) pour les $K’$-candidats :

Si $t$ est un $𝜆$-terme dont la réduction gauche ne termine pas, et $x$ une variable, alors la réduction gauche de $tx$ ne termine pas non plus.

Soient $t$ un $𝜆$-terme dont la réduction gauche ne termine pas, et $x$ une variable.

Par l’absurde : supposons que la réduction gauche de $tx$ termine.

Comme la réduction de tête est un cas particulier de réduction gauche, la réduction de tête de $t$ ne termine pas non plus.

Donc, par IV.12), la réduction de tête de $tx$ ne termine pas.

Or, comme la réduction gauche de $tx$ termine, $tx$ a une forme normale de tête.

• car sinon : en notant $t_n$ le dernier terme produit par la réduction gauche de $tx$, la forme normale de $t_n$ a un rédex de tête (puisqu’elle n’est pas normale de tête), lequel peut être contracté par réduction gauche (ce qui contredit la définition de $t_n$).

Cela contredit le fait que la réduction de tête de $tx$ ne termine pas, d’après les équivalences montrées à la fin de la partie IV) $\big( b) ⟹ a) \big)$.

---

Résultat analogue à IV. 13) pour les $K’$-candidats :

Si $S$ et $S’$ sont des $K’$-candidats, $S ⟹ S’$ reste un $K’$-candidat.

Soient $S$ et $S’$ des $K’$-candidats. Montrons que $S ⟹ S’$ est un $K’$-candidat.

1. $S ⟹ S’$ est saturé

En effet : on applique l’analogue de la question 11, puisque $S’$ est saturé (car $S’$ est un $K’$-candidat).

2. $S’_0 ⊆ S ⟹ S’$

Si $x u_1 ⋯ u_n ∈ S’_0$, montrons que $x u_1 ⋯ u_n ∈ S ⟹ S’$.

Soit $v∈S$.

Comme $S ⊆ S_l$ (car $S$ est un $K’$-candidat), $v$ est normalisable par la gauche.

En outre, $x u_1 ⋯ u_n ∈ S’_0$ implique que tous les $u_i$ le sont aussi, donc $x u_1 ⋯ u_n v ∈ S_0$.

Montrons que $x u_1 ⋯ u_n v ∈ S’$.

C’est le cas puisque $S_0 ⊆ S’$ (car $S’$ est un $K’$-candidat) et :

\[x u_1 ⋯ u_n v ∈ S_0 ⊆ S'\]

3. $S ⟹ S’ ⊆ S_l$

Si $u∈S ⟹ S’$, montrons que $u∈S_l$.

Comme $u∈S ⟹ S’$ et $S’ ⊆ S_l$ (car $S’$ est un $K’$-candidat) :

\[∀v∈S, uv∈S' ⊆ S_l\]

Par conséquent, pour toute variable $x∈S$ : $ux$ a une réduction gauche finie, ce qui implique, par contraposée de l’analogue de la question 12, que $u$ aussi, c’est-à-dire que $u∈S_l$.

Or, il existe une variable $x∈S$ puisque $\underbrace{S \supseteq S'_0 }_{\rlap{\text{car } S \text{ est un } K'\text{-candidat}}} \supseteq Var$ : donc

\[u∈S_l\]

---

Les $K’$-candidats sont donc clos par $⟹$ et par intersection (trivialement, puisque les conditions à vérifier sont quantifiées universellement).

Ces résultats de stabilité nous permettent dès lors de définir $I’(d)$ de la même manière que dans la partie IV., et les résultats analogues à ceux des questions IV.14) et IV.15) s’ensuivent (en remplaçant “${\cal E}_C ⟦t⟧𝜌 ≠ ∅$” par “${\cal E}_C ⟦t⟧𝜌$ contient un élément strict” dans IV.15)).

$3. ⟹ 1.$

C’est immédiat.