--- Paul Hudak <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> "Interaction is the mind-body problem of computing." --Philip Wadler _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
