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