“doc” (Col. : Science Sup 17x24) — 2007/7/19 — 18:18 — page 131 — #141
i
i
i
i
i
i
i
i
3.4 La programmation avec la récursion
131
où length(L) donne la longueur de la liste L. Nous soupçonnons que P((i, Ys)) est un
invariant d’état. Nous utilisons l’induction pour le prouver :
– D’abord nous vérifions P(S 0 ). C’est une conséquence directe de S 0 = (0, Xs).
– En supposant P(S i ) et S i n’est pas l’état final, il faut prouver P(S i+1 ). C’est
une conséquence de la sémantique de l’instruction case et l’appel de fonction.
Nous avons S i = (i, Ys). Nous ne sommes pas dans l’état final, Ys a donc une
longueur non zéro. D’après la sémantique, I+1 ajoute 1 à i et l’instruction case
enlève un élément de Ys. En conséquence, P(S i+1 ) est vrai.
Comme Ys est réduit d’un élément à chaque appel, nous arrivons tôt ou tard à l’état
final S final = (i, nil), et la fonction renvoie i. Comme length(nil) = 0 et P(S final )
est vraie, nous déduisons que i = length(Xs).
L’étape difficile dans cette preuve est le choix de la propriété P. Elle doit satisfaire
deux contraintes. D’abord, elle doit combiner les arguments du calcul itératif de telle
façon que le résultat ne change pas pendant le calcul. Ensuite, elle doit être assez forte
pour que l’exactitude soit une conséquence de P(S final ). Une bonne règle pour trouver
P est d’exécuter le programme à la main pour quelques cas simples, et de formuler à
partir de ces résultats le cas intermédiaire général.
f) La construction des programmes en suivant le type
Ces exemples de fonctions sur les listes ont tous une propriété curieuse. Ils ont tous
un argument de liste, List T, qui est défini comme :
List T : := nil
| T ´|´ List T
et ils ont tous une instruction case qui a la forme :
case Xs of nil then expr % Cas de base
[] X|Xr then expr end
% Appel r´ ecursif
Que se passe-t-il ici ? La structure récursive des fonctions sur les listes suit exactement
la structure récursive de la définition du type. Nous verrons que c’est presque toujours
vrai pour les fonctions sur les listes.
Nous pouvons utiliser cette propriété pour nous aider à écrire des fonctions
récursives. Cela peut énormément faciliter le travail quand les définitions des types
deviennent compliquées. Par exemple, définissons une fonction qui compte le nombre
d’éléments dans une liste imbriquée. Une liste imbriquée (« nested list ») est une liste
dans laquelle chaque élément peut lui-même être une liste, comme [[1 2] 4 nil
[[5] 10]]. Nous définissons le type NestedList T comme ceci :
NestedList T : := nil
| |NestedList T ´|´ NestedList T
| T ´|´ NestedList T
© Dunod – La photocopie non autorisée est un délit
i
i
i
i
i
i
i
i
3.4 La programmation avec la récursion
131
où length(L) donne la longueur de la liste L. Nous soupçonnons que P((i, Ys)) est un
invariant d’état. Nous utilisons l’induction pour le prouver :
– D’abord nous vérifions P(S 0 ). C’est une conséquence directe de S 0 = (0, Xs).
– En supposant P(S i ) et S i n’est pas l’état final, il faut prouver P(S i+1 ). C’est
une conséquence de la sémantique de l’instruction case et l’appel de fonction.
Nous avons S i = (i, Ys). Nous ne sommes pas dans l’état final, Ys a donc une
longueur non zéro. D’après la sémantique, I+1 ajoute 1 à i et l’instruction case
enlève un élément de Ys. En conséquence, P(S i+1 ) est vrai.
Comme Ys est réduit d’un élément à chaque appel, nous arrivons tôt ou tard à l’état
final S final = (i, nil), et la fonction renvoie i. Comme length(nil) = 0 et P(S final )
est vraie, nous déduisons que i = length(Xs).
L’étape difficile dans cette preuve est le choix de la propriété P. Elle doit satisfaire
deux contraintes. D’abord, elle doit combiner les arguments du calcul itératif de telle
façon que le résultat ne change pas pendant le calcul. Ensuite, elle doit être assez forte
pour que l’exactitude soit une conséquence de P(S final ). Une bonne règle pour trouver
P est d’exécuter le programme à la main pour quelques cas simples, et de formuler à
partir de ces résultats le cas intermédiaire général.
f) La construction des programmes en suivant le type
Ces exemples de fonctions sur les listes ont tous une propriété curieuse. Ils ont tous
un argument de liste, List T, qui est défini comme :
List T : := nil
| T ´|´ List T
et ils ont tous une instruction case qui a la forme :
case Xs of nil then expr % Cas de base
[] X|Xr then expr end
% Appel r´ ecursif
Que se passe-t-il ici ? La structure récursive des fonctions sur les listes suit exactement
la structure récursive de la définition du type. Nous verrons que c’est presque toujours
vrai pour les fonctions sur les listes.
Nous pouvons utiliser cette propriété pour nous aider à écrire des fonctions
récursives. Cela peut énormément faciliter le travail quand les définitions des types
deviennent compliquées. Par exemple, définissons une fonction qui compte le nombre
d’éléments dans une liste imbriquée. Une liste imbriquée (« nested list ») est une liste
dans laquelle chaque élément peut lui-même être une liste, comme [[1 2] 4 nil
[[5] 10]]. Nous définissons le type NestedList T comme ceci :
NestedList T : := nil
| |NestedList T ´|´ NestedList T
| T ´|´ NestedList T
© Dunod – La photocopie non autorisée est un délit