[Haskell-cafe] Re: Seeking advice about monadic traversal
functions
Darryn Reid
djreid at aapt.net.au
Wed Mar 31 18:17:42 EDT 2010
Heinrich,
Thanks for your excellent response! Indeed, it was the rebuilding of the
tree that had me stumped. I also see the benefits of using the lift
functions, thanks again for this insight.
Darryn.
On Wed, 2010-03-31 at 12:44 +0200, Heinrich Apfelmus wrote:
> Darryn Reid wrote:
> >
> > I've coded a (fairly) general rewriting traversal - I suspect the
> > approach might be generalisable to all tree-like types, but this doesn't
> > concern me much right now. My purpose is for building theorem provers
> > for a number of logics, separating the overall control mechanism from
> > the specific rules for each logic.
> >
> > The beauty of Haskell here is in being able to abstract the traversal
> > away from the specific reduction rules and languages of the different
> > logics. I have paired down the code here to numbers rather than modal
> > formulas for the sake of clarity and simplicity. My question is
> > two-fold:
> > 1. Does my representation of the traversal seem good or would it be
> > better expressed differently? If so, I'd appreciate the thoughts of more
> > experienced Haskell users.
>
> Looks fine to me, though I have no experience with tree
> rewriting. :) I'd probably write it like this:
>
> > data Tableau a = Nil -- End of a path
> > | Single a (Tableau a) -- Conjunction
> > | Fork (Tableau a) (Tableau a) -- Disjunction
> > deriving (Eq, Show)
> > data Action = Cut | Next
> > type Rewriter m a = Tableau a -> m (Tableau a, Action)
>
> rewrite :: (Monad m) => Rewriter m a -> Tableau a -> m (Tableau a)
> rewrite f t = f t >>= (uncurry . flip) go
> where
> go Cut t = return t
> go Next Nil = return Nil
> go Next (Single x t1) = liftM (Single x) (rewrite f t1)
> go Next (Fork t1 t2 ) = liftM2 Fork (rewrite f t1)
> (rewrite f t2)
>
> In particular, liftM and liftM2 make it apparent that we're just
> wrapping the result in a constructor.
>
>
> In case you want more flexibility in moving from children to parents,
> you may want to have a look at zippers
>
> http://en.wikibooks.org/wiki/Haskell/Zippers
>
> > 2. I cannot really see how to easily extend this to a queue-based
> > breadth-first traversal, which would give me fairness. I'm sure others
> > must have a good idea of how to do what I'm doing here except in
> > breadth-first order; I'd appreciate it very much if someone could show
> > me how to make a second breadth-first version.
>
> This is more tricky than I thought! Just listing the nodes in
> breadth-first order is straightforward, but the problem is that you
> also want to build the result tree. Depth-first search follows the tree
> structure more closely, so building the result was no problem.
>
> The solution is to solve the easy problem of listing all nodes
> in breadth-first order first, because it turns out that it's possible to
> reconstruct the result tree from such a list! In other words, it's
> possible to run breadth-first search in reverse, building the tree from
> a list of nodes.
>
> How exactly does this work? If you think about it, the analogous problem
> for depth-first search is not too difficult, you just walk through the
> list of nodes and build a stack; pushing Nil nodes and combining the
> top two items when encountering Fork nodes. So, for solving the
> breadth-first version, the idea is to build a queue instead of a stack.
>
> The details of that are a bit tricky of course, you have to be careful
> when to push what on the queue. But why bother being careful if we have
> Haskell? I thus present the haphazardly named:
>
>
> Lambda Fu, form 132 - linear serpent inverse
>
> The idea is to formulate breadth-first search in a way that is *trivial*
> to invert, and the key ingredient to that is a *linear* function, i.e.
> one that never discards or duplicates data, but only shuffles it around.
> Here is what I have in mind:
>
> {-# LANGUAGE ViewPatterns #-}
> import Data.Sequence as Seq -- this will be our queue type
> import Data.List as List
>
> type Node a = Tableau a -- just a node without children (ugly type)
> type State a = ([Action],[(Action,Node a)], Seq (Tableau a))
> queue (_,_,q) = q
> nodes (_,l,_) = l
>
> analyze :: State a -> State a
> analyze (Cut :xs, ts, viewl -> t :< q) =
> (xs, (Cut , t ) : ts, q )
> analyze (Next:xs, ts, viewl -> Nil :< q) =
> (xs, (Next, Nil ) : ts, q )
> analyze (Next:xs, ts, viewl -> Single x t1 :< q) =
> (xs, (Next, Single x u) : ts, q |> t1 )
> analyze (Next:xs, ts, viewl -> Fork t1 t2 :< q) =
> (xs, (Next, Fork u u ) : ts, (q |> t1) |> t2 )
> u = Nil -- or undefined
>
> bfs xs t = nodes $
> until (Seq.null . queue) analyze (xs,[],singleton t)
>
> So, bfs just applies analyze repeatedly on a suitable state which
> includes the queue, the list of nodes in breadth-first order and a
> stream of actions. (This is a simplified example, you will calculate the
> actions on the fly of course.) To be able to pattern match on the queue,
> I have used GHC's ViewPattern extension.
>
> It should be clear that analyze performs exactly one step of a
> breadth-first traversal.
>
> Now, the key point is that analyze is *linear*, it never discards or
> duplicates any of the input variables, it just shuffles them around,
> like moving a constructor from the tree to the node list or from one
> list to the other. This makes it straightforward to implement an inverse
> function synthesize which fulfills
>
> synthesize . analyze = id
>
> After all, we only have to write the definition of analyze from right
> to left!
>
> synthesize :: State a -> State a
> synthesize (xs, (Cut , t ) : ts, q) =
> (Cut:xs , ts, t <| q)
> synthesize (xs, (Next, Nil ) : ts, q) =
> (Next:xs, ts, Nil <| q)
> synthesize (xs, (Next, Single x _) : ts, viewr -> q :> t1) =
> (Next:xs, ts, Single x t1 <| q)
> synthesize (xs, (Next, Fork _ _ ) : ts, viewr ->
> (viewr -> q :> t1) :> t2) =
> (Next:xs, ts, Fork t1 t2 <| q)
>
> Looks a bit noisy, but I have simply copy & pasted the four equations
> for analyze and interchanged the left-hand and the right-hand sides,
> adjusting the view patterns.
>
> Thus, we can invert bfs by repeatedly applying synthesize to the
> final state of bfs :
>
> unBfs ts = (`index` 0) . queue $
> until (List.null . nodes) synthesize ([],ts,empty)
>
> By construction, we have obtained the desired
>
> unBfs . bfs xs = id
>
>
>
> Regards,
> Heinrich Apfelmus
>
> PS:
> * I have used a double-ended queue, but we're never really using both
> ends at once. An ordinary FIFO queue will suffice if we interpret it to
> "change direction" between bfs and unBfs .
> * Exchanging the queue for a stack will give depth-first search and its
> inverse.
>
>
> --
> http://apfelmus.nfshost.com
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list