Re: definition recursive de valeur

[Pierre Weis <weis@pauillac.inria.fr>]

[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