[Haskell-beginners] Rewriting traversal over trees

[Brent Yorgey]

Hi Darryn,

This code looks very nice to me.  There probably are different ways to
do it, existing things it is related to, and so on, but if you want
that sort of commentary you will probably get a better response on the
haskell-cafe at haskell.org mailing list (where such a message would be
quite welcome).

-Brent

On Fri, Mar 26, 2010 at 04:53:27PM +1030, Darryn Reid wrote:
> 
> Hi, I hope that this is an appropriate place to post this question; I'm
> an experienced computer scientist and mathematician but am new to
> Haskell (I love it, I might add, but have much to learn).
> 
> 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.
> 2. I cannot really see how to easily extend this to a queue-based
> breadth-first traversal. 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.
> 
> Thanks in advance for any help!
> 
> Darryn.
> 
> start of code.
> -------------------------------------------------------------------------
> import Control.Monad
> import Control.Monad.Identity
> 
> -- Tableau is a tree containing formulas of type a, in 
> -- Fork (disjunctive) nodes and Single (conjunctive) nodes.
> -- Paths from root to Nil each represent an interpretation.
> data Tableau a =   Nil                           -- End of a path
>                  | Single a (Tableau a)          -- Conjunction
>                  | Fork (Tableau a) (Tableau a)  -- Disjunction
>                  deriving (Eq, Show)
> 
> -- 'Cut' directs the traversal to move back up the tree rather than into
> -- the current subtree, while 'Next' directs the traversal to proceed
> -- into the subtree.
> data Action = Cut | Next 
>               deriving (Eq, Show)
> 
> -- The type of the rewrite function to perform at each node in
> -- the traversal of the tree. The Rewriter returns the new
> -- subtree to replace the existing subtree rooted at the
> -- traversal node, and a direction controlling the traversal
> -- to the next node.
> type Rewriter m a = Tableau a -> m (Tableau a, Action)
> 
> -- The traversal function, depth-first order.
> rewrite :: (Monad m) => Rewriter m a -> Tableau a -> m (Tableau a)
> rewrite rf t = do (t', d) <- rf t
>                   rewrite' rf d t'
> 
> -- Worker function for traversal, really its main body.
> rewrite' :: (Monad m) => Rewriter m a -> Action -> Tableau a -> m
> (Tableau a)
> rewrite' rf Cut  t             = return t
> rewrite' rf Next Nil           = return Nil
> rewrite' rf Next (Single x t1) = do t1' <- rewrite rf t1
>                                     return (Single x t1')
> rewrite' rf Next (Fork t1 t2)  = do t1' <- rewrite rf t1
>                                     t2' <- rewrite rf t2
>                                     return (Fork t1' t2')
> 
> -- Some examples to test the code with:
> -- ghci> let t0 = (Single 2 (Single 3 Nil))
> -- ghci> let t1 = (Single 1 (Fork t0 (Fork (Single 4 Nil) (Single 5
> Nil))))
> -- ghci> let t2 = (Fork (Single 10 Nil) (Single 11 Nil))
> -- ghci> let t3 = (Fork (Single 3 Nil) (Single 3 Nil))
> 
> -- Running "test4 t1 t2" produces the expected result; running 
> -- "test4 t1 t3" does not terminate, because this endlessly 
> -- generates new patterns that match the substitution condition:
> test4 :: (Num t) => Tableau t -> Tableau t -> Tableau t
> test4 tab tab' = runIdentity (rewrite rf tab)
>             where rf (Single 3 Nil) = return (tab', Next)
>                   rf t              = return (t, Next)
> 
> -- Running "test5 t1 t3", however, does terminate because the "Cut"
> -- prevents the traversal from entering the newly spliced subtrees
> -- that match the pattern.
> test5 :: (Num t) => Tableau t -> Tableau t -> Tableau t
> test5 tab tab' = runIdentity (rewrite rf tab)
>             where rf (Single 3 Nil) = return (tab', Cut)
>                   rf t              = return (t, Next)
> -------------------------------------------------------------------------
> end of code.
> 
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners