Re: Programmation Dynamique

Effectivement, le livre n'explique pas le lien entre CPS et élimination des coupures : celui-ci est plutôt le fruit d'une réflexion personnelle en faisant un raisonnement par analogie via la correspondance de Curry-Howard. Cela étant, c'est plus une réflexion informelle qu'autre chose et il se peut que je pousse l'analogie au-delà de ses limites acceptables (ce n'est pas mon domaine de spécialisation, je ne suis pas informaticien théoricien).

Je vais détailler le schéma de pensée qui m'a amené à cette conclusion. Que dit la règle des coupures en théorie de la démonstration ? Elle généralise le principe du modus ponens : si A alors B, or A donc B. La forme générale de la règle des coupures est donné en bas de la page 11 dans le livre sus-cité : si j'ai deux séquents dans lesquels une même proposition A se trouve dans les prémisses de l'un et dans les conclusions de l'autre, alors je peux produire un séquent dans lequel celle-ci a disparue en fusionnant les prémisses et les conclusions. En haut de la page 12, cette règle est exprimée sous la forme particulière du modus ponens : si j'ai une preuve P1 qui a pour conclusion la proposition A, puis une preuve P2 dont la conclusion est la proposition B et dont A fait partie des prémisses, alors je peux produire une preuve P3 de la proposition B dans laquelle A ne fait plus partie des prémisses. Ensuite, la règle d'élimination des coupures affirme qu'il est également possible de produire une preuve P4 de la proposition B directement sans faire intervenir la preuve P1 qui produit la conclusion A ni la preuve P2 qui produit la proposition B lorsqu'elle a la proposition A dans ses prémisses.

Maintenant passons dans le monde des programmes via la correspondance de Curry-Howard. Cette dernière nous dit que chacune des preuves Pi correspond à un programme et les formules qu'elles manipulent sont les types des objets des programmes. Ainsi la preuve P1 produit un objet de type A qui est consommé par la preuve P2 pour produire un objet de type B ce qui, par coupure, fournit un programme P3 qui produit un objet de type B mais qui dans son exécution (par son recours à P1) doit allouer sur le tas un objet de type A (qui sera à terme désallouer par le ramasse-miette) : le modus ponens est la règle de typage de l'application de fonction :

let app (f:'a->'b) (x:'a):'b = f x;;
val app : ('a -> 'b) -> 'a -> 'b = <fun>

Mais, la règle d'élimination des coupures nous dit qu'il est possible d'écrire un programme P4 qui se passe totalement de cette allocation. Prenons maintenant l'exemple donné par Pierre Chambart dans l'article de blog chez OCamlPro pour calculer le minimum et le maximum d'une liste :

let rec fold_left f init l =
 match l with
 | [] -> init
 | h :: t ->
 let acc = f init h in
 fold_left f acc t
let keep_min_max (min, max) v =
 let min = if v < min then v else min in
 let max = if v > max then v else max in
 min, max
let find_min_max l =
 match l with
 | [] -> invalid_arg "find_min_max"
 | h :: t ->
 fold_left keep_min_max (h, h) t

Les types de ces trois fonctions sont :

val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a = <fun>
val keep_min_max : 'a * 'a -> 'a -> 'a * 'a = <fun>
val find_min_max : 'a list -> 'a * 'a = <fun>

Icikeep_min_max joue le rôle de la preuve P1 (c'est un lemme qui est responsable d'allocation) et fold_left joue le rôle de la coupure qui produit la preuve P3 à savoir find_min_max. Puis dans la suite de l'article, en transformant son code via CPS, il produit la preuve P4 sans coupure find_min_max_k2 qui se passe d'allocation et qui aura la même fonction que la fonction find_min_max initiale si on lui passe comme continuation la fonction identité fun x -> x.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.