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