definition recursive de valeur

definition recursive de valeur

[Michel Levy]

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.

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.

Michel Levy
L.S.R.
BP53x - 38041 Grenoble cedex - France
Tel : 76827246
e.mail : Michel.Levy@imag.fr

Re: definition recursive de valeur

[Pierre 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

Re: definition recursive de valeur

[Kip Rugger]

>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

The ``equal'' predicate does suggest an implementation using mark bits
in the data structure, making it not portable.  The only portable
algorithm that I know is as follows (in pseudo C code):

    if ( {terminal case} ) ...
    if ( *p == *q ) return true;
    save( p, *p );
    t = *p, *p = *q;
    return compare( t, *q );

so given the initial conditions:

    p --> x = 1 :: y
    q --> y = 1 :: x

this is reduced after one iteration to:

    q --> x = 1 :: x
    p --> y = 1 :: x

from which equality follows.  Unfortunately, both data structures are
potentially destroyed in the process, making it necessary to save and
restore the modifications on a stack.

I agree that ``equal'' is of limited use, even if it could handle
cyclical structures.  It is usually better to build unique representations
of the underlying structures so that ``=='' can be used instead.

What is useful is a ``shallow equal'' which applies ``=='' to the top
level of a data structure.  This allows easy comparison of records,
tuples, or arrays of scalar objects, as well as supplying the terminal
condition for recursive data structures.

Kip Rugger