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 LAA12379; Wed, 24 Apr 2002 11:06:21 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA12411 for ; Wed, 24 Apr 2002 11:06:21 +0200 (MET DST) Received: from indyio.rz.uni-sb.de (indyio.rz.uni-sb.de [134.96.7.3]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g3O96KP07864 for ; Wed, 24 Apr 2002 11:06:20 +0200 (MET DST) Received: from mars.rz.uni-sb.de (IDENT:WBSTqG2DLbuM+8sXWCY+Trr+DN5S5kla@mars.rz.uni-sb.de [134.96.7.4]) by indyio.rz.uni-sb.de (8.9.3/8.9.3) with ESMTP id LAA3774242 for ; Wed, 24 Apr 2002 11:06:19 +0200 (CEST) Received: from uni-sb.de (uni-sb.de [134.96.7.230]) by mars.rz.uni-sb.de (8.8.8/8.8.4/8.8.2) with ESMTP id LAA97537839 for ; Wed, 24 Apr 2002 11:06:19 +0200 (CEST) Received: from cs.uni-sb.de (cs.uni-sb.de [134.96.252.31]) by uni-sb.de (8.12.2/2002030600) with ESMTP id g3O96Id29539; Wed, 24 Apr 2002 11:06:18 +0200 (CEST) Received: from mail.cs.uni-sb.de (IDENT:J1PnZcNNstvv50+nyw1PWACW8mCdGxPn@mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.12.1/2002030600) with ESMTP id g3O96HW16610; Wed, 24 Apr 2002 11:06:18 +0200 (CEST) Received: from ps.uni-sb.de (grizzly.ps.uni-sb.de [134.96.186.68]) by mail.cs.uni-sb.de (8.12.3/2002040900) with ESMTP id g3O96F604171; Wed, 24 Apr 2002 11:06:16 +0200 (CEST) X-Authentication-Warning: email: Host grizzly.ps.uni-sb.de [134.96.186.68] claimed to be ps.uni-sb.de Received: from ps.uni-sb.de (zoidberg.ps.uni-sb.de [134.96.186.121]) by ps.uni-sb.de (8.11.6/8.11.0) with ESMTP id g3O96Gh32748; Wed, 24 Apr 2002 11:06:16 +0200 Message-ID: <3CC675D7.40ADAD0F@ps.uni-sb.de> Date: Wed, 24 Apr 2002 11:07:35 +0200 From: Andreas Rossberg Organization: =?iso-8859-1?Q?Universit=E4t?= des Saarlandes X-Mailer: Mozilla 4.78 [en] (X11; U; Linux 2.4.9-21 i686) X-Accept-Language: de, en MIME-Version: 1.0 To: John Max Skaller , caml-list@inria.fr Subject: Re: [Caml-list] How to compare recursive types? References: <3CBD4523.6080707@ozemail.com.au> <87y9fmr4fo.dlv@wanadoo.fr> <3CC656E1.5020108@ozemail.com.au> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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