[Haskell-cafe] Detecting Cycles in Datastructures

[Greg Woodhouse]

--- 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
> of
>  > "Eq" such that cyclic == cyclic is smart enough to avoid a
> recursive
>  > 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
> I
> 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
computed.
> 
>  > e1,e2 :: Expr
>  > e1 = fix fe1          -- finite
>  > e2 = fix fe2          -- infinite
> 
> Note that e2 is equivalent to your "cyclic".  But now we can also
> test
> 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
> not
> "syntactically", or structurally, equivalent.  Thus this definition
> of
> 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,
> 
>    -Paul
> 



===
Gregory Woodhouse  <gregory.woodhouse at sbcglobal.net>


"Interaction is the mind-body problem of computing."

--Philip Wadler