Revisiting "forward node-selecting queries over trees"

In “Forward Node-Selecting Queries over Trees”, Olteanu (TODS 32(1):A3, 2007) gives three rewriting systems for eliminating reverse XPath axis steps from node-selecting queries over trees, together with arguments for their correctness and termination for a large class of input graphs, including cyclic ones. These proofs are valid for tree or acyclic formulas, but two of the rewrite systems (TRS2 and TRS3) do not terminate on cyclic graphs — that is, there are infinite rewrite sequences that never yield a normal form. We investigate the reasons why the termination arguments do not work for general cyclic formulas, and develop alternative algorithms that can be used instead. We prove that TRS2 is weakly normalizing, while TRS3 is not weakly normalizing, but it can be extended to a weakly normalizing system TRS3◦. The algorithms and proof techniques illustrate unforeseen subtleties in the handling of cyclic queries.