In the code above Tableau is the same type after rewriting. If that's
the case, maybe you don't need a state monad solution. However, if you
are labelling something with /w/ which looks like an integer from your
explanation, then first you want to make a variation of the Tableau
datatype that holds the label, thus rewrite would be a type changing
function:

rewrite :: Tableau -> Tableau'

I think the basic tableau data type would look like:

data Tableau = Node (World, Expr) [Tableau]
type World = Int

and the rewrite function would need to track the current position of rewrite
in the tableau and store a complete tableau (or some kind of record, possibly
in a zipper) in order to move around, depending on the instruction it's given. So
I would need something like:

rewrite :: Tableau -> State (Record, Tableau)

So that it could be passed an instruction such as:

(Poss, [ex]) -> (a) inject ex into Tableau; (b) Store
Tableau in Record; (c) move to correct spot in Record;
(d) restart rewriting from position in Record.

Even though Haskell's my first language, I still want a function that says: store
current Tableau in r, then get r and restart.

If this is what you want to do, you should be able to thread "number
supply" through the rewrite and rule functions fairly simply with a
state monad.

rewrite :: Tableau -> State Int Tableau'

I think this means that when implementing the monad, I should define (>>=) as a
general rule similar to the set of instructions above, e.g,. if f is a function that
injects the list ex into a tree structure, and g is a rewrite function, then >>= should
have a structure abstracted from the following:

f >>= g = do f ~> State Record Tableau
            store Tableau in Record
               do g at Record
                  make Record into current Tableau

This seems similar to the "threading" method that, for instance, Wadler uses in the first
sections of his paper on functional programming and monads, when building an evaluator
that keeps track of division operations.

Thanks or the response. If you see any glaring 'monadic errors,' I'd be happy to hear about
them, but your advice was helpful :)