From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA09115; Mon, 6 Jan 2003 18:36:36 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA07952 for ; Mon, 6 Jan 2003 18:36:35 +0100 (MET) Received: from shiva.jussieu.fr (shiva.jussieu.fr [134.157.0.129]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h06HaY512099 for ; Mon, 6 Jan 2003 18:36:34 +0100 (MET) Received: from ibm3.cicrp.jussieu.fr (ibm3.cicrp.jussieu.fr [134.157.15.3]) by shiva.jussieu.fr (8.12.5/jtpda-5.4) with ESMTP id h06HaYb4012094 for ; Mon, 6 Jan 2003 18:36:34 +0100 (CET) Received: from ibm1.cicrp.jussieu.fr (ibm1.cicrp.jussieu.fr [134.157.15.1]) by ibm3.cicrp.jussieu.fr (8.8.8/jtpda/mob-V8) with ESMTP id SAA44518 for ; Mon, 6 Jan 2003 18:35:21 +0100 Received: from localhost (fernande@localhost) by ibm1.cicrp.jussieu.fr (8.8.8/jtpda/mob-v8) with ESMTP id SAA4423784 for ; Mon, 6 Jan 2003 18:35:21 +0100 Date: Mon, 6 Jan 2003 18:35:21 +0100 (NFT) From: Diego Olivier Fernandez Pons To: Caml-list@inria.fr Subject: [Caml-list] Preuves avec le filtrage de motifs Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=iso-8859-1 Content-Transfer-Encoding: QUOTED-PRINTABLE X-Antivirus: scanned by sophie at shiva.jussieu.fr Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Bonjour, Sven Luther a =E9crit 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 =3D function > | i when i > 500 -> 1 > | i when i =3D 500 -> 2 > | i when i < 500 -> 3 > > Which will output a warning. A quoi Pierre Weis a r=E9pondu > What do you mean ? Il me semble que l'on peut faire un certain nombre de preuves d'exhaustivit=E9 pour le filtrage de motifs, plus pouss=E9es 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=E9cial pour les filtrages les plus simples (ici, une structure de donn=E9es g=E9rant les intervalles suffit, par exemple un Diet tree), mais que c'est impossible dans les cas le cas g=E9n=E9ral. Si les contraintes sont arithm=E9tiques, et ce quel que soit le nombre de variables sur lesquelles elles portent, le probl=E8me de l'exhaustivit=E9 du filtrage se ram=E8ne =E0 celui de la recherche d'une valeur v=E9rifiant toutes les contraintes let f =3D 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=E8me pour les domaines finis (les entiers dans ce cas pr=E9cis) et les contraintes arithm=E9tiques est un probl=E8me de programmation par contraintes bien maitris=E9 : il suffit de faire un branch and bound avec propagation de contraintes (tel que dans la librairie Facile) J'ai relev=E9 un second cas dans lequel il me semblait ais=E9 de faire quelque chose type number =3D One | Two | Three | Many let f =3D function | One -> One | Two -> Two | Three -> Many | Many -> Many let g =3D function x -> match f x with | One -> 1 | Two -> 2 | Many -> 10 La premi=E8re id=E9e qui vient =E0 l'esprit est de faire un graphe o=F9 les noeuds repr=E9sentent des fonctions avec en entr=E9e et sortie les membres gauches et droits des filtrages respectifs. Alors le compilateur pourrait v=E9rifier l'exhaustivit=E9 de la composition. Il s'agit en r=E9alit=E9 du m=EAme cas que le pr=E9c=E9dent, m= ais il faut adopter une mod=E9lisation plus riche des contraintes (le graphe en question =E9tant le graphe (hyper-graphe) des contraintes) Le probl=E8me en somme semble se ramener =E0 la d=E9finition pr=E9cise du t= ype de fonctions que le solveur de contraintes peut traverser : let f =3D fun x -> x > 3 (fonctions booleennes "purement arithm=E9tiques") let f =3D function x -> max 3 x (restriction du domaine) pour les deux cas pr=E9c=E9dents (si l'on consid=E8re le type One | Two | Tree isomorphe =E0 l'intervalle [1, 2, 3]) Parcontre il est =E0 peu pr=E8s =E9vident que l'on pourra difficilement traverser une fonction comme let f =3D function x -> let num =3D Random.int (1024) in x =3D num || x <> = num Car nous n'avons aucun moyen de traverser la fonction Random.int m=EAme si cette contrainte est trivialement v=E9rifi=E9e. L'exemple que propose la FAQ expert est =E0 ce titre particuli=E8rement pervers : let rec f =3D function | n when n >=3D 0 -> n | n when - f (-n) < 0 -> n + 1 la fonction doit se traverser elle m=EAme comme contrainte, alors qu'elle n'est que partiellement d=E9finie. Cela dit, il me semble possible d'=E9tendre le domaine de recherche d'exhaustivit=E9 du filtrage de motifs par la technique du solveur de contraintes. De surcro=EEt notons que l'on peut obtenir des informations suppl=E9mentaires (par exemple disjonction de contraintes) qui permettent la commutation des cas par exemple. let f =3D function | n when n < 0 -> ... | 0 -> ... | n when n > 0 -> ... les cas =E9tant 2 =E0 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=E9j=E0 de tirer profit des informations d'exhaustivit=E9 et de commutativit=E9, mais j'ignore si cela s'applique pour le filtrage avec gardes. La deuxi=E8me partie de ma r=E9ponse concerne les cascades "if ... then =2E.. 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=EAme plan (filtrage) que si l'on a forc=E9 artificiellement un des test a avoir lieu d'abord comme ce serait le cas dans if n =3D 0 then ... else if n > 0 then ... else ... En effet, il faut ressortir les contraintes de l'int=E9rieur de la premi=E8re condition (par exemple constater ici que n =3D 0 et n > 0 sont disjoints donc on peut extraire n > 0 sans modifications), pour ensuite refaire le m=EAme traitement que pr=E9c=E9demment (choisir le meilleur ordre d'=E9valuations). 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