dag – Termination of term rewiting using strict partial order on subterms


Are there any good books, research reports, surveys, theses, or papers that display proof techniques, with clear proofs of termination of term rewriting problems that have the following form…?

Terms are represented by directed acyclic graphs where the terms are vertices with arcs labelled $arg_{1}…arg_{n}$ pointing to the immediate sub-terms. There would be additional equality arcs between vertices. Thinking of the transitive closure of the equality arcs as representing equivalence classes of vertices that are “merged”, the $arg$ arcs in the graph form a lattice (because or the strict order on sub-terms, and some sub-terms might be shared). A rewrite rule would add extra arcs, such that existing partial order would be preserved and added to, so the rewrite rules would be constructing a series of partial orders (represented in the graph state at each step) $p_{0} subset … subset p_{m}$ more and more “constraining” the partial order relation between vertices until either the re-write rules find nothing to re-write or a rewrite would introduce a cycle (immediately detectable by a depth first search). I think this kind of termination proof is correct because we can say every step was a reduction under the partial order $p_{m}$ but I’d like a formal justification because I have worries about my not knowing $p_{m}$ before hand, only when it is constructed. And if the rewrite finds a cycle then that cycle was implicit from the beginning. Again I think that’s OK because my re-write rules are prove-ably LHS iff RHS so they transform the problem to an equivalent problem. I call this “construct a partial order or die trying.” Is there a more formal name for this kind of proof?

Ideally the proof examples would be constructive and mathematically thorough. I see some papers that assume a lot of prior knowledge, probably because of brevity requirement, and not wanting to bore an expert audience. And others with “wordy” explanations, which are great to give intuitive understanding, but proofs should not depend on them.