Well-Definedness and Semantic Type-Checking in the Nested Relational Calculus and XQuery

TL;DR

This paper investigates the decidability of well-definedness and semantic type-checking in XQuery and nested relational calculus, revealing undecidability in general but decidability in certain restricted variants.

Contribution

It establishes the undecidability of key decision problems in XQuery and nested relational calculus, and identifies conditions under which these problems become decidable.

Findings

Well-definedness and semantic type-checking are undecidable in general.

Decidability is achieved for a restricted 'pure' variant of XQuery.

The results extend to the nested relational calculus setting.

Abstract

Two natural decision problems regarding the XML query language XQuery are well-definedness and semantic type-checking. We study these problems in the setting of a relational fragment of XQuery. We show that well-definedness and semantic type-checking are undecidable, even in the positive-existential case. Nevertheless, for a ``pure'' variant of XQuery, in which no identification is made between an item and the singleton containing that item, the problems become decidable. We also consider the analogous problems in the setting of the nested relational calculus.