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 UAA28477; Wed, 24 Apr 2002 20:30:12 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id UAA28474 for caml-list@pauillac.inria.fr; Wed, 24 Apr 2002 20:30:11 +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 PAA20049 for ; Wed, 24 Apr 2002 15:14:18 +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 g3ODEGH16049 for ; Wed, 24 Apr 2002 15:14:16 +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 g3ODEEXt003100; Wed, 24 Apr 2002 23:14:15 +1000 (EST) Received: from ozemail.com.au (ppp171.dyn20.pacific.net.au [61.8.20.171]) by wisma.pacific.net.au with ESMTP id XAA13316; Wed, 24 Apr 2002 23:14:07 +1000 (EST) Message-ID: <3CC6AF9F.5040801@ozemail.com.au> Date: Wed, 24 Apr 2002 23:14:07 +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: Andreas Rossberg 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> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Andreas Rossberg wrote: >This is highly off-topic, but anyway... > Aw, come on. I'm writing a compiler using Ocaml. Who else would I ask about a typing problem than people who regularly use ocaml to implement compilers? I don't read news, I subscribe to exactly one mailing list (this one) and I'm neither an academic or a student. > >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). > Not yet no... they're next :-) > In that case >any type term can be interpreted as a rational tree. > .. what's that? > >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 .. >>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... > No of course not. Obviously, you return false if you reach two different primitives, or a product and a primitive. > >Seriously, what do you mean by "reaching a typedef name"? In one >argument? > Yes. In one of the arguments. >In both simultanously? What if you reach different names? > No, and irrelevant given that. >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). > I don't understand: probably because my description of the algorithm was incomplete, you didn't follow my intent. Real code below. >>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.] > No, that case is handled easily. Output of code below: ----------------------------------------------------- (((fix 1 * float) as 2 * int) as 1 * float) ((fix 1 * int) as 2 * float) as 1 equal (fix 1 * int) as 1 (fix 1 * int) as 1 equal ----------------------------------------------------- type node_t = | Prim of string | Pair of node_t * node_t | Name of string type env_t = (string * node_t) list type lnode_t = | LPrim of string | LPair of lnode_t * lnode_t | LBind of int * lnode_t | LFix of int let rec bind' env n labels t = match t with | Prim s -> LPrim s | Pair (t1, t2) -> LPair ( bind' env n labels t1, bind' env n labels t2 ) | Name s -> if List.mem_assoc s labels then LFix (List.assoc s labels) else LBind ( n, bind' env (n+1) ((s,n)::labels) (List.assoc s env) ) let bind env t = bind' env 1 [] t let rec str t = match t with | LPrim s -> s | LPair (t1,t2) -> "(" ^ str t1 ^ " * " ^ str t2 ^ ")" | LBind (i,t) -> str t ^ " as " ^ string_of_int i | LFix i -> "fix " ^ string_of_int i let rec cmp n lenv renv x y = if n = 0 then true else match x, y with | LPrim s, LPrim r -> s = r | LPair (a1,a2), LPair (b1,b2) -> cmp n lenv renv a1 b1 && cmp n lenv renv a2 b2 | LBind (i,a),_ -> cmp n ((i,a)::lenv) renv a y | _, LBind (i,b) -> cmp n lenv ((i,b)::renv) x b | LFix i,_ -> cmp (n-1) lenv renv (List.assoc i lenv) y | _,LFix i -> cmp (n-1) lenv renv x (List.assoc i renv) | _ -> false let env = [ "x", Pair (Name "y", Prim "int"); (* typedef x = y * int *) "y", Pair (Name "x", Prim "float") (* typedef y = x * float *) ] (* t1 = x * float, this equals y *) let t1 = Pair (Name "x", Prim "float") let t1' = bind env t1 let t2' = bind env (Name "y") ;; print_endline (str t1');; print_endline (str t2');; print_endline ( match cmp 10 [] [] t1' t2' with | true -> "equal" | false -> "not equal" ) ;; let env = [ "x", Pair (Name "x", Prim "int"); "y", Pair (Name "y", Prim "int") ] ;; let t1 = bind env (Name "x") let t2 = bind env (Name "y") ;; print_endline (str t1);; print_endline (str t2);; print_endline ( match cmp 10 [] [] t1 t2 with | true -> "equal" | false -> "not equal" ) ;; -- 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