[Haskell-cafe] Detecting Cycles in Datastructures
gregory.woodhouse at sbcglobal.net
Fri Nov 18 13:07:46 EST 2005
--- Paul Hudak <paul.hudak at yale.edu> wrote:
> This is a very late response to an old thread...
> Tom Hawkins wrote:
> > In a pure language, is it possible to detect cycles in recursive
> > data structures? For example, is it possible to determine that
> > "cyclic" has a loop? ...
> > data Expr = Constant Int | Addition Expr Expr
> > cyclic :: Expr
> > cyclic = Addition (Constant 1) cyclic
> > Or phased differently, is it possible to make "Expr" an instance
> > "Eq" such that cyclic == cyclic is smart enough to avoid a
> > decent?
I'm a little confused. It's one thing to demonstrate that a (possibly
infinite) digraph contains a loop, but quite another to show that it
does not. Carrying around a copy of the subgraph consisting of nodes
actually visited is workable in a pure language, but there's no
guarantee of termination.
> > -Tom
> Perhaps it's obvious, but one way to do this is to make the cycle
> *implicit* via some kind of a fixed-point operator, which is a trick
> used recently in a DSL application.
So, you imagine f to be a function that (non-deterministally) follows
an edge in a digraph. The idea being that G is (possibly infinite)
digraph and F is a subgraph. The "function" f would
non-deterministically select a vertext of F, follow an edge in G (again
chosen non-deterministically), add the (possibly new) edge to F, and
return the resulting graph. Then, you are asking if f has a fixpoint in
this broader context?
> For example, you could define:
> > data Expr = Const Int
> > | Add Expr Expr
> > | Loop -- not exported
> > deriving (Eq, Show)
> The purpose of Loop is to "mark" the point where a cycle exists.
> Instead of working with values of type Expr, you work with values of
> type Expr -> Expr, or Fix Expr:
> > type Fix a = a -> a
> For example:
> > fe1,fe2 :: Fix Expr
> > fe1 e = Add (Const 1) (Const 1) -- non-recursive
> > fe2 e = Add (Const 1) e -- recursive
> You can always get the value of an Expr from a Fix Expr whenever you
> need it, by computing the fixed point:
> > fix f = x where x = f x
If it can be computed. Maybe I'm off-track here, but it seems to me
that when you introduce laziness into the equation, you lose any
guarantee of there even being a fixpoint, much less one that can be
> > e1,e2 :: Expr
> > e1 = fix fe1 -- finite
> > e2 = fix fe2 -- infinite
> Note that e2 is equivalent to your "cyclic". But now we can also
> for equality:
> > instance Eq (Fix Expr) where
> > fe1 == fe2 = fe1 Loop == fe2 Loop
> For example, fe2 == fe2 returns "True", whereas e2 == e2
> (i.e. your cyclic == cyclic) diverges.
> Of course, note that, although fe1 == fe2 implies that fix fe1 == fix
> fe2, the reverse is not true, since there will always be loops of
> varying degrees of unwinding that are semantically equivalent, but
> "syntactically", or structurally, equivalent. Thus this definition
> equality is only approximate, but still, it's useful.
I'm lost. Are you saying bottom is bottom?
> If you want to have multiple loops, or a loop not at the top level,
> then you need to add some kind of a loop constructor to Expr. I've
> sketched that idea below, and pointed out a couple of other useful
> ideas, such as showing a loop, and mapping a function over a loop
> without unwinding it.
> I hope this helps,
Gregory Woodhouse <gregory.woodhouse at sbcglobal.net>
"Interaction is the mind-body problem of computing."
More information about the Haskell-Cafe