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

[Heinrich Apfelmus]

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