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 ∈ ℂ$ et $α: FA ⟶ A$

Un morphisme de $F$-algèbres $(A, α) ⟶ (B, β)$:

est un morphisme $f: A ⟶ B$ tq le diagramme suivant commute: \(\begin{xy} \xymatrix{ FA \ar[r]^\alpha \ar[d]_{Ff} & A \ar[d]^f \\ FB \ar[r]_\beta & B } \end{xy}\)

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

Algèbre initiale pour $F$:

un objet initial de $Alg(F)$: $(Z, ζ)$, avec $ζ: FZ ⟶ Z$ tel que $∀(A, α)$ $F$-algèbre $∃! i_A: (Z, ζ) ⟶ (A, α)$

Prop: Soit $(Z, ζ)$ une $F$-alg initiale. Alors \((FZ, 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, ⋯, c_n)$ où

  • $T ∈ Set$
  • $c_i: θ_i(T) ⟶ T$ pour des foncteurs $θ_1, ⋯, θ_n: Set ⟶ Set$ donnés

tq $(T, [c_1, ⋯, c_n])$ est la $(θ_1 + ⋯ + θ_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, ⋯, c_n]: \underbrace{θ_1(T) + ⋯ + θ_n(T)}_{≝ (θ_1 + ⋯ + θ_n)(T)} ⟶ T$

En théorie des types: \(θ_i(X) ≝ θ_i^{k_1}(X) × ⋯ × θ_i^{k_i}(X)\)

Que signifie le caractère initial?

Point fixe:

\[T ≃ (θ_1 + ⋯ + θ_n)(T)\]

Donc tout $x ∈ T$ s’écrit $c_i(y) ∈ θ_i(T)$ où $i ∈ \lbrace 1, ⋯, n \rbrace$ et $y∈T$ sont uniques.

Ex:

  • $θ_1 ≝ id: Set ⟶ Set$
  • $θ_2 ≝ 1: Set ⟶ Set$
\[(θ_1+θ_2)(A) = (id+1)(A) = \underbrace{A+1}_{A \text{ plus un autre élément } \star}\]

Algèbre initiale: l’ensemble $ℕ$

  • $θ_2$ est le constructeur zéro
  • $θ_1$ est le constructeur successeur

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

Les entiers dans le système F

\[Nat ≝ ∀X. (X → X) → X → X\]

Lemme: les termes normaux de type $Nat$ sont de la forme

  1. \[\underline{n} ≝ ΛX. λs^{X→X}. λz^X. s^n(z)\]

    c’est-à-dire les entiers de Church!

  2. ou l’identité \(ΛX. λf^{X→X}. f ≃_η ΛX. λf^{X→X}. λx^X. f x\)
Rappel: $η$-équivalence:
\[M ≃_η λx. M x\]

Système T

\[M, N := x \mid λx. M \mid MN \mid 0 \mid SN \mid \texttt{if } z \texttt{ then } P \texttt{ else } x.M\\ \mid ⟨M, N⟩ \mid π_i M \mid \texttt{iter}(N, x. M, P)\]

où

  • $\texttt{iter}(0, M, P) ⟶ P$

  • $\texttt{iter}(SN, M, P) ⟶ M[\texttt{iter}(N, M, P)/x]$

i.e.

\[\cfrac{Γ ⊢ N: Nat \qquad Γ,x:A ⊢ M: A \qquad Γ ⊢ P: A}{Γ ⊢ iter(N, x.M, P): A}\]

Système T dans le système F

\[\cfrac{}{Γ ⊢ \underline{0}: Nat}\]

c’est clair car tous les entiers de Church sont de type $Nat$

\[\cfrac{Γ ⊢ N: Nat}{Γ ⊢ SN: Nat}\]

Vérifions que

\[succ ≝ λn^{Nat}. (ΛX. λs^{X→X}. λz^X. n \, X \, s\, (sz)): Nat ⟶ Nat\] \[\cfrac{Γ ⊢ N: Nat \qquad Γ ⊢ succ: Nat → Nat}{Γ ⊢ succ \, N: Nat}\]
  • \[\underline{0} \, A \, (λx^A.M) P: P\]
  • \[\underline{n+1} \, A \, (λx^A.M) P ⟶^\ast (λx^A.M) ( ⋯ (λx^A.M) P) ⋯) \\ ⟶ (λx^A.M) (iter(n, M, P)) ⟶ M[iter(n, M, P)/x]\]
\[pred ≝ λn^{Nat}. π_1 \Big(n \, (Nat × Nat) \, \big(λp^{Nat × Nat}. ⟨π_2 p, succ(π_2 \, p)⟩\big) ⟨0, 0⟩\Big)\] \[bool ≝ ∀X. X → X → X\] \[\cfrac{Γ ⊢ b: bool \qquad Γ ⊢ P:A \qquad Γ ⊢ M:A}{Γ ⊢ \texttt{if } b \texttt{ then } P \texttt{ else } M: A}\] \[true ≝ ΛX. λx^X. λy^X. x\\ false ≝ ΛX. λx^X. λy^X. y\\ \texttt{if } b \texttt{ then } P \texttt{ else } M ≝ b \, A \, P \, M\] \[isZero ≝ λn^{Nat}. n \, Bool \, (λk^{Bool}. false) \, true: Nat → Bool\]

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 ⟶^\ast N$ (mais: il se pourrait qu’il existe une stratégie de réduction qui ne termine pas)

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

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 $PA_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 \mid A → B\]

Candidats de réductibilité

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

\[Red(X) ≝ WN_X ≝ \lbrace M : X \mid M \text{ normalisant}\rbrace \qquad \text{(WN = weakly normalisable)}\\ Red(A → B) ≝ \lbrace M: A → B \mid ∀N∈Red(A), MN∈Red(B) \rbrace\]
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

\[NN_A ≝ \lbrace M: A \mid M \text{ normal et neutre} \rbrace\]

Lemme 1: Pour tout type $A$,

\[NN_A ⊆ Red(A) ⊆ WN_A\]

Lemme 2 (Adéquation):

Si $x_1: C_1, ⋯, x_n: C_n ⊢ M:A$ est dérivable, alors pour tout $i∈ \lbrace 1, ⋯, n\rbrace$, $N_i ∈ Red(C_i)$, on a \(M[N_1/x_1, ⋯, N_n/x_n] ∈ Red(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

\[Red(∀X. A) ≝ \lbrace M: ∀X.A \mid ∀B, MB ∈ Red(A[B/X]) \rbrace\]

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

Leave a comment