Message-Id: <v01530503ad5226209225@[129.88.38.40]>
Date: Thu, 22 Feb 1996 15:16:50 +0100
To: caml-list@pauillac.inria.fr
From: Michel.Levy@imag.fr (Michel Levy)
Subject: definition recursive de valeur
D=E9finissons les deux valeurs infinies suivantes :
let rec x =3D 1::x;;
let rec y =3D 1::y;;
x =3D y;;
Demandons =E0 v=E9rifier leur =E9galit=E9s : camllight essaie de comparer x=
et y
par une m=E9thode qui ne se termine pas.
Pour les arbres infinis rationnels (cf Prolog) l'=E9galit=E9 est d=E9cidable=
: ne
serait-il pas possible soit de refuser de comparer x et y, soit d'utiliser
l'algorithme testant l'=E9galit=E9 de ce type d'arbre.
Let us define the following infinite values :
let rec x =3D 1::x ;;
let rec y =3D 1::y;;
x =3D 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