Cours 1: Algèbre initiale

Algèbre intiale (pour un foncteur)

Soit $ℂ$ une catégorie et $F : ℂ ⟶ ℂ$ un foncteur.

Une $F$ -algèbre:: est une paire $(A, α)$ où $A \in ℂ$ et $α : F A ⟶ A$
Un morphisme de $F$ -algèbres $(A, α) ⟶ (B, β)$ :: est un morphisme $f : A ⟶ B$ tq le diagramme suivant commute: $F A α F f A f F B β B$

On note $A l g (F)$ la catégorie des $F$ -algèbres.

Algèbre initiale pour $F$ :: un objet initial de $A l g (F)$ : $(Z, ζ)$ , avec $ζ : F Z ⟶ Z$ tel que $\forall (A, α)$ $F$ -algèbre $\exists! i_{A} : (Z, ζ) ⟶ (A, α)$

Prop: Soit $(Z, ζ)$ une $F$ -alg initiale. Alors $(F Z, F ζ) ≃ (Z, ζ)$

NB: en un certain sens, c’est le plus petit point fixe de $F$ .

Structures libres

Structure libre:

est un $n$ -uplet $(T, c_{1}, \dots, c_{n})$ où

$T \in S e t$
$c_{i} : θ_{i} (T) ⟶ T$ pour des foncteurs $θ_{1}, \dots, θ_{n} : S e t ⟶ S e t$ donnés

tq $(T, [c_{1}, \dots, c_{n}])$ est la $(θ_{1} + \dots + θ_{n})$ -algèbre initiale

Co-pairing de $f : A ⟶ C, g : B ⟶ C$ :

$[f, g] : A + B ⟶ C$ (définition par cas, fonction donnée par la propriété universelle du coproduit)

Donc $[c_{1}, \dots, c_{n}] : \underset{≝ (θ_{1} + \dots + θ_{n}) (T)}{\underset{⏟}{θ_{1} (T) + \dots + θ_{n} (T)}} ⟶ T$

En théorie des types: $θ_{i} (X) ≝ θ_{i}^{k_{1}} (X) \times \dots \times θ_{i}^{k_{i}} (X)$

Que signifie le caractère initial?

Point fixe:

T ≃ (θ_{1} + \dots + θ_{n}) (T)

Donc tout $x \in T$ s’écrit $c_{i} (y) \in θ_{i} (T)$ où $i \in {1, \dots, n}$ et $y \in T$ sont uniques.

Ex:

$θ_{1} ≝ i d : S e t ⟶ S e t$
$θ_{2} ≝ 1 : S e t ⟶ S e t$

(θ_{1} + θ_{2}) (A) = (i d + 1) (A) = \underset{A plus un autre élément ⋆}{\underset{⏟}{A + 1}}

Algèbre initiale: l’ensemble $ℕ$

$θ_{2}$ est le constructeur zéro
$θ_{1}$ est le constructeur successeur

Clôture par $i d + 1$ ⟹ on a tous les entiers

Les entiers dans le système F

N a t ≝ \forall X . (X \to X) \to X \to X

Lemme: les termes normaux de type $N a t$ sont de la forme

$\underset{―}{n} ≝ Λ X . λ s^{X \to X} . λ z^{X} . s^{n} (z)$
c’est-à-dire les entiers de Church!
ou l’identité $Λ X . λ f^{X \to X} . f ≃_{η} Λ X . λ f^{X \to X} . λ x^{X} . f x$

Rappel: $η$ -équivalence:: $M ≃_{η} λ x . M x$

Système T

\begin{matrix} M, N := x ∣ λ x . M ∣ M N ∣ 0 ∣ S N ∣ if z then P else x . M \\ ∣ ⟨ M, N ⟩ ∣ π_{i} M ∣ iter (N, x . M, P) \end{matrix}

où

$iter (0, M, P) ⟶ P$
$iter (S N, M, P) ⟶ M [iter (N, M, P) / x]$

i.e.

\frac{Γ ⊢ N : N a t Γ, x : A ⊢ M : A Γ ⊢ P : A}{Γ ⊢ i t e r (N, x . M, P) : A}

Système T dans le système F

\frac{}{Γ ⊢ \underset{―}{0} : N a t}

c’est clair car tous les entiers de Church sont de type $N a t$

\frac{Γ ⊢ N : N a t}{Γ ⊢ S N : N a t}

Vérifions que

s u c c ≝ λ n^{N a t} . (Λ X . λ s^{X \to X} . λ z^{X} . n X s (s z)) : N a t ⟶ N a t

\frac{Γ ⊢ N : N a t Γ ⊢ s u c c : N a t \to N a t}{Γ ⊢ s u c c N : N a t}

$\underset{―}{0} A (λ x^{A} . M) P : P$
$\begin{matrix} \underset{―}{n + 1} A (λ x^{A} . M) P ⟶^{*} (λ x^{A} . M) (\dots (λ x^{A} . M) P) \dots) \\ ⟶ (λ x^{A} . M) (i t e r (n, M, P)) ⟶ M [i t e r (n, M, P) / x] \end{matrix}$

p r e d ≝ λ n^{N a t} . π_{1} (n (N a t \times N a t) (λ p^{N a t \times N a t} . ⟨ π_{2} p, s u c c (π_{2} p) ⟩) ⟨ 0, 0 ⟩)

b o o l ≝ \forall X . X \to X \to X

\frac{Γ ⊢ b : b o o l Γ ⊢ P : A Γ ⊢ M : A}{Γ ⊢ if b then P else M : A}

\begin{matrix} t r u e ≝ Λ X . λ x^{X} . λ y^{X} . x \\ f a l s e ≝ Λ X . λ x^{X} . λ y^{X} . y \\ if b then P else M ≝ b A P M \end{matrix}

i s Z e r o ≝ λ n^{N a t} . n B o o l (λ k^{B o o l} . f a l s e) t r u e : N a t \to B o o l

Puis: règle du “if zero”

Donc système F contient le système T.

Par un argument diagonal: un langage de programmation total ne peut pas exprimer toutes les fonctions récursives totales.

Système de réécriture (faiblement) normalisant:: ssi pour tout $M$ , il existe $N$ normal (plus de réduction possible) tq $M ⟶^{*} N$ (mais: il se pourrait qu’il existe une stratégie de réduction qui ne termine pas)

Ex: $λ$ -calcul pas normalisant ⟹ cf. $Ω ≝ δ δ ≝ (λ x . x x) (λ x . x x) ⟶ Ω ⟶ \dots$

Gödel a introduit le système T pour réduire la cohérence de l’arithmétique de Peano à la normalisation de ce système

Gödel: Normalisation du système T ⟹ cohérence de PA

Fortement normalisant:: ssi il n’existe pas de chemin de réécriture infini partant de $M$ (le graphe de réduction de tout terme est fini)
Confluence:: il existe au plus une forme normale.

Girard: Normalisation (faible) du système F ⟹ cohérence de $P A_{2}$

En fait: systèmes T et F sont fortement normalisants, mais on ne va montrer que leur normalisation faible.

Système de réécriture du système F

$(λ x^{A} . M) N ⟶ M [N / x]$
$(Λ X . M) A ⟶ M [A / X]$

La deuxième règle ne “fait rien”, on peut la vérifier sans à l’extérieur du système F.

Réductibilité (Tait)

$λ$ -calcul simplement typé ⟶ logique propositionelle

Types pour le $λ$ -calcul simplement typé:: $A, B := X ∣ A \to B$

Candidats de réductibilité

On définit un prédicat sur les types: l’ensemble des termes réductibles de type $A$ .

\begin{matrix} R e d (X) ≝ W N_{X} ≝ {M : X ∣ M normalisant} (WN = weakly normalisable) \\ R e d (A \to B) ≝ {M : A \to B ∣ \forall N \in R e d (A), M N \in R e d (B)} \end{matrix}

Un terme est neutre:: s’il n’est pas une abstraction (soit une variable, soit une application)

NB: on ne crée pas de nouveaux rédex quand on remplace les termes neutres par une variable

N N_{A} ≝ {M : A ∣ M normal et neutre}

Lemme 1: Pour tout type $A$ ,
$N N_{A} \subseteq R e d (A) \subseteq W N_{A}$

Lemme 2 (Adéquation):

Si $x_{1} : C_{1}, \dots, x_{n} : C_{n} ⊢ M : A$ est dérivable, alors pour tout $i \in {1, \dots, n}$ , $N_{i} \in R e d (C_{i})$ , on a $M [N_{1} / x_{1}, \dots, N_{n} / x_{n}] \in R e d (A)$

Attention: pour démontrer l’adéquation, on fait une induction qui dépend de types arbitrairement complexes ⟶ pas de borne sur les formules sur lesquelles on applique l’induction ⟹ ne marchera pas pour le système T à l’intérieur du système T (mais fonctionne dans le système F, au second ordre).

Conséquence: le $λ$ -calcul simplement typé est faiblement normalisant, puisque que c’est le cas de toutes les variables, et on conclut par induction.

Pour le système F

R e d (\forall X . A) ≝ {M : \forall X . A ∣ \forall B, M B \in R e d (A [B / X])}

MAIS: définition circulaire !!! Pas bien fondée ⟶ $A [B / X]$ n’est pas “plus petit” que $A$

Share on

Twitter Facebook Google+ LinkedIn