TD sur la dérécursivation

Igor Stéphan 7 avril 1999

Références

[JFD95] Y. Bertrand J.-F. Dufourd, D. Bechmann. Spécification algébriques,

algorithmique et programmation. InterÉditions, 1995. La fonction qui renverse une liste est définie par :

renverse(l) = ; \begin{matrix}si vide ?(l) alors l \\ sinon conc(renverse(fin(l)), cons(premier(l), [])) \end{matrix}

La fonction est bien récursive simple :

\begin{aligned}f(x_{1}) & = & renverse(x_{1}) \\ p(x_{1}) & = & vide ?(x_{1}) \\ g(x_{1}) & = & x_{1} \\ h(r, x_{1}) & = & conc(r, cons(premier(x_{1}), [])) \\ s_{1}(x_{1}) & = & fin(x_{1}) \end{aligned}

La concaténation est associative et possède pour élément neutre [].

renverse(l) = ; \begin{matrix}soit (r, u) = \begin{matrix}init ( inter = [], n = l) \\ tant que ¬vide ?(n) \\ répéter ( (conc(cons(premier(n), []), inter), fin(n))) \end{matrix} \\ dans r \end{matrix}

conc(cons(premier(n), []), inter) = cons(premier(n), inter)

renverse_{rec}([a, b, c]) = conc(conc(conc(conc([], [c]), [b]), [a]), [])
renverse_{iter}([a, b, c]) = conc([c], conc([b], conc([a], [])))
conc(conc(conc(conc([], [c]), [b]), [a]), [])
cons(c, cons(b, cons(a, [])))

(inter_{1}, n_{1}) = ([], [a, b, c])
(inter_{2}, n_{2}) = (conc(cons(premier(n_{1}), []), inter_{1}), fin(n_{1}))
= ([a], [b, c])
(inter_{3}, n_{3}) = (conc(cons(premier(n_{2}), []), inter_{2}), fin(n_{2}))
= ([b, a], [c])
(inter_{4}, n_{4}) = (conc(cons(premier(n_{3}), []), inter_{3}), fin(n_{3}))
= ([c, b, a], [])