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))

  • $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