On considère une autre construction dans les langages de programmation, celle des programmes récursifs. Un programme récursif (fonction ou procédure) est récursivement associé à un nom. Le corps du programme fait explicitement référence à ce nom (c'est ce qu'on désigne par “appel récursif”).

On voit ici que la définition sémantique dénotationnelle des programmes récursifs pose le même genre de problème que pour l'itération. Dans la mesure où la sémantique d'un programme récursif, disons P, dépend de la sémantique de P, elle n'est pas compositionnelle. De ce point de vue, on peut considérer le cas de l'itération comme un cas particulier de celui des programmes récursifs, c'est le cas où l'appel récursif n'est suivi d'aucune autre opération, le cas de récursivité terminale.

Cas particulier de récursivité terminale.

pgcd(a,b) = if b>0 then pgcd(b, a mod b) else a

Version itérative (avec un sémantique dénotationnelle) :

while b>0 do
{  r:= a mod b;
   a:= b;
   b:=r
}

Le passage de la version récursive à la version itérative n'a pas été prouvé, et n'est pas aussi simple dans le cas général de récursivité non-terminale. On cherche à résoudre le problème général de la définition sémantique des programmes récursifs et cela permettra de prouver l'équivalence de programmes récursifs et itératifs.

La sémantique de l'itération est la limite d'une suite croissante de fonctions partielles (elles-même associées à des programmes). Idée : utiliser la limite d'une suite croissante de fonctions partielles mais qui ne sont pas explicitement asscoiées à des programmes. Donc, utiliser la limite d'une suite croissante de fonctions partielles (f_i) définies par une récurrence en appliquant une fonctionnelle F :

• f_0 = \bot
• f_{i+1} = F\left(f_i\right), i\in \mathbb{N}

On peut voir cette limite comme le point fixe de F, c'est à dire une fonction x qui vérifie x = F(x). L'existence de cette limite est soumise aux conditions sur F du théorème du point fixe.

Soit E un ensemble partiellement ordonné (≤) et tel que (E,≤ ) est inductif (en anglais, un CPO : complet partial order), i.e.

• E admet un plus petit élément (⊥) : ∀ x ∈ E, ⊥ ≤ x .
• Toute suite croissante d'éléments de E admet un plus petit majorant.

Si F est une fonction croissante sur E (∀ x,y ∈ E, x ≤ y ⇒ F(x)≤F(y)) alors l'équation X=F(X) admet une solution minimale dans (E,≤ ) et cette solution, appelée le plus petit point fixe de F, est la limite de la suite définie par

• x₀ = ⊥
• x_i+1 = F(x_i), i ∈ N

Admis.

Sémantique du programme de calcul de factorielle de n\in \mathbb{N}

facto(n) = if n=0 then 1 else n*facto(n-1)

Le CPO considéré est l'ensemble E des fonctions de N dans N, muni de (≤) l'ordre d'inclusion des domaines. Il reste à définir la fonctionnelle F et montrer qu'elle est croissante.

• F : E → E
• f : \mapsto F\left(f\right) définie par
  • F\left(f\right) : \mathbb{N}\rightarrow\mathbb{N}
  • n \mapsto 1 si n=0
  • n \mapsto n*f\left(n-1\right) si n > 0

Démontrons que cette F est croissante. Soient f, g ∈ E telles que f ≤ g selon l'ordre d'inclusion des domaines. Il faut montrer que F(f) ≤ F(g). Soit n\in dom\left(F\left(f\right)\right).

• si n=0 alors n\in dom\left(F\left(g\right)\right) et F(g)(n) = 1 = F(f)(n)
• si n>0 alors n\in dom\left(F\left(g\right)\right)
  • si n > 0 et alors n\in dom\left(F\left(f\right)\right) alors
  • n-1 ∈ dom(f) par définition de F(f)
  • donc n-1 ∈ dom(g) car f ≤ g
  • donc n-1 ∈ dom(F(g)) par définition de F(g)
• F(g)(n) = n*g(n-1) = n*f(n-1) = F(f)(n) donc on a bien F(f) ≤ F(g) ⇒ croissante.

Ainsi, la sémantique du programme facto est définie par le plus petit point fixe de F, c'est à dire la limite de la suite de fonctions suivantes :

Cette limite est la fonction définie pour tout i ∈ N par f(i) = i!.

Vérifier que cette sémantique est la même que celle du programme itératif :

i:=0; f:=1
while i < n do
{
    i:=i+1; f:=f*i;
}
return f

Sémantique due programme du calcul du pgcd.

pgcd(a,b) = if b>0 then pgcd(b, a mod b)
                   else a
                  

Le CPO considéré est l'ensemble E des fonctions de \mathbb{N}^2 \rightarrow \mathbb{N}. La fonctionnelle F suivante est croissante ¹⁾

• F : E → E
  • f \mapsto F\left(f\right) définie par
  • F\left(f\right) : \mathbb{N}^2 \rightarrow \mathbb{N}
    • \left(a,b\right) \mapsto a \text{ si } b=0,f\left(b, a\; mod\; b\right) \text{ si } b>0

Donc la sémantique du programme pgcd est définie par le plus petit point fixe de F, c'est à dire la limite de la suite des fonctions

D'après Euclide, cette limite est la fonction définie, le pgcd(a,b) pour le couple (a,b)∈ N. On peut montrer que cette sémantique est la même que celle de la version itérative. On démontre ainsi l'équivalence des deux versions.

Il s'agit ici de définir la sémantique de programmes récursifs sur des structures dynamiques, dont les listes linéaires sont des exemples classiques : on se contentera d'une définition intuitive de type liste pour se concentrer sur le problème.

Exemple : concaténation de deux listes, exprimée par un programme en OCAML :

let rec concat x y = match (x) with 
  [] -> y
  | a::z -> a::(concat z y);;
 

Le CPO considéré est l'ensemble E des fonctions de L×L → L où L est l'ensemble des listes. La fonctionnelle est :

• F : E → E
  • f\mapsto F\left(f\right) définie par
    • F\left(f\right):L^2 \rightarrow L
    • \left(x,y\right) \mapsto y si x est vide
    • \left(x,y\right) \mapsto a::f\left(z,y\right) si x = a::z

Montrons que F est croissante :

… : démo à rajouter

Ainsi, la sémantique du programme concat est définie par le plus petit point fixe de F, la limite de la suite de fonctions :

En conclusion, ces exemples classiques ont une sémantique ainsi définie par application du Théorème du Point Fixe, lorsque la fonctionnelle est croissante. C'est à dire, si un calcul est fonctions antérieurs et ne les remets pas en cause.

Le lien entre la sémantique dénotationnelle des programmes récursifs et la sémantique opérationnelle du λ-calcul enrichi (combinateur Y). La syntaxe du λ-calcul permet d'exprimer et d'évaluer des programmes récursifs.

Exemple : calcul de la factorielle dans le λ-calcul enrichi. Définition récursive à l'aide d'une fonctionnelle F :

F = λf.λn.(con(zero?n) 1 (*n(f(pred n)))

facto = YF

où Y est le combinateur de point fixe qui vérifie YF = F(YF).

facto 2
= Y F 2 = F(Y F) 2
= cond(zero?2) 1 (* 2 ( Y F ( pred 2)))
= (* 2 (Y F 1))
= ( * 2 (cond(zero?1) 1 (* 1 (YF(pred 1))))
= ( * 2 ( * 1 (YF 0)))
= (* 2 (* 1 (cond(zero?0) 1 (* 0 (YF(pred 0 ))))))
= (* 2 ( * 1 1)) = 2

III. Preuves de correction des programmes