Limiting until in ordered tree query languages
Marx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete – that is it cannot express every query definable in first-order logic over the naviga- tional predicates. How can one extend XPath to get a first-order complete language? Marx has...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Published: |
Association for Computing Machinery
2016
|
| _version_ | 1826290760748630016 |
|---|---|
| author | Benedikt, M Ley, C |
| author_facet | Benedikt, M Ley, C |
| author_sort | Benedikt, M |
| collection | OXFORD |
| description | Marx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete – that is it cannot express every query definable in first-order logic over the naviga- tional predicates. How can one extend XPath to get a first-order complete language? Marx has shown that Conditional XPath – an extension of XPath with an “Until” operator – is first order complete. The com- pleteness argument makes essential use of the presence of upward axes in Conditional XPath. We examine whether it is possible to get “forward-only” languages that are first-order complete for Boolean queries on ordered trees. It is easy to see that a variant of the temporal logic CTL ∗ is first-order complete; the vari- ant has path quantifiers for downward, leftward and rightward paths, while along a path one can check arbitrary formulas of linear temporal logic (LTL). This language has two major disadvantages: it requires path quantification in both horizontal directions (in particular, it requires looking backward at the prior siblings of a node), and it requires the consideration of formulas of LTL of arbitrary complexity on vertical paths. This last is in contrast with Marx’s Conditional XPath, which requires only the checking of a single Until operator on a path. We investigate whether either of these restrictions can be eliminated. Our main results are negative ones. We show that if we restrict our CTL ∗ language by having an until operator in only one horizontal direction, then we lose completeness. We also show that no restriction to a “small” subset of LTL along vertical paths is sufficient for first order completeness. Smallness here means of bounded “Until Depth”, a measure of complexity of LTL formulas defined by Etessami and Wilke. In particular, it follows from our work that Conditional XPath with only forward axes is not expressively complete; this extends results proved by Rabinovich and Maoz in the context of infinite unordered trees. |
| first_indexed | 2024-03-07T02:49:07Z |
| format | Journal article |
| id | oxford-uuid:ad100836-30c0-45ad-8f1a-052644a6fd93 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T02:49:07Z |
| publishDate | 2016 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:ad100836-30c0-45ad-8f1a-052644a6fd932022-03-27T03:33:04ZLimiting until in ordered tree query languagesJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:ad100836-30c0-45ad-8f1a-052644a6fd93Symplectic Elements at OxfordAssociation for Computing Machinery2016Benedikt, MLey, CMarx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete – that is it cannot express every query definable in first-order logic over the naviga- tional predicates. How can one extend XPath to get a first-order complete language? Marx has shown that Conditional XPath – an extension of XPath with an “Until” operator – is first order complete. The com- pleteness argument makes essential use of the presence of upward axes in Conditional XPath. We examine whether it is possible to get “forward-only” languages that are first-order complete for Boolean queries on ordered trees. It is easy to see that a variant of the temporal logic CTL ∗ is first-order complete; the vari- ant has path quantifiers for downward, leftward and rightward paths, while along a path one can check arbitrary formulas of linear temporal logic (LTL). This language has two major disadvantages: it requires path quantification in both horizontal directions (in particular, it requires looking backward at the prior siblings of a node), and it requires the consideration of formulas of LTL of arbitrary complexity on vertical paths. This last is in contrast with Marx’s Conditional XPath, which requires only the checking of a single Until operator on a path. We investigate whether either of these restrictions can be eliminated. Our main results are negative ones. We show that if we restrict our CTL ∗ language by having an until operator in only one horizontal direction, then we lose completeness. We also show that no restriction to a “small” subset of LTL along vertical paths is sufficient for first order completeness. Smallness here means of bounded “Until Depth”, a measure of complexity of LTL formulas defined by Etessami and Wilke. In particular, it follows from our work that Conditional XPath with only forward axes is not expressively complete; this extends results proved by Rabinovich and Maoz in the context of infinite unordered trees. |
| spellingShingle | Benedikt, M Ley, C Limiting until in ordered tree query languages |
| title | Limiting until in ordered tree query languages |
| title_full | Limiting until in ordered tree query languages |
| title_fullStr | Limiting until in ordered tree query languages |
| title_full_unstemmed | Limiting until in ordered tree query languages |
| title_short | Limiting until in ordered tree query languages |
| title_sort | limiting until in ordered tree query languages |
| work_keys_str_mv | AT benediktm limitinguntilinorderedtreequerylanguages AT leyc limitinguntilinorderedtreequerylanguages |