Sémantique des Programmes Récursifs

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.

Exemple

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.

Point de Départ

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 (fi) 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.

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

  • x0 = ⊥
  • xi+1 = F(xi), i ∈ N

Démonstration

Admis.

Application aux Programmes Récursifs

Exemple

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 :

f0 =
f1 = F(f0) 1 si n=0,
non déf. si n>0
f2 = F(f1) 1 si n=0,
1*1 si n=1
non-déf. si n>1
f3 = F(f2) 1 si n=0,
1*1 si n=1
2*1*1 si n=2
non-déf. si n>2
fi+1 = </jsm> F(fi) 1 si n=0,
1*1 si n=1
i*(i-1)*…*2*1*1 si n=i
non-déf. si n>i

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

Exercice

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

Autre exemple

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 1)

  • 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

f0 =
f1 = F(f0) = a si b = 0
non. déf. sinon
f2 = F(f1) = a si b = 0
b si (a mod b) = 0
non. déf. sinon
f3 = F(f2) = a si b = 0
b si (a mod b) = 0
(a mod b) si (b mod (a mod b))=0
non. déf. sinon

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.

Programmes Récursifs sur la Structure de Liste

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 :

FIXME : 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 :

f0 =
f1 = F(f0 f1(x,y) = y si x est vide
non déf. sinon
dom(f1 = L∅ × L où L∅ est l'ensemble des listes vides
f2 = F(f1 f2(x,y) = y si x est vide
a::f1(z,y) si x=a::z. Or, f1(z,y) n'est définie que pour f1( [],y) donc f2(x,y) = a::y si x=[a]
non déf. sinon
dom(f2 = L1 × L où L1 est l'ensemble des listes de longueur ≤ 1
f3 = F(f2 f3(x,y) = y si x est vide
a::f2(z,y) si x=a::z
non déf. sinon
c'est à dire y si x vide
a::y si x=[a]
a::b::y si x =[a,b]
non déf. sinon
dom(f3) = L2 × L où L2 est l'ensemble des listes de longueur ≤ 2

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

1) exercice?

 
m1ilc/semantics_5.txt · Dernière modification: 2010/05/24 10:09 par suitable