Sesión Lógica y Computabilidad (II)

Diciembre 14, 11:20 ~ 11:40

Axiomatizations for Downward XPath on Data Trees

Descotte, Maria Emilia

XML (eXtensible Markup Language) is the most successful language for data exchange on the web. An XML document can be abstracted as a data tree, where nodes have labels (such as {\em LastName}) from a finite domain, and data values (such as {\em Smith}) from an infinite domain. For some tasks, data values can be disregard (for instance, checking whether a given XML document conforms to a schema specification). But many applications require data-aware query languages, that is, languages with the ability of comparing data values. XPath is the most widely used query language for XML documents. It has syntactic operators or \textquoteleft axes\textquoteright \ to navigate the tree using the \textquoteleft child\textquoteright, \textquoteleft parent\textquoteright, \textquoteleft sibling\textquoteright, etc. accessibility relations, and can make tests on intermediate nodes. CoreXPath is the fragment of XPath 1.0 containing only the navigational behavior of XPath, i.e. without any reference to the data in the queries. This language can be seen as a {\em modal language}, such as Linear Temporal Logic (LTL) or Propositional Dynamic Logic (PDL), and has been already investigated from this point of view. CoreDataXPath is the extension of CoreXPath with (in)equality tests between attributes of elements in an XML document. It is important to be aware that CoreDataXPath can only compare data values at the end of paths by equality or inequality but it cannot compare the data value of a node with a constant. The rationale of this feature is twofold: on the one hand, it remains a finitary language; on the other, its semantics is invariant over renaming of data values. Whilst the model theory of CoreDataXPath was recently investigated both for the node expressions fragment and for the path expressions fragment, the only research into the proof theory of CoreDataXPath outside of this work is for a simpler fragment. Obtaining a complete axiomatization has applications in static analysis of queries, such as optimization through query rewriting. Studying complete axiomatizations can also give us an alternative method for solving the validity problem, which is undecidable for the full logic CoreDataXPath, but it is decidable when the only axis present in the language is \textquoteleft child\textquoteright, and in fact, also when adding \textquoteleft descendant\textquoteright (also for other fragments). In this work, we give sound and complete axiomatizations for CoreDataXPath with \textquoteleft child\textquoteright\ as the only axis. We call this fragment \textquoteleft Downward XPath\textquoteright. We extend a previous axiomatization of CoreXPath (no data involved) with the needed axioms to obtain all validities of Downward XPath. Our axiomatizations are equational. We prove soundness and completeness theorems both for node expressions and for path expressions. Our completeness proof relies on a normal form theorem for expressions of Downward XPath, and a construction of a canonical model for any consistent formula in normal form. We proceed gradually. To warm up, we first show an axiomatization for the fragment with all Boolean operators, with equality tests, but keeping out inequality tests. This fragment is still interesting since it allows us to express the join query constructor. Then we give the axiomatization for the full Downward XPath, whose proof is more involved but uses some ideas from the simpler case.

Autores: Abriola, Sergio / Descotte, Maria Emilia / Fervari, Raul / Figueira, Santiago.