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 RAA23866; Wed, 24 Apr 2002 17:03:23 +0200 (MET DST) 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 RAA23770 for ; Wed, 24 Apr 2002 17:03:23 +0200 (MET DST) Received: from indyio.rz.uni-sb.de (indyio.rz.uni-sb.de [134.96.7.3]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g3OF3M122129 for ; Wed, 24 Apr 2002 17:03:22 +0200 (MET DST) Received: from mars.rz.uni-sb.de (IDENT:kXZpWZFxoT5DdBevBvD2acJO2Q7/G5AP@mars.rz.uni-sb.de [134.96.7.4]) by indyio.rz.uni-sb.de (8.9.3/8.9.3) with ESMTP id RAA3834182 for ; Wed, 24 Apr 2002 17:03:21 +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 RAA99779397 for ; Wed, 24 Apr 2002 17:03:21 +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 g3OF3Kd07841; Wed, 24 Apr 2002 17:03:20 +0200 (CEST) Received: from mail.cs.uni-sb.de (IDENT:RnPdJb3+D+L1XXJfE31ZHr5Aje12x4sk@mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.12.1/2002030600) with ESMTP id g3OF3KW29197; Wed, 24 Apr 2002 17:03:20 +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 g3OF3I619464; Wed, 24 Apr 2002 17:03:18 +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 g3OF3Jh07095; Wed, 24 Apr 2002 17:03:19 +0200 Message-ID: <3CC6C986.A32F40F7@ps.uni-sb.de> Date: Wed, 24 Apr 2002 17:04:38 +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 CC: 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> <3CC675D7.40ADAD0F@ps.uni-sb.de> <3CC6AF9F.5040801@ozemail.com.au> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk John Max Skaller wrote: > > > In that case > >any type term can be interpreted as a rational tree. > > > .. what's that? An infinite tree that has only a finite number of different subtrees. Such trees can naturally be represented as cyclic graphs. > >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. > > > In the first instance, the client will have to apply type functions > to create types .. I don't understand what you mean. If you have type functions you have type lambdas, even if they are implicit in the source syntax. And decidability of structural recursion between type functions is an open problem, at least for arbitrary functions, so be careful. (Thanks to Haruo for reminding me of Salomon's paper, I already forgot about that.) OCaml avoids the problem by requiring uniform recursion for structural types, so that all lambdas can be lifted out of the recursion. > >[...] > > I don't understand: probably because my description of the algorithm > was incomplete, you didn't follow my intent. Real code below. OK, now it is getting clearer. Your idea is to unroll the types k times for some k. Of course, this is trivially correct for infinite k. The correctness of your algorithm depends on the existence of a finite k. > I guess that, for example, 2(n +1) is enough for the counter, > where n is the number of typedefs in the environment. I don't think so. Consider: t1 = a*(a*(a*(a*(a*(a*(a*(a*b))))))) t2 = a*t2 This suggests that k must be at least 2m(n+1), where m is the size of the largest type in the environment. Modulo this correction, you might be correct. Still, ordinary graph traversal seems the more appropriate approach to me: represent types as cyclic graphs and check whether the reachable subgraphs are equivalent. There is also a recent paper about how to apply hash-consing techniques to cyclic structures: @article{Mauborgne:IncrementalUniqueRepresentation, author = "Laurent Mauborgne", title = "An Incremental Unique Representation for Regular Trees", editor = "Gert Smolka", journal = "Nordic Journal of Computing", volume = 7, pages = "290--311", year = 2000, month = nov, } -- 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