Re: [Caml-list] How to compare recursive types?

[Andreas Rossberg <rossberg@ps.uni-sb.de>]

This is highly off-topic, but anyway...

John Max Skaller wrote:
> 
> 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

OK, so you don't have type lambdas (parameterised types). In that case
any type term can be interpreted as a rational tree. There are standard
algorithms for comparing such trees, they are essentially simple graph
algorithms. Something along these lines is used in the OCaml compiler.

If you add lambdas (under recursion) things get MUCH harder. Last time I
looked the problem of equivalence of such types under the equi-recursive
interpretation you seem to imply (i.e. recursion is `transparent') was
believed to be undecidable.

> 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).

So you return true for any infinite (i.e. recursive) type.
Interesting...

Seriously, what do you mean by "reaching a typedef name"? In one
argument? In both simultanously? What if you reach different names? From
the second paragraph it seems that you have only considered one special
case. For the others, if your counter dropped to 0, you had to return
false for the sake of termination, which renders the algorithm incorrect
(or incomplete, if you want to put it mildly).

> 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]

I doubt that ;-) In fact it is obvious that your algorithm is incorrect.
[The proof is a simple counter example like (cmp n t1 t2) where
t1=prim*t1, t2=prim*t2.]

Regards,

	- Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners