[Caml-list] Preuves avec le filtrage de motifs

[Diego Olivier Fernandez Pons <Diego-Olivier.FERNANDEZ-PONS@cicrp.jussieu.fr>]

    Bonjour,

Sven Luther a écrit dans "Re : [Caml-list] Guards vs. conditionals"

> It is just a matter of coding style. I think that the if version is
> maybe easier to do prooves on or something such, and that guard
> version is easier to read and maybe better when there are more than
> one condition, but the compiler does not know when the guards cover
> all the cases, and may output a warning when non is needed :
>
> consider :
>
> let foo = function
>   | i when i > 500 -> 1
>   | i when i = 500 -> 2
>   | i when i < 500 -> 3
>
> Which will output a warning.

A quoi Pierre Weis a répondu

> What do you mean ?

Il me semble que l'on peut faire un certain nombre de preuves
d'exhaustivité pour le filtrage de motifs, plus poussées que celles
que fait Caml pour l'instant, et que c'est plus simple que dans le cas
des cascades de conditionnelles [if ... then ... else]

La FAQ expert indique que l'on pourrait ajouter un cas spécial pour
les filtrages les plus simples (ici, une structure de données gérant
les intervalles suffit, par exemple un Diet tree), mais que c'est
impossible dans les cas le cas général.

Si les contraintes sont arithmétiques, et ce quel que soit le nombre
de variables sur lesquelles elles portent, le problème de
l'exhaustivité du filtrage se ramène à celui de la recherche d'une
valeur vérifiant toutes les contraintes

let f = function
  | n when c1 (n) -> ...
  | n when c2 (n) -> ...
  | n when c3 (n) -> ...

Il suffit de montrer qu'il n'existe pas de x tel que c1(x) && c2 (x)
&& c3 (x). Or ce problème pour les domaines finis (les entiers dans ce
cas précis) et les contraintes arithmétiques est un problème de
programmation par contraintes bien maitrisé : il suffit de faire un
branch and bound avec propagation de contraintes (tel que dans la
librairie Facile)

J'ai relevé un second cas dans lequel il me semblait aisé de faire
quelque chose

type number = One | Two | Three | Many

let f = function
  | One -> One
  | Two -> Two
  | Three -> Many
  | Many -> Many

let g = function x ->
  match f x with
   | One -> 1
   | Two -> 2
   | Many -> 10

La première idée qui vient à l'esprit est de faire un graphe où les
noeuds représentent des fonctions avec en entrée et sortie les membres
gauches et droits des filtrages respectifs.

Alors le compilateur pourrait vérifier l'exhaustivité de la
composition. Il s'agit en réalité du même cas que le précédent, mais
il faut adopter une modélisation plus riche des contraintes (le graphe
en question étant le graphe (hyper-graphe) des contraintes)

Le problème en somme semble se ramener à la définition précise du type
de fonctions que le solveur de contraintes peut traverser :

let f = fun x -> x > 3 (fonctions booleennes "purement arithmétiques")

let f = function x -> max 3 x (restriction du domaine)

pour les deux cas précédents (si l'on considère le type One | Two |
Tree isomorphe à l'intervalle [1, 2, 3])

Parcontre il est à peu près évident que l'on pourra difficilement
traverser une fonction comme

let f = function x -> let num = Random.int (1024) in x = num || x <> num

Car nous n'avons aucun moyen de traverser la fonction Random.int même
si cette contrainte est trivialement vérifiée.

L'exemple que propose la FAQ expert est à ce titre particulièrement
pervers :

let rec f = function
  | n when n >= 0 -> n
  | n when - f (-n) < 0 -> n + 1

la fonction doit se traverser elle même comme contrainte, alors
qu'elle n'est que partiellement définie.

Cela dit, il me semble possible d'étendre le domaine de recherche
d'exhaustivité du filtrage de motifs par la technique du solveur de
contraintes.

De surcroît notons que l'on peut obtenir des informations
supplémentaires (par exemple disjonction de contraintes) qui
permettent la commutation des cas par exemple.

let f = function
  | n when n < 0 -> ...
  | 0 -> ...
  | n when n > 0 -> ...

les cas étant 2 à 2 disjoints, tous les ordres conviennent, et donc le
compilateur est libre de choisir celui qui lui convient le mieux

Je crois bien avoir lu dans un article de Luc Maranguet et Fabrice Le
Fessant sur l'optimisation du filtrage de motifs dans Caml que Caml
s'efforceait déjà de tirer profit des informations d'exhaustivité et
de commutativité, mais j'ignore si cela s'applique pour le filtrage
avec gardes.

La deuxième partie de ma réponse concerne les cascades "if ... then
... else". Bon... c'est purement subjectif mais il me semble que ce
type de traitement des contraintes est plus simple si elles sont
toutes sur le même plan (filtrage) que si l'on a forcé
artificiellement un des test a avoir lieu d'abord comme ce serait le
cas dans

  if n = 0 then ...
  else if n > 0 then ...
  else ...

En effet, il faut ressortir les contraintes de l'intérieur de la
première condition (par exemple constater ici que n = 0 et n > 0 sont
disjoints donc on peut extraire n > 0 sans modifications), pour
ensuite refaire le même traitement que précédemment (choisir le
meilleur ordre d'évaluations).

Cela dit, ce n'est qu'une impression, je serais incapable de donner
des arguments plus probants.


        Diego Olivier

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners