Pour énoncer le théorème, nous avons besoin de structures mathématiques spécifiques :
- Ensemble Partiellement Ordonné (Poset) : Un ensemble $D$ muni d’une relation d’ordre $\sqsubseteq$ (réflexive, antisymétrique, transitive).
- Ensemble Dirigé : Un sous-ensemble $X \subseteq D$ est dirigé si pour toute paire d’éléments $x, y \in X$, il existe un $z \in X$ qui les majore ($x \sqsubseteq z$ et $y \sqsubseteq z$). Une chaîne est un cas particulier d’ensemble dirigé où tous les éléments sont comparables.
- Ordre Partiel Complet (CPO) : Un poset $(D, \sqsubseteq)$ qui possède un plus petit élément (noté $\bot$, « bottom ») et dans lequel tout sous-ensemble dirigé (ou toute chaîne) admet une borne supérieure (le plus petit des majorants, noté $\bigsqcup$).
- Fonction Monotone et Continue : Une fonction $f: D \to D$ est monotone si $x \sqsubseteq y \implies f(x) \sqsubseteq f(y)$. Elle est continue (au sens de Scott) si elle préserve les bornes supérieures des ensembles dirigés : pour tout ensemble dirigé $X \subseteq D$, $f(\bigsqcup X) = \bigsqcup \{f(x) \mid x \in X\}$.
Soit $(D, \sqsubseteq)$ un ordre partiel complet (CPO) et $f: D \to D$ une fonction continue. Alors $f$ admet un plus petit point fixe, noté $lfp(f)$, qui est donné par la borne supérieure de la chaîne des itérations de $f$ à partir du plus petit élément $\bot$. $$ lfp(f) = \bigsqcup_{n \in \mathbb{N}} f^n(\bot) $$ où $f^0(\bot) = \bot$, $f^1(\bot) = f(\bot)$, $f^2(\bot) = f(f(\bot))$, etc.
Démonstration Détaillée
La démonstration se déroule en trois étapes : on construit un candidat, on montre que c’est un point fixe, puis on montre que c’est le plus petit.
Étape 1 : Construction d’une chaîne
On définit la suite $(x_n)_{n \in \mathbb{N}}$ par $x_n = f^n(\bot)$. Montrons que cette suite forme une chaîne, c’est-à-dire $x_n \sqsubseteq x_{n+1}$ pour tout $n$.
- Base (n=0) : On a $x_0 = \bot$. Par définition, $\bot$ est le plus petit élément de $D$, donc $\bot \sqsubseteq f(\bot)$, ce qui signifie $x_0 \sqsubseteq x_1$.
- Hérédité : Supposons que $x_k \sqsubseteq x_{k+1}$ pour un certain $k \ge 0$. Comme la fonction $f$ est monotone, l’application de $f$ préserve l’ordre : $f(x_k) \sqsubseteq f(x_{k+1})$. Par définition de la suite, cela signifie $x_{k+1} \sqsubseteq x_{k+2}$.
Par récurrence, la suite $(\bot, f(\bot), f^2(\bot), \dots)$ est bien une chaîne.
Étape 2 : Le candidat est un point fixe
Puisque $(D, \sqsubseteq)$ est un CPO et que l’ensemble $C = \{f^n(\bot) \mid n \in \mathbb{N}\}$ est une chaîne, sa borne supérieure existe. Posons $L = \bigsqcup_{n \in \mathbb{N}} f^n(\bot)$.
Nous utilisons maintenant la continuité de $f$. Une fonction continue préserve les bornes supérieures des chaînes : $$ f(L) = f\left(\bigsqcup_{n \in \mathbb{N}} f^n(\bot)\right) = \bigsqcup_{n \in \mathbb{N}} f(f^n(\bot)) = \bigsqcup_{n \in \mathbb{N}} f^{n+1}(\bot) $$ La chaîne $(f^{n+1}(\bot))_{n \in \mathbb{N}}$ est simplement la chaîne initiale à laquelle on a retiré le premier élément $\bot$. La borne supérieure reste la même. Donc : $$ \bigsqcup_{n \in \mathbb{N}} f^{n+1}(\bot) = \bigsqcup_{n \in \mathbb{N}} f^n(\bot) = L $$ Nous avons donc montré que $f(L) = L$. Le vecteur $L$ est bien un point fixe de $f$.
Étape 3 : Le point fixe est le plus petit
Soit $y$ un autre point fixe quelconque de $f$, c’est-à-dire $f(y)=y$. Nous devons montrer que $L \sqsubseteq y$. Pour cela, il suffit de montrer que $y$ est un majorant de tous les éléments de la chaîne $C$, car $L$ est le plus petit des majorants.
Montrons par récurrence que $f^n(\bot) \sqsubseteq y$ pour tout $n \in \mathbb{N}$.
- Base (n=0) : $f^0(\bot) = \bot$. Par définition, $\bot \sqsubseteq y$ pour tout $y \in D$.
- Hérédité : Supposons que $f^k(\bot) \sqsubseteq y$. Comme $f$ est monotone, on a $f(f^k(\bot)) \sqsubseteq f(y)$. Or, $f(y)=y$ (car $y$ est un point fixe), donc $f^{k+1}(\bot) \sqsubseteq y$.
Par récurrence, $y$ est bien un majorant de tous les $f^n(\bot)$. Puisque $L$ est la borne supérieure (le plus petit des majorants), on a nécessairement $L \sqsubseteq y$.
Ceci achève la démonstration : $L$ est le plus petit point fixe de $f$.
Implications en Informatique Théorique
Ce théorème est le fondement de la sémantique dénotationnelle. Une fonction récursive, comme la fonction factorielle, peut être vue comme le point fixe d’un opérateur (une fonction d’ordre supérieur). Par exemple, la fonction factorielle `fact` est la solution de l’équation : $$ \text{fact} = F(\text{fact}) \quad \text{où} \quad F(g)(n) = \begin{cases} 1 & \text{si } n=0 \\ n \times g(n-1) & \text{si } n>0 \end{cases} $$ Le théorème de Kleene garantit que cette équation a une solution bien définie (le plus petit point fixe), qui peut être construite par approximations successives à partir de la fonction « totalement indéfinie » (l’élément $\bot$).