Programmation Avancée

TP5: combinatoire et continuations

Exercice conçu par David Baelde

On commencera par faire un bref point sur le problème des reines vu (brièvement pour la plupart d'entre vous) au TP précédent. En particulier, nous parlerons des styles de programmation destructif et persistant. Le but de ce TP est ensuite d'appliquer des transformations de programmes vues en cours pour dégager une discipline du programmation de haut-niveau pour la recherche combinatoire.

Exercice 1: le retour des reines

On reprend le problème des reines du TP précédent. On repartira par exemple de cette solution. Si votre propre solution est plutôt propre, je vous encourage à continuer avec.

Question 1

Transformer le code pour se débarasser de la construction for. Il ne devra rester que des appels de fonctions, des opérations sur les tableaux, et bien sûr la séquence.

Question 2

Transformer le code en style de passage par continuation. L'itérateur reines devra avoir le type (int array -> k -> unit) -> int -> k -> 'ak = unit -> 'a est le type des continuations. Tout appel de fonction devra être terminal. La séquence n'est donc autorisée qu'après une instruction élémentaire comme une update de tableau.

Exercice 2: double continuation

A priori, vous venez de re-découvrir ce qu'on appelle les "double-barrelled continuations", ou plus simplement "success/failure continuations".

L'idée générale permet de coder de façon modulaire et (plutôt) efficace des algorithmes de recherche avec backtracking. Intuitivement, la première continuation (correspondant à f dans reines f n k, et appelée continuation de succès) va permettre de "renvoyer" plusieurs résultats possibles. La seconde (correspondant à k, et appelée continuation d'échec) va permettre de pouvoir signaler quand il n'y a pas (ou plus) de solution possible; c'est par ce biais qu'on va implémenter le backtracking.

Par exemple, le calcul qui renvoie 1 ou 2 peut être représenté par fun success failure -> success 1 (fun () -> success 2 failure).

Plus formellement, on définit le type 'a t des calculs non déterministes renvoyant des valeurs de type 'a:

type cont = unit -> unit
type 'a success = 'a -> cont -> unit
type failure = cont
type 'a t = 'a success -> failure -> unit

Un calcul non-déterministe qui prend des arguments de types t1 ... tn (non fonctionnels) et qui renvoie des valeurs de type r sera encodée par une fonction Caml de type t1 -> ... -> tn -> r t.

Dans ce style, on peut implémenter un certain nombre de combinateurs bien pratiques pour écrire naturellement des recherches combinatoires. Par exemple, considérons la recherche des décompositions d'un entier comme somme d'entiers strictement positifs. Si l'on se restreint aux solutions dont les facteurs de la somme vont décroissant, on peut décrire la recherche en la paramétrant par max et target, donnant respectivement l'entier maximum utilisable et ce qu'il nous manque pour atteindre la somme, avec max<=target. Cette recherche se décrit alors informellement comme "trouver une solution avec max:=max-1 OU trouver une solution pour target:=target-max ET on y rajoute max". Ceci s'écrit (assez) directement:

let rec f max target =
  if target = 0 then return [] else
    if max = 0 then fail else
      (* On met [max] dans la liste, ou pas. *)
      orelse
        (andthen
           (* Ajouter [max] à une solution pour [target-max].
              On met à jour max pour assurer max<=target. *)
           (f (min max (target-max)) (target-max))
           (fun l -> return (max::l)))
        (f (max-1) target)

Question

Votre mission est d'implémenter les combinateurs nécessaires pour faire passer le code précédent. Le combinateur fail : 'a t code le calcul qui ne renvoie aucune valeur, il doit donc seulement appeler la continuation d'échec. Le combinateur return : 'a -> 'a t code le calcul qui renvoie une seule valeur, donnée en argument. Le combinateur orelse : 'a t -> 'a t -> 'a t prend deux calculs et renvoie toutes les valeurs renvoyées par ces calculs, tandis que andthen : 'a t -> ('a -> 'b t) -> 'b t prend deux calculs m et n et renvoie toutes les valeurs w renvoyées par n v pour un v renvoyé par m.

Tester:

let print_list l =
  Printf.printf "[%s]\n" (String.concat "," (List.map string_of_int l))

let () =
  let fk () = () in
  let sk l k = print_list l ; k () in
    f 5 5 sk fk