[Caml-list] equi-recursive Fold isomorphism

[Caml-list] equi-recursive Fold isomorphism

[John Max Skaller]

Given a recursive type

    Fix 'a .  T  (where 'a occurs in T)

we can unfold the type to T' = T['a -> Fix 'a.T],
we define unfold t = t, if t doesn't start with a fixpoint operator.

Any ideas how to best implement fold, the inverse isomorphism?

Brute force method: examine every subterm, and compare with
the main term using equi-recusive comparison .. this seems quadratic
in the number of nodes .. smarter method: only compare arguments
of fixpoint binders .. can we do any better? For example,
replace the subterm in the main term with a fixpoint variable, and compare
the subterm with the modified main term (directly, ie. using ocaml 
'compare')
[I don't know how to do this 'replacement' efficiently though]

-- 
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

Re: [Caml-list] equi-recursive Fold isomorphism

[Alain Frisch]

Hello,

On Sun, 28 Jul 2002, John Max Skaller wrote:

> Given a recursive type
>
>     Fix 'a .  T  (where 'a occurs in T)
>
> we can unfold the type to T' = T['a -> Fix 'a.T],
> we define unfold t = t, if t doesn't start with a fixpoint operator.
>
> Any ideas how to best implement fold, the inverse isomorphism?
>
> Brute force method: examine every subterm, and compare with
> the main term using equi-recusive comparison .. this seems quadratic
> in the number of nodes .. smarter method: only compare arguments
> of fixpoint binders .. can we do any better?

You can keep in each node of the term a hash value for the
corresponding subterm; this hash value should be invariant by
folding/unfolding (you can for instance look at a fixed depth to
compute this hash value and unfold when necessary). These hash values
avoid most equi-recursive comparisons (and elegate most of the
remaining ones).

My Recursive module uses the same technique; it may do what you want:
http://www.eleves.ens.fr:8080/home/frisch/soft#recursive

It helps manipulating recursive structures (and recursive types was
indeed the main motivation) with maximal sharing and unique representation
(that is: two terms that have the same infinite unfolding will
be represented by the same value). You can also have a look at
the following papers, which describe another solution:

[1] Improving the Representation of Infinite Trees to Deal with Sets of Trees,
    Laurent Mauborgne;
    http://www.di.ens.fr/~mauborgn/publi/esop00.ps.gz

[2] Efficient Hash-Consing of Recursive Types, Jeffrey Considine;
    http://www.cs.bu.edu/techreports/2000-006-hashconsing-recursive-types.ps.Z



Hope this helps.

Alain

-------------------
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

Re: [Caml-list] equi-recursive Fold isomorphism

[John Max Skaller]

Alain Frisch wrote:

>My Recursive module uses the same technique; it may do what you want:
>http://www.eleves.ens.fr:8080/home/frisch/soft#recursive
>
Thanks!  

Hmmm: Ocaml 3.04+15 with -rectypes


# let rec x = (1,(1,(1,x)));;
val x : int * (int * (int * 'a)) as 'a =
 ....

Seem like Ocaml doesn't minimise the type, but:


let rec y = (1,y);;

x = y;;

Works correctly (so it knows the two types are comparable).
Interestingly, the answer is false: both data structures 
consist of an infinite stream of 1's, represented by
cycles of distinct lengths. No item by item comparison
could reveal any distinction: the infinite tree expansions
of the data structures are the same. Is Ocaml's answer correct?


-- 
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

Re: [Caml-list] equi-recursive Fold isomorphism

[Alain Frisch]

On Sun, 28 Jul 2002, John Max Skaller wrote:

> Hmmm: Ocaml 3.04+15 with -rectypes
>
>
> # let rec x = (1,(1,(1,x)));;
> val x : int * (int * (int * 'a)) as 'a =
>  ....
>
> Seem like Ocaml doesn't minimise the type, but:
>
>
> let rec y = (1,y);;
>
> x = y;;
>
> Works correctly (so it knows the two types are comparable).
> Interestingly, the answer is false

Are you sure ?  It seems that the comparison doesn't terminate,
as expected (as it does not consume memory). The manual
says:
<<
Equality between cyclic data structures may not terminate.
>>


: both data structures
> consist of an infinite stream of 1's, represented by
> cycles of distinct lengths. No item by item comparison
> could reveal any distinction: the infinite tree expansions
> of the data structures are the same. Is Ocaml's answer correct?

As you know, to implement the comparison between cyclic values with the
expected behaviour, one has to use a coinductive algorithm with some kind
of memoization. This would be much slower for the non-cyclic case, and
many people expect a fast generic compare function. I would like to say
that you can always take the code in byterun/compare.c and implement your
own equirecursive generic comparison in C, but this is actually not
possible (you need the Is_young and Is_in_heap macros that are not
available). Using the mentioned Recurse module, you could do:

module I = struct
  type 'a t = Int of int | Pair of 'a * 'a

  let map f = function
    | Int i -> Int i
    | Pair (a,b) -> Pair (f a, f b)

  let equal f x y =
    match (x,y) with
      | (Int i, Int j) when i = j -> ()
      | (Pair (a1,b1), Pair (a2,b2)) -> f a1 a2; f b1 b2
      | _ -> raise Recursive.NotEqual

  let iter f x = ignore (map f x)
  let hash f x = Hashtbl.hash (map f x)
  let deep = 4
end

module X = Recursive.Make(I)


let cons x = let n = X.make () in X.define n x; n
let recurs f = let n = X.make () in X.define n (f n); n
let int' i = I.Int i
let int i = cons (int' i)
let pair' a b = I.Pair (a,b)
let pair a b = cons (pair' a b)

let x = recurs (fun x -> pair' (int 1) (pair (int 1) (pair (int 1) x)))
let y = recurs (fun y -> pair' (int 1) y)

let x = X.internalize x and y = X.internalize y
let () = Printf.printf "%i;%i;%b\n" (X.id x) (X.id y) (x = y)


(the equility test is specified by Recurse to run in constant time)


Side-note: be careful if you implement a language with subtyping and both
recursive types and recursive (cyclic) values. Indeed, the usual
equi-recursive definition of subtyping is not sound if you allow cyclic
values. For instance, the algorithm would say that the type ('a * 'a) as
'a is empty, even though it is inhabited by values.


-- Alain

-------------------
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

[Caml-list] Question about distribution

[John Max Skaller]

Excuse dumb question: I have CVS version of Ocaml.
Is there a reason to also install 3.05 distribution?
(Does it contain something I can't build from  CVS, for example 
documentation,
camlp4, etc..?)

-- 
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

Re: [Caml-list] Question about distribution

[Xavier Leroy]

> Excuse dumb question: I have CVS version of Ocaml.
> Is there a reason to also install 3.05 distribution?
> (Does it contain something I can't build from  CVS, for example 
> documentation,
> camlp4, etc..?)

The source distribution (ocaml-3.05.tar.gz) is identical to the ocaml/
CVS subdirectory of camlcvs.inria.fr.  (Well, the CVS archive contains
some additional test files, but these are not part of the normal build
process.)

The user manual is not available via CVS, but you can get it from the
Caml Web site.

In summary: synchronizing your CVS copy (with cvs update -r ocaml305)
and building it is exactly equivalent to downloading and building
ocaml-3.05.tar.gz.

- Xavier Leroy

-------------------
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

Re: [Caml-list] Question about distribution

[Daniel de Rauglaudre]

Hi,

On Fri, Aug 02, 2002 at 12:49:32AM +1000, John Max Skaller wrote:

> Excuse dumb question: I have CVS version of Ocaml.
> Is there a reason to also install 3.05 distribution?
> (Does it contain something I can't build from  CVS, for example 
> documentation, camlp4, etc..?)

No. The release of OCaml is just a "snapshot" of the CVS version at a
given time.

-- 
Daniel de RAUGLAUDRE
daniel.de_rauglaudre@inria.fr
http://cristal.inria.fr/~ddr/
-------------------
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