[Camllist] Polymorphic variants
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20020424 (06:55) 
From:  John Max Skaller <skaller@o...> 
Subject:  [Camllist] How to compare recursive types? 
How to compare recursive types? [Or more generally, datya structures ..] Here is my best solution so far. For sake of argment types are either a) primitive b) binary product c) typedef (alias) name Suppose there is an environment typedef t1 = ... typedef t2 = ... typedef t3 .... and two type expression e1 and e2 We compare the type expressions structurally and recursively, also passing a counter value: cmp 99 e1 e2 When we reach a typedef name, we decrement the counter argument. If the counter drops to zero, we return true, otherwise we replace the name by the expression it denotes and continue (using the decremented counter). It is "obvious" that for a suitably large counter, this algorithm always terminates and gives the correct result. [The proof would follow from some kind of structural induction] Q1: is there a better algorithm? What does Ocaml use? Q2: how to estimate the initial value of the counter? I guess that, for example, 2(n +1) is enough for the counter, where n is the number of typedefs in the environment. My argument is in two parts: A. if we don't get a recursion after substituting each typedef (while chasing down a branch of the tree), we can't get it at all. B. The fixpoint of a branch of the second expression must be somewhere between the recursion target of the first fixpoint of the equivalent branch of the first expression and the second one. In other words, it is always enough to expand the fixpoint twice in one expression (along a single branch), any more expansions are sure to follow exactly the same behaviour as has already been performed. Q3: the same issue must arise in implementing the ocaml structural comparison function. Is there a way to build the data structures (factor out the typedefs) so i can use it directly on the terms? Q4: Is there a way to minimise the representation?  John Max Skaller, mailto:skaller@ozemail.com.au snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia. voice:61296600850  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners