XPath with transitive closure
Seminar Room 1, Newton Institute
We determine the expressivity of the expansion of Core XPath with a reflexive transitive closure operator. This expansion is known under the name "Regular XPath". It allows us to write expressions as (child::*/child::*)+ meaning "give me all nodes which are an even number of steps below me", and filter expressions like "I have an even number of descendants". The transitive closure operator is NOT part of the XPath 1.0 or 2.0 standards, but is available in the XSLT processors SAXON and XALAN.
Regular XPath can be seen as a variant of Propositional Dynamic logic, with four programs (child, parent, left, right) and propositional variables corresponding to XML tag names. Core XPath corresponds to a fragment of PDL in which the Kleene star may only be applied to atomic programs.
Interestingly, in order to obtain a nice characterization of Regular XPath in terms of first order logic expanded with transitive closure, we need to add something more to Core XPath. This extra addition can be phrased in a number of different ways. One is the following: if P and Q are path expressions, then P=Q is a filter expression. P=Q is true at a node n iff there exists a node m which is reachable from n by both P and Q. At present we do not know if this extra addition is really needed.