This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

[Caml-list] equi-recursive Fold isomorphism
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2002-07-27 (17:32) From: John Max Skaller Subject: [Caml-list] equi-recursive Fold isomorphism
```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

```