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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe