[Haskell-cafe] Re: Seeking advice about monadic traversal functions

[Darryn Reid]

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