Cerise.moe

Candidats de réducibilité

Les candidats de réducibilité sont une méthode permettant d'effectuer des preuves de normalisation en théorie des types, pour peu que la métathéorie soit assez puissante.

L'idée générale est de donner une sémantique R mélangée à de la syntaxe — comme en réalisabilité. Étant donné un type A, R(A) sera l'ensemble des termes syntaxiques de type A qui normalisent. Mais, comme notre sémantique est un minimum honnête, elle est définie inductivement sur les types. Vient alors un « lemme d'interprétation » qui permet de prouver inductivement que R(A) est clos par […]

Trois exemples, du plus simple au plus complexe :

Ce framework est souple, et ne demande pas automatiquement toute la puissance de ZFC : la preuve de normalisation pour le premier système ne nécessite que EM et la capacité de raisonner au second ordre de manière prédicative, tandis les deux suivantes ont crucialement besoin d'imprédicativité.

Types intersection idempotents

Présentation du système

Il s'agit d'une manière de typer le lambda-calcul pur. Le système de types est donné par

A ::= X
    | ⋂ Aᵢ → B

Les contextes sont donnés par

Γ ::= •
    | Γ, x : ⋂ Aᵢ

Et les règles de typage sont

———————————————————— (ax)
Γ, x : ⋂ Aᵢ ⊢ x : Aⱼ

 Γ, x : ⋂ Aᵢ ⊢ t : B
————————————————————— (abs)
Γ ⊢ λx . t : ⋂ Aᵢ → B

Γ ⊢ t : ⋂ Aᵢ → B      Δᵢ ⊢ u : Aᵢ
————————————————————————————————— (app)
      Γ ∪ ⋃ Δᵢ ⊢ t u : B

Par une induction immédiate, ce système vérifie la réduction du sujet : si t ↝ u, alors t : A implique u : A.
Mais, phénomène plus rare, il vérifie également l'expansion du sujet : u : A implique t : A. L'idée pour le cas de la β-réduction (λx.t) u ↝ t[u/x] est que si t[u/x] : A, alors chaque occurence de u substituée (possiblement aucune) va être typée par un type Aᵢ. On va alors donner le type ⋂ Aᵢ à u.

Cela implique immédiatement que tout terme normalisant pour la réduction de tête (HN) est typable : on type les formes normales de tête et on utilise l'expansion du sujet pour remonter.
Les candidats de réducibilité vont permettre de montrer la direction inverse : tout terme typable est HN.

Sémantique

On définit la sémantique de manière inductive :

       R(A) = { t : A | t est HN }
R(⋂ Aᵢ → B) = ⋂ R(Aᵢ) → B
            = { t | ∀ u ∈ ⋂ R(Aᵢ), t u ∈ B }

En travaillant dans un « contexte » qui accorde une infinité de variables de chaque type.

Lemme 0 (saturation) : R(A) est clos par anti-réduction

Preuve par induction sur A :

Lemme 1 : HN₀(A) ⊆ R(A) ⊆ HN(A)

Où HN₀(A) est l'ensemble des termes des type A qui HN en un terme de la forme x t₁ … tₙ.

Première inclusion par induction sur A :

Seconde inclusion par induction sur A :

Lemme 2 : stabilité forte de R par substitution

Si x₁ : ⋂ Aᵢ , … , xₙ : ⋂ Aᵢ ⊢ t : B
Et u₁ ∈ R(⋂ Aᵢ) … uₙ ∈ R(⋂ Aᵢ), alors t[u₁/x₁ … uₙ/xₙ] ∈ R(B)

Preuve par induction sur la dérivation :

Maintenant, si on spécialise notre lemme 2 au contexte vide, on obtient que tout terme t de type A est dans R(A). Et par le lemme 1, on obtient que t est HN.

Donc la typabilité caractérise la normalisation de tête. On en déduit immédiatement que la typabilité est indécidable.

Système F

Présentation du système

Les types sont décrits par

A ::= X
    | A → B
    | ∀X,A

Les abstractions sont annotées par le type, et on rajoute des annotations pour binder les types

t ::= x
    | λ(x:A).t
    | t u
    | ΛX.t
    | t A

Les contextes sont simplement

Γ ::= •
    | Γ, x:A

Les règles de typage deviennent alors

—————————————— (ax)
Γ, x:A ⊢ x : A

 Γ, x:A ⊢ t : B
———————————————— (abs)
Γ ⊢ λx.t : A → B

Γ ⊢ t : A → B       Δ ⊢ u : A
————————————————————————————— (app)
       Γ, Δ ⊢ t u : B

Γ ⊢ t : A     X ∉ Γ
——————————————————— (abs2)
  Γ ⊢ ΛX.t : ∀X,A

  Γ ⊢ t : ∀X,A
———————————————— (app2)
Γ ⊢ t B : A[B/X]

Il est bien connu que ce système est très expressif, il permet en particulier de typer Δ := λx.xx avec par exemple
⊢ λ (x : ∀X, X → X) . (x (A → A)) (x A) : A → A

L'imprédicativité donne automatiquement des types inductifs faibles : produits, sommes, entiers, listes…     ℕ := ∀X, X → (X → X) → X
A + B := ∀X, (A → X) → (B → X) → X
A × B := ∀X, (A → B → X) → X

En fait, une fonction peut être typée dans système F si et seulement si on peut prouver qu'elle est totale dans PA2. Tant d'expressivité rend la typabilité dans système F indécidable.

Sémantique

TODO

Calcul des constructions

Présentation du système

Il existe plusieurs moyens de présenter CC. Je prends le parti ici de séparer les termes et les types, parce que j'ai l'habitude de raisonner en termes de catégories. Toutefois, l'imprédicativité de CC rend les choses un peu houleuses…
En effet, on aimerait avoir un « petit » univers explicite (Ω) qui correspond à l'objet des codes ainsi qu'un univers implicite correspondant aux objets de la catégorie, représenté par le jugement Γ ⊢ A Type.
Toutefois, si cela est simple dans le cas prédicatif, ici on veut pouvoir construire un code pour Ω → A. Donc il faut avoir un code pour Ω, qui vit dans un « grand » univers de codes U.

Les termes et les types sont décrits par une induction mutuelle :

A ::= X
    | Ω
    | U
    | (x:A) → B
    | El t

t ::= x
    | λ(x:A).t
    | (x:t) → u
    | Ω
    | t u

 

————————
⊢ U Type

———————
⊢ Ω : U

Γ ⊢ A Type    Γ, x:A ⊢ B Type
————————————————————————————— (Π-type)
    Γ ⊢ (x:A) → B Type

Γ ⊢ A : Ω/U    Γ, x:El A ⊢ B : U
———————————————————————————————— (Π-U)
       Γ ⊢ (x:A) → B : U

Γ ⊢ A : Ω/U    Γ, x:El A ⊢ B : Ω
———————————————————————————————— (Π-Ω)
       Γ ⊢ (x:A) → B : Ω

 Γ ⊢ t : Ω/U
—————————————
Γ ⊢ El t Type

  Γ ⊢ A Type
——————————————
Γ, x:A ⊢ x : A

Γ, x:A ⊢ t : B    Γ ⊢ (x:A) → B Type
————————————————————————————————————
      Γ ⊢ λ(x:A).t : (x:A) → B

Γ ⊢ t : (x:A) → B    Δ ⊢ u : A
——————————————————————————————
      Γ ⊢ t u : B[u/x]

Γ ⊢ A Type   Γ ⊢ B Type   Γ ⊢ t : A   A ≃ B
———————————————————————————————————————————
                 Γ ⊢ t : B

À cela, on doit rajouter des équations pour βη, pour que El d'un Π-terme corresponde au Π-type associé…