From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id IAA10109; Wed, 24 Apr 2002 08:55:36 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id IAA10102 for ; Wed, 24 Apr 2002 08:55:35 +0200 (MET DST) Received: from sunny.pacific.net.au (sunny.pacific.net.au [203.25.148.40]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g3O6tXH26748 for ; Wed, 24 Apr 2002 08:55:34 +0200 (MET DST) Received: from wisma.pacific.net.au (wisma.pacific.net.au [210.23.129.72]) by sunny.pacific.net.au with ESMTP id g3O6tVXt021085 for ; Wed, 24 Apr 2002 16:55:32 +1000 (EST) Received: from ozemail.com.au (ppp106.dyn71.pacific.net.au [202.7.71.106]) by wisma.pacific.net.au with ESMTP id QAA21850 for ; Wed, 24 Apr 2002 16:55:30 +1000 (EST) Message-ID: <3CC656E1.5020108@ozemail.com.au> Date: Wed, 24 Apr 2002 16:55:29 +1000 From: John Max Skaller User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:0.9.2.1) Gecko/20010901 X-Accept-Language: en-us MIME-Version: 1.0 To: caml-list@inria.fr Subject: [Caml-list] How to compare recursive types? References: <3CBD4523.6080707@ozemail.com.au> <87y9fmr4fo.dlv@wanadoo.fr> Content-Type: text/plain; charset=ISO-8859-15; format=flowed Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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:61-2-9660-0850 ------------------- 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