Cours 3: Candidats de réductibilité de Tait

Comment pallier le problème de définition circulaire des candidats de réductibilité $Red(∀X. A)$ ?

\[ρ: Var_2 ⟶ \underbrace{Candidats}_{\text{ensemble de termes}}\] \[Red(∀X. A) ≝ \lbrace M: ∀X. A \mid ∀B. MB ∈ Red(A[B/X]) \rbrace\]

est transformé en

\[Red_ρ(∀X. A) ≝ \lbrace M: ∀X. A \mid ∀\text{candidat } C, M ∈ Red_{ρ[X ⟼ C]}(A) \rbrace\]

NB: cette définition est bien fondée, car on va donner un ordre bien fondé sur les $Red_ρ(A)$ (c’est la taille de la formule $A$)

  • \[Red_ρ(X) ≝ ρ(X)\]
  • \[Red_ρ(A→B) ≝ \lbrace M \mid ∀N ∈ Red_ρ(A), MN∈Red_ρ(B) \rbrace\]

Lemme 0 (Clôture par extension (= anti-réduction)): Pour tout $A$, $M∈Red(A)$,

\[M' ⟶ M ⟹ M' ∈ Red(A)\]

Lemme 1: Pour tout $A$,

\[\underbrace{NN}_{\text{neutral normalizable}} ⊆ Red(A) ⊆ \underbrace{WN}_{\text{weakly normalizable}}\]

Lemme 2 (Adéquation):

\[x_1: C_1, ⋯, x_n: C_n ⊢ M: A \\ ⟹ ∀N_1 ∈ Red(C_1), ⋯, N_n ∈ Red(C_n), M[N_i/x_i]_i ∈ Red(A)\]

NB:

  • Pour l’adéquation, on utilise le lemme 0 + induction

  • pour conclure la normalisabilité du $λ$-calcul, on utilise le lemme 2 avec les $N_i = x_i$ (les variables sont neutres, donc normalisables par le lemme 1)

Candidats de réductibilité de Tait

Candidat de réductibilité $C$:

un ensemble $C$ tel que:

  • CR1: \(∀M ∈ C, M' ⟶ M ⟹ M' ∈ C\)
  • CR2: \(NN ⊆ C ⊆ \underbrace{WN}_{\text{weakly normalizable}}\)

si NN est l’ensemble des termes normaux et différents de $λx. M$ et $ΛX. M$

Termes normaux neutres forment une opérade ⟶ stables par substitution

Typage à la Church VS Typage à la Curry

Typage à la Church Typage à la Curry
Termes typés Termes typables
Typage à la Church:

les types apparaissent explicitement dans les termes (comme décorations des variables: $x^A, λx^A. M, …$)

Typage à la Curry:

on utilise des $λ$-termes “purs” (sans types à l’intérieur)

\[M, N ≝ x \mid λx. M \mid MN\]

et on donne des règles de typage pour définir les termes typables

Ex:

  • Curry: $λx.x: A ⟶ A$ pour tout $A$ (une infinité de types possibles)

  • Church: $λx^A.x: A ⟶ A$ (l’information du type est déjà contenue dans le terme: un seul type possible)

NB: Les deux présentations sont équivaentes, mais des fois, c’est plus ou moins facile d’utiliser l’une ou l’autre.

Ex:

  • pour les preuves de normalisation du système F, Curry est plus “léger” (pas de $ΛA. M$)

  • pour la théorie des types de Martin-Löf, Church est plus utilisé (ex: $\prod_{x:A} B(x)$)

Retour au système F

Expressivité du système F:

Représentable dans le système F ⟺ Totalement démontrable dans $PA_2$

$M: Nat ⟶ Nat$ représente une fonction de $ℕ ⟶ ℕ$

Dans le livre “Proofs and Types” (Girard, Lafont, Taylor), la direction $⟹$ est faite très rapidement

Typage à la Curry du système F

Dans la suite, on utilise le typage à la Curry.

\[x_1: C_1, ⋯, x_n:C_n ⊢ \underbrace{M}_{\text{pur}}:A\]

Dérivation de types $\sim$ règle de la déduction naturelle

VS: Pour Church: termes $\sim$ règles de la déduction naturelle

$λ$-calcul simplement typé

\[\cfrac{Γ, x:A}{x:A} (var)\] \[\cfrac{Γ, x:A ⊢ M: B}{Γ ⊢ λx.M: A → B} (abs)\]

(suite à écrire)

On peut gödeliser les $λ$-termes pour les traduire en entiers ⟶ on le fait de façon transparente

CR1 et CR2 deviennent des formules.

L’ensemble $X$ est clos par extension:
\[CR1(X) ≝ ∀x, y. X(x) ⟹ (y⟶x) ⟹ X(y)\]
L’ensemble $X$ vérifie $CR2$:
\[CR2(X) ≝ ∀x (NN(x) ⟹ X(x)) ∧ (X(x) ⟹ WN(x))\]

où

  • $NN(x)$ est la formule $Δ_0$: “$x$ est neutre et normal”

  • $WN(x) ≝ ∃y. N(y) ∧ x ⟶^\ast y$ est une formule $Σ_1$ (on ne peut pas borner la taille de la réduction)

L’ensemble $X$ est un candidat de réductibilité:
\[CR(X) ≝ CR1(X) ∧ CR2(X)\]
$x$ réalise $A$ (“est de type”):

On déf. la formule $x \Vdash A$ ($x$ réalise $A$) par induction sur $A$:

  • $x \Vdash X ≝ X(x)$

  • $x \Vdash A →B ≝ ∀y. y \Vdash A ⟹ \underbrace{xy}_{\text{application du } λ\text{-calcul}} \Vdash B$

  • $x \Vdash ∀X. A ≝ ∀X. CR(X) ⟹ x \Vdash A$

Fait: \(PA_2 ⊢ \underbrace{CR(WN)}_{≝ CR[WN/X]}\)

Preuve: car $WN$ est clos par extension, et $NN ⊆ WN ⊆ WN$

Lemme 1: Pour tout $A$, $\vec{X} ≝ fv(x \Vdash A) = fv(A)$

\[PA_2 ⊢ CR((x \Vdash A)[WN/\vec{X}])\]

Lemme (Adéquation): Soit $\vec{X} ≝ fv(C_1, ⋯, C_n, A)$. Alors

Si $x_1: C_1, ⋯, x_n:C_n ⊢ M:A$ dans le système F, alors pour tous $N_1, ⋯, N_n$,

\[PA_2, CR(\vec{X}), N_1 \Vdash C_1, ⋯, N_n \Vdash C_n ⊢_{NJ_2} M[N_1/x_1, ⋯, N_n/x_n] \Vdash A\]

Normalisation du système F

$x_1: C_1, ⋯, x_n:C_n$ sera noté $\vec{x}: Γ$

Si $\vec{x}:Γ ⊢ M:A$, avec le lemme 2 où les $N_i = x_i$:

\[PA_2, CR(\vec{X}), \vec{x}\Vdash Γ ⊢ M \Vdash A\]

Donc

\[PA_2, CR(WN), (\vec{x} \Vdash Γ)[WN/\vec{X}] ⊢ (M \Vdash A)[WN/\vec{X}]\]

et, comme on a déjà $PA_2 ⊢ CR(WN)$:

\[PA_2, (\vec{x} \Vdash Γ)[WN/\vec{X}] ⊢ (M \Vdash A)[WN/\vec{X}]\]

Puis, conséquence du lemme 1 et le premier point de $CR2$: $PA_2 ⊢ (\vec{x} \Vdash Γ)[WN/\vec{X}]$

\[PA_2 ⊢ (M \Vdash A)[WN/\vec{X}]\]

Et enfin, par le lemme 1 et le deuxième point de $CR2$:

\[PA_2 ⊢ WN(M)\]

NB: De même, on a $∀M \text{ sys T}$, \(PA_1 ⊢ WN(M)\)

Mais on ne peut pas mettre un “pour tout” devant: on utilise des schémas de compréhension pour l’ordre 2 $x \Vdash ∀X.A ≝ ∀X. CR(X) ⟹ x \Vdash A$ (induction pour l’ordre 1), mais la complexité des formules “réalise” devient arbitrairement grande pour le premier ordre (pas de souci pour $PA_2$) mais aussi pour le second ordre (à cause des candidats): aïe !

⟹ On ne peut pas exprimer tout ça en une seule formule de $PA_2$ (on peut pour un terme fixé / un $Σ^n_k/Π^n_k$ fixé, mais pas pour tous)

Leave a comment