From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.6.10/8.6.6) id NAA06258 for caml-redistribution; Fri, 23 Feb 1996 13:30:41 +0100 Received: (from weis@localhost) by pauillac.inria.fr (8.6.10/8.6.6) id NAA06135; Fri, 23 Feb 1996 13:19:58 +0100 From: Pierre Weis Message-Id: <199602231219.NAA06135@pauillac.inria.fr> Subject: Re: definition recursive de valeur To: Michel.Levy@imag.fr (Michel Levy) Date: Fri, 23 Feb 1996 13:19:58 +0100 (MET) Cc: caml-list@pauillac.inria.fr In-Reply-To: from "Michel Levy" at Feb 22, 96 03:16:50 pm MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Sender: weis [Franc,ais plus bas] > Let us define the following infinite values : > let rec x = 1::x ;; > let rec y = 1::y;; > x = y;; > The evaluation of the last expression doesn't terminate. > We could consider that the equations above have solutions wich are infinite > rational trees and there exists a algorithm to test the equality of such > trees, could it be possible either to use such an algorithm, either to > refuse to test the equality. As you may know, Caml offers two polymorphic predicates to compare values, that is == (physical identity) and = (re'cursive descent into values to find differences). None of these is the mathematical equality, except for some basic data types such that integers. In the library of the Caml V3.1 system, we have a third ``equal'' predicate that ``Compare graphs''. Unfortunately this ``equal'' predicate is hard to implement efficiently, is highly not portable, and moreover was found not very useful in practice: when people need such a sophisticated predicate, they need a complex semantic equality, upto some equivalence relationship, this predicate by no means correspond to ``equal'', so that they must write the predicate by themselves. Pierre Weis [Franc,ais] > Définissons les deux valeurs infinies suivantes : > let rec x = 1::x;; > let rec y = 1::y;; > x = y;; > Demandons à vérifier leur égalités : camllight essaie de comparer x et y > par une méthode qui ne se termine pas. > Pour les arbres infinis rationnels (cf Prolog) l'égalité est décidable : ne > serait-il pas possible soit de refuser de comparer x et y, soit d'utiliser > l'algorithme testant l'égalité de ce type d'arbre. Comme vous le savez certainement, Caml vous offre 2 pre'dicat polymorphes pour comparer les valeurs, == l'identite' physique et = (descente re'cursive dans les valeurs pour trouver des diffe'rences). Aucun des deux n'est l'egalite' mathe'matique, sauf pour quelques types de donne'es de base comme les entiers. Dans la bibliothe`que de Caml V3.1, il y a un troisie`me pre'dicat ``equal'' qui ``compare les graphes''. Malheureusement ce pre'dicat ``equal'' est difficile a` imple'menter efficacement, est hautement non portable, et comble de tout pas tre`s utile en pratique: quand on a besoin d'un pre'dicat aussi sophistique', l'expe'rience prouve qu'on a besoin en fait d'une e'galite' se'mantique complexe (modulo e'quivalence) qui ne correspond pas non plus a` ``equal'', et on est force' de l'e'crire soi-me^me. Pierre Weis INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis