Version française
Home     About     Download     Resources     Contact us    
Browse thread
definition recursive de valeur
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Michel.Levy@i...
Subject: definition recursive de valeur


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