definition recursive de valeur

[Michel.Levy@imag.fr (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