English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
[Caml-list] Polymorphic variants
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2002-04-24 (06:55)
From: John Max Skaller <skaller@o...>
Subject: [Caml-list] 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.

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