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

arXiv:cs/0406060v1 [cs.DB] 29 Jun 2004

Jan Van den Bussche1 , Dirk Van Gucht2⋆ , and Stijn Vansummeren1⋆⋆
1

Limburgs Universitair Centrum
Diepenbeek, Belgium
jan.vandenbussche@luc.ac.be, stijn.vansummeren@luc.ac.be
2
Indiana University
Bloomington, Indiana, USA
vgucht@cs.indiana.edu

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.

⋆
⋆⋆

The author is supported by NSF Grant IIS-0082407
Research Assistant of the Fund for Scientific Research - Flanders (Belgium)

2

1

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

Introduction

Much attention has been paid recently to XQuery, the XML query language currently under development by the World Wide Web Consortium [5, 9]. Unlike in
traditional query languages, expressions in XQuery can have an undefined meaning (i.e., these expressions produce a run-time error). As an example, consider
the following variation on one of the XQuery use cases [7]:
<bib> {
for $b in $bib/book
where $b/publisher = "Springer-Verlag"
return element{$b/author}{$b/title}
} </bib>
This expression should create for each book published by Springer-Verlag a node
whose name equals the author of the book, and whose child is the title of the
book. If there is a book with more than one author node however, then the
result of this expression is undefined because the first argument to the element
constructor must be a singleton list.
This leads us to the natural question whether we can solve the well-definedness
problem for XQuery: given an expression and an input type, check whether the
semantics of the expression is defined for all inputs adhering to the input type.
This problem is undecidable for any computationally complete programming
language, and hence also for XQuery. Following good programming language
practice, XQuery therefore is equipped with a static type system (based on XML
Schema [4, 18]) which ensures “type safety” in the sense that every expression
which passes the type system’s tests is guaranteed to be well-defined. Due to the
undecidability of the well-definedness problem, such type systems are necessarily
incomplete, i.e., there are expressions which are well-defined, but not well-typed.
Can we find fragments of XQuery for which the well-definedness problem
is decidable? In this paper we will study Relational XQuery (RX), a set-based
fragment of XQuery where we omit recursive functions, only allow the child axis,
take a value-based point of view (i.e., we ignore node identity), and use a type
system similar to that of the nested relational or complex object data model [1,
6, 19]. We regard RX as the “first-order database fragment” of XQuery.
Even for RX, the well-definedness problem is still undecidable, due to two
features which allow us to simulate the relational algebra: quantified expressions
and type switches. Surprisingly, however, well-definedness remains undecidable
for RX without these features, which we call positive-existential RX or PERX
for short.
The core difficulty here is due to the fact that in the XQuery data model
an item is identified with the singleton containing that item [11]. In a set-based
model this identification becomes difficult to analyze, since {i, j} is a singleton
if and only if i = j. Since, as shown in the example above, there are expressions
which are undefined on non-singleton inputs, this implies that in order to solve
the well-definedness problem, one also needs to solve the equivalence problem.
Indeed, we will see that the equivalence problem for PERX is undecidable.

Well-Definedness and Semantic Type-Checking

3

Nevertheless, for a “pure” variant of PERX, in which no identification is
made between an item and the singleton containing that item, well-definedness
becomes decidable. We actually prove this result not for pure PERX itself, but
for PENRC: the positive-existential fragment of the nested relational calculus
[6, 19], which is well-known from the complex object data model, and whose
well-definedness problem is interesting in its own right.
All our results hold not only for well-definedness, but also for semantic typechecking: given an expression, an input type and an output type, check whether
the expression always returns outputs adhering to the output type on inputs
adhering to the input type.
In the main body of the paper we will work in a set-based data model.
Considering that the real XML data model is list-based, at the end of the paper
we will discuss how and if our results transfer to a list-based or bag-based setting.
Related work The semantic type-checking problem has already been studied extensively in XML-related query languages [2, 3, 13–15, 17]. In particular, our setting closely resembles that of Alon et al. [2, 3] who, like us, study the problem in
the presence of data values. In particular they have shown that (un)decidability
depends on the expressiveness of both the query language and the type system.
While the query language of Alon et al. can simulate PERX, our results do
not follow immediately from theirs, since their type system is incompatible with
ours [16].

2

Relational XQuery

In what follows we will need to define various query languages. In some definitions
it will help to talk abstractly about a query language. To this end, we define a
query language Q as a tuple (V, T, E, J.K) where V is a set of values; T is a set
of types; E is a set of expressions; and J.K is the interpretation function giving
a semantics to types and expressions. The set V is also referred to as the data
model.
We assume to be given an infinite set X = {x, y, . . . } of variables. Every
expression e has associated with it a finite set FV (e) ⊆ X of free variables.
An environment on e is a function σ : FV (e) → V which associates to each
x ∈ FV (e) a value σ(x) ∈ V . A type assignment on e is a function Γ : FV (e) → T
which associates to each x ∈ FV (e) a type Γ (x) ∈ T . If ρ is an environment (or
a type assignment), and v is a value (respectively a type), then we write x : v, ρ
for the environment (respectively type assignment) ρ′ with domain dom(ρ)∪{x}
such that ρ′ (x) = v and ρ′ (y) = ρ(y) for y 6= x. Intuitively, environments describe
the input to expressions, and type assignments describe their type.
Every type τ is associated with a set Jτ K of values. An environment σ is
compatible with a type assignment Γ , denoted by σ ∈ Γ , if they have the same
domain and σ(x) ∈ JΓ (x)K for all x. Every expression e has associated with it
a (possibly partial) computable function JeK which associates environments on
FV (e) to values in V . We call JeK the semantics of e.

4

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

In order not to burden our notation we will identify types and expressions
with their respective interpretations, and write for example e(σ) for JeK(σ).
2.1

Relational XQuery data model

In this section we define a set-based fragment of the XQuery data model [11]
called the Relational XQuery (RX) data model. We take a value-based point of
view (i.e., we ignore node identity), focus on data values, element nodes and
data nodes (known as text nodes in XQuery), and abstract away from the other
features in the XQuery data model such as attributes.
We assume to be given a recursively enumerable set A = {a, b, . . . } of atoms.
An item is an atom or a node. A node is either an element node ha : N i or a data
node hai, where a ∈ A and N is a finite set of nodes (N is called the content of
the element node). An RX-value, finally, is any finite set of items.
An RX-type τ is a term generated by the following grammar:
τ ::= coll(ι) | single(ι)
ι ::= atom | ν | ι ∪ ι
ν ::= data | elem(γ) | ν ∪ ν
γ ::= coll(ν) | single(ν)
Here, τ ranges over types, ι ranges over item types, ν ranges over node types,
and γ ranges over node content types. An RX-type denotes a set of RX-values:
– data denotes the set of all data nodes,
– elem(γ) denotes the set of all element nodes ha : N i for which N is a finite
set over the denotation of γ,
– atom denotes the set A of all atoms,
– ι1 ∪ ι2 denotes the union of the denotations of ι1 and ι2 ,
– coll(ι) denotes the set of all finite sets over the denotation of ι, and
– single(ι) denotes the set of all singletons over the denotation of ι.
Note that every γ is also a τ , and hence the denotation of terms produced by γ
is subsumed in the definition above.
An RX-kind κ is a term generated by the following grammar:
κ ::= atom | data | elem | κ ∪ κ
An RX-kind denotes a set of items, which can be the set of all atoms, the set of
all data nodes, the set of all element nodes, or the union of the denotations of
two kinds.
Discussion The type system we have defined above is quite simple. Types merely
indicate the many-or-one cardinality of a value, and the kinds of items that can
appear in it. Only values of a fixed maximal nesting height can be described in
our type system. This is justified because the expressions in the XQuery fragment
RX we will work with in this paper can look only a fixed number of nesting levels

Well-Definedness and Semantic Type-Checking

5

down anyway. Also, it is a public secret that most XML documents in practice
have nesting heights at most five or six, and that unbounded-depth nesting is
not needed for many XML data processing tasks.
The presence of the single type constructor is justified by the fact that an
item i is identified with the singleton set {i} in the XQuery data model [11].
Consequently, an XQuery expression in which the input is always expected to
be a string actually receives singleton strings as inputs. Its input type would
therefore be single(atom) in our setting.
Our types also do not specify anything about the names of element nodes,
but this is an omission for the sake of simplicity; we could have added node types
of the form elema (γ), with a the atom that must be the name of the element
node, without sacrificing any of the results we present in this paper.
2.2

Relational XQuery syntax and semantics

A Relational XQuery expression is an expression generated by the following
grammar:
e ::= x
| text {e} | elem {e}{e} | data(e) | name(e) | children (e)
| () | e, e | for x : κ in e return e
| if e eq e then e else e | if e = ∅ then e else e | if e ∈ τ then e else e
Here, e ranges over RX-expressions, x ranges over variables, τ ranges over RXtypes and κ ranges over RX-kinds. The free variables of e are defined in the
usual way, and will be denoted by FV (e).
The semantics of RX is parameterized by two “oracle” functions:
– content, which maps element nodes to atoms; and
– concat , which maps finite sets of atoms to atoms.
We further define the following (partial) functions on values:
– data(v) = {a | a ∈ v} ∪ {a | hai ∈ v} ∪ {content(ha : N i) | ha : N i ∈ v},
– name(v), which is {a} if v is a singleton element node {ha : N i}; concat (v)
if v is empty; and undefined otherwise.
– children (v), which is undefined if there is some atom in v, and otherwise
returns
[
{N | ha : N i ∈ v}.

– construct(v, w) which is undefined if data(v) is not a singleton atom {a}; and
returns ha : N i otherwise, where N is obtained from w by replacing every
atom in w by a corresponding data node:
N = {hai | a ∈ w} ∪ {i | i ∈ w, i is a node}.

6

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

Let e be an RX-expression and let σ be an RX-environment on e.3 The
semantics e(σ) of e under σ can now be inductively defined as follows:
x(σ) = σ(x)
text {e} = {hconcat (data(e(σ)))i}
elem {e1 }{e2 }(σ) = {construct(e1 (σ), e2 (σ))}
data(e)(σ) = data(e(σ))
name(e)(σ) = name(e(σ))
children(e)(σ) = children (e(σ))
()(σ) = ∅
e1 , e2 (σ) = e1 (σ) ∪ e2 (σ)
[
for x : κ in e1 return e2 = {e2 (x : {i}, σ) | i ∈ e1 (σ) ∩ κ}

e3 (σ) if data(e1 (σ)) = data(e2 (σ)) = {a},




with a an atom
(if e1 eq e2 then e3 else e4 )(σ) =

e4 (σ) if data(e1 (σ)) = {a}, data(e2 (σ)) = {b},



with a, b atoms, a 6= b
(
e2 (σ) if e1 (σ) = ∅
(if e1 = ∅ then e2 else e3 )(σ) =
e3 (σ) otherwise
(
e2 (σ) if e1 (σ) ∈ τ
(if e1 ∈ τ then e2 else e3 )(σ) =
e3 (σ) otherwise

Note that e(σ) is not necessarily defined: this models the situations in which
XQuery expression evaluation produces a run-time error. Specifically, e(σ) can
become undefined for the following reasons:
– e = elem {e1 }{e2 }, and data(e1 (σ)) is not a singleton atom. (This can only
happen if e1 (σ) is not a singleton.)
– e = name(e′ ), and e′ (σ) is not a singleton element node.
– e = children(e′ ), and e′ (σ) contains an atom.
– e = if e1 eq e2 then e3 else e4 , and data(e1 (σ)) is not a singleton atom, or
data(e2 (σ)) is not a singleton atom. (This can only happen if e1 (σ) respectively e2 (σ) is not a singleton.)
Relation to XQuery The RX query language corresponds to a set-based version
of XQuery [5, 9] where we have omitted recursive functions, literals, arithmetic
expressions, generalized and order comparisons, and only allow the children axis.
We have replaced XQuery quantified expressions by the emptiness test (which
is equivalent in expressive power), and have moved kind tests from XQuery step
3

Recall from the beginning of this section that σ assigns an RX-value to each free
variable of e.

Well-Definedness and Semantic Type-Checking

7

expressions to the “for” expression. As an example, the XQuery step expression
$x/child :: text() can be expressed in RX as
for z : data in children (x) return z.
The “oracle” functions concat and content model features which are present
in XQuery, but which are clumsy to take into account in our data model. For
example name applied to the empty set returns the empty string in XQuery.
Furthermore, applying data to a singleton element node in XQuery returns the
“string content” of the node. This is (roughly speaking) a concatenation of all
atoms (converted to strings) encountered in a depth-first left-to-right traversal
of the node’s content.

3

Well-definedness and semantic type-checking

As we have noted in Section 2.2, the semantics e(σ) of RX-expression e under
environment σ can be undefined. This leads us to the following definition.
Definition 1. The well-definedness problem for a query language Q consist of
checking, given a Q-expression e and a Q-type assignment Γ on e: whether e(σ)
is defined for every σ ∈ Γ . In this case we say that e is well-defined under Γ .
A problem which is related to well-definedness is the semantic type-checking
problem:
Definition 2. The semantic type-checking problem for a query language Q consist of checking, given a Q-expression e, a Q-type assignment Γ on e such that
e is well-defined under Γ , and a Q-type τ : whether e(σ) ∈ τ for every σ ∈ Γ . In
this case we say that τ is an output type for e under Γ .

4

Undecidability results

We will show that well-definedness for RX is undecidable, even for a quite restricted fragment. Our results do not depend on the particular interpretation
given to the oracle functions concat and content.
Let us begin by defining RX− as the fragment of RX where
– we disallow data node construction expressions of the form text {e};
– we disallow data extraction expressions of the form data(e); and
– we disallow kind tests, or equivalently, we only allow the use of the single
“universal” kind atom ∪ data ∪ elem.
An RX− -expression e is positive existential if it does not contain emptiness
tests of the form if e1 = ∅ then e2 else e3 , or type switches of the form if e1 ∈
τ then e2 else e3 . We denote the language of all positive-existential RX− expressions by PERX− , and we will mention specific features added back to PERX− in
square brackets. Thus, PERX− [empty] includes emptiness tests, and PERX− [type]
includes type switches.

8

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

Proposition 1. PERX− [type] is equivalent to RX− ; in other words, type switches
can be used to simulate emptiness tests.
Indeed, if e1 = ∅ then e2 else e3 can be expressed as follows:
if (for x in e1 return elem {a}{()}) ∈ coll(data) then e2 else e3
The following proposition is not surprising, and parallels earlier results on
semistructured query languages such as StruQL [10]:
Proposition 2. PERX− [empty] can simulate the relational algebra. Concretely,
for every relational algebra expression φ over database schema S, there exists a
PERX− [empty]-expression eφ and a type assignment ΓS , such that
– eφ is well-defined under ΓS , and,
– eφ evaluated on an encoding of database D equals an encoding of φ(D).
The simulation is described in Appendix A.
Consequently, satisfiability (i.e., nonempty output on at least one input) is
undecidable for PERX− [empty] (and thus for RX− ), because it is undecidable
for the relational algebra. Since the expression
for x in e return elem {()}{()}
is well-defined if, and only if, e is unsatisfiable, we obtain:
Corollary 1. Well-definedness for PERX− [empty] (and thus RX) is undecidable.
What is perhaps more surprising is that without emptiness test, we remain
undecidable:
Theorem 1. Well-definedness for PERX− is undecidable.
Proof (Crux). The proof goes by reduction from the implication problem for
functional and inclusion dependencies, which is known to be undecidable [1, 8].
Let Σ be a set of functional and inclusion dependencies, and let ρ be an inclusion dependency. We show in Appendix B that we can construct two expressions
e1 and e2 , a type assignment Γ and a node content type γ, such that
– e1 and e2 are well-defined under Γ ,
– γ is an output type for e1 and e2 under Γ , and,
– e1 (σ) = e2 (σ) for every σ ∈ Γ if, and only if, ρ is implied by Σ.
Consequently, the expression name(elem {a}{e1 }, elem {a}{e2 }) is well-defined
under Γ if, and only if, ρ is implied by Σ.
⊓
⊔
As a corollary to the proof, we note:
Corollary 2. Equivalence of PERX− expressions is undecidable.

Well-Definedness and Semantic Type-Checking

9

We further derive:
Corollary 3. Semantic type-checking for PERX− is undecidable.
Indeed, referring to the above proof sketch of Theorem 1, e1 and e2 are equivalent
if, and only if, (elem {a}{e1}, elem {a}{e2}) has output type single(elem(γ)).
We remark that to establish undecidability of well-definedness we do not need
singleton types. For undecidability of semantic type-checking, we do.

5

Pure RX

In the XQuery data model, an item i is identified with the singleton {i} [11].
With this identification, it is indeed natural to let, e.g., name(e) be undefined
when e(σ) is a set with more than one element. As we have seen in the previous
Section, it is exactly this behavior that causes well-definedness to be undecidable.
So let us define a version of RX, called pure RX, which does not explicitly
identify an item i with {i}. We will show in Section 6 that well-definedness
and semantic type-checking for the positive-existential fragment of pure RX is
decidable.
A pure RX-value is an item or a set of items. A pure RX-type τ is a term
generated by the following grammar:
τ ::= coll(ι) | ι | τ ∪ τ
ι ::= atom | ν | ι ∪ ι
ν ::= data | elem(ν1 ∪ · · · ∪ νk )
Here, τ ranges over types, ι ranges over item types, ν ranges over node types,
and k ≥ 0.
A pure RX-type denotes a set of pure RX-values:
– data denotes the set of all data nodes,
– elem(ν1 ∪ · · · ∪ νk ) denotes the set of all element nodes ha : N i for which N
is a finite set over the union of the denotations of ν1 , . . . , νk .
– atom denotes the set A of all atoms,
– τ1 ∪ τ2 denotes the union of the denotations of τ1 and τ2 , and,
– coll(ι) denotes the set of all finite sets over the denotation of ι.
Note that since every ι is also a τ , the denotation of ι1 ∪ ι2 is subsumed by the
definition above.
The syntax of pure RX is obtained from the syntax of RX by adding a
singleton constructor expression (e), and by replacing RX-types in type switch
expressions by pure RX types.
In order to give the semantics of pure RX, we define the following (partial)
functions on pure RX-values.
– data ′ (v) = {a | a ∈ v} ∪ {a | hai ∈ v}

10

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

– name ′ (v), which is a if v is an element node ha : N i, and is undefined otherwise.
– children ′ (v), which undefined if there is some atom in v, and otherwise returns
[
{N | ha : N i ∈ v}.
– construct ′ (v, w) which is undefined if v is not an atom, and returns hv : N i
otherwise where N is obtained from w by replacing every atom in w by a
corresponding data node:
N = {hai | a ∈ w} ∪ {i | i ∈ w, i is a node}
The semantics of pure RX is then defined as follows:
x(σ) = σ(x)
text {e}(σ) = hai if e(σ) = a
elem {e1 }{e2 }(σ) = construct′ (e1 (σ), e2 (σ))
data(e)(σ) = data ′ (e(σ))
name(e)(σ) = name ′ (e(σ))
children(e)(σ) = children ′ (e(σ))
()(σ) = ∅
(e)(σ) = {e(σ)} if e(σ) is an item
e1 , e2 (σ) = e1 (σ) ∪ e2 (σ)
[
for x : κ in e1 return e2 = {e2 (x : i, σ) | i ∈ e1 (σ) ∩ κ}
(
e3 (σ) if e1 (σ), e2 (σ) ∈ A and e1 (σ) = e2 (σ)
(if e1 eq e2 then e3 else e4 )(σ) =
e4 (σ) if e1 (σ), e2 (σ) ∈ A and e1 (σ) 6= e2 (σ)
(
e2 (σ) if e1 (σ) = ∅
(if e1 = ∅ then e2 else e3 )(σ) =
e3 (σ) otherwise
(
e2 (σ) if e1 (σ) ∈ τ
(if e1 ∈ τ then e2 else e3 )(σ) =
e3 (σ) otherwise

Note that again e(σ) is not necessarily defined. Specifically, e(σ) can become
undefined for the following reasons:
–
–
–
–
–
–
–

e = text {e′ }, and e′ (σ) is not an atom,
e = elem {e1 }{e2 }, and e1 (σ) is not an atom,
e = name(e′ ), and e′ (σ) is not an element node,
e = children(e′ ), and e′ (σ) contains an atom,
e = (e′ ), and e′ (σ) is not an item,
e = e1 , e2 , and e1 (σ) is not a set or e2 (σ) is not a set, or,
e = if e1 eq e2 then e3 else e4 , and e1 (σ) or e2 (σ) is not an atom.

Well-Definedness and Semantic Type-Checking

11

Pure PERX
Clearly, well-definedness and semantic type-checking for the entire pure RX remains undecidable due to the presence of the emptiness test and type switch
expressions. Let us define pure PERX as the fragment of pure RX in which
these expressions are disallowed.

6

Decidability results

In this section we will show that well-definedness and semantic type-checking for
pure PERX are decidable. In fact, we will solve the corresponding problems for
the nested relational calculus (NRC): the well-known standard query language
for nested relations and complex objects. Indeed, this language remains fundamental and its study remains interesting in its own right. As we will see, pure
PERX can be simulated by the positive-existential fragment of NRC (extended
with kind-tests).
6.1

Nested relational calculus

An NRC-value is either an atom, a pair of NRC-values, or a finite set of NRCvalues. Note that we allow sets to be heterogeneous. If v = (v1 , v2 ), then we
write π1 (v) for v1 and π2 (v) for v2 .
An NRC-type τ is a term generated by the following grammar:
τ ::= ∅ | atom | τ × τ | τ ∪ τ | coll(τ )
An NRC-type denotes a set of NRC-values:
–
–
–
–
–

∅ denotes the empty set,
atom denotes the set A of all atoms,
τ1 × τ2 denotes the cartesian product of the denotations of τ1 and τ2 ,
τ1 ∪ τ2 denotes the union of the denotations of τ1 and τ2 , and,
coll(τ ) denotes the set of all finite sets over the denotation of τ .
An NRC-kind κ is a term generated by the following grammar:
κ ::= atom | coll | κ × κ | κ ∪ κ

An NRC-kind denotes a set of NRC-values, which can be the set of all atoms,
the set of all finite sets of values, the cartesian product of the denotation of two
kinds, or the union of the denotation of two kinds.
The positive existential nested relational calculus (PENRC) is the set of all
expressions generated by the following grammar:
e ::= x
| (e, e) | π1 (e) | π2 (e)
[
| ∅ | {e} | e ∪ e |
e | {e | x ∈ e}
| e=e?e : e

12

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

Here e ranges over expressions, and x ranges over variables. The PENRC with
kind tests, denoted by PENRC[kind] is the PENRC extended with one additional
expression:
e ::= · · · | e ∈ κ ? e : e
Here, κ ranges over NRC kinds. The free variables of e are defined in the usual
way, and will be denoted by FV (e).
If e is a PENRC[kind]-expression and σ is an NRC-environment on e, then
the semantics e(σ) of e under σ is inductively defined as follows:
x(σ) = σ(x)
(e1 , e2 )(σ) = (e1 (σ), e2 (σ))
π1 (e)(σ) = π1 (e(σ))
π2 (e)(σ) = π2 (e(σ))
∅(σ) = ∅
{e}(σ) = {e(σ)}
(e1 ∪ e2 )(σ) = e1 (σ) ∪ e2 (σ)
[
[
( e)(σ) =
e(σ)

{e2 | x ∈ e1 }(σ) = {e2 (x : v, σ) | v ∈ e1 (σ)}
(
e3 (σ) if e1 (σ), e2 (σ) ∈ A and e1 (σ) = e2 (σ)
(e1 = e2 ? e3 : e4 )(σ) =
e4 (σ) if e1 (σ), e2 (σ) ∈ A and e1 (σ) 6= e2 (σ)
(
e2 (σ) if e1 (σ) ∈ κ
(e1 ∈ κ ? e2 : e3 )(σ) =
e3 (σ) otherwise
Note that e(σ) can be undefined. For example π1 (x)(σ) is undefined when σ(x)
is not a pair, and (x ∪ y)(σ) is undefined when σ(x) is not a set. Hence, we can
also study the well-definedness problem for PENRC[kind].
It is easy to see that well-definedness for full NRC: PENRC extended with an
emptiness test, is undecidable. Indeed, it is well known that NRC can simulate
the relational algebra [6].
6.2

Simulating RX in NRC

Formally, a simulation of a query language Q in a query language Q′ is a function
enc : VQ → VQ′ such that
– for every type τ ∈ TQ there exits a type τ ′ ∈ TQ′ such that v ∈ τ if and only
if enc(v) ∈ τ ′ , and
– for every expression e ∈ EQ there exists an expression e′ ∈ EQ′ such that
1. e(σ) is defined if and only if e′ (enc(σ)) is defined, and
2. if e(σ) is defined, then enc(e(σ)) = e′ (enc(σ)).

Well-Definedness and Semantic Type-Checking

13

A simulation is effective if τ ′ can be computed from τ and e′ can be computed
from e.
Lemma 1. Pure PERX can be effectively simulated in PENRC[kind].
Proof (Crux). Consider the encoding function enc for which
enc(a) = a
enc(ha : N i) = (a, enc(N ))

enc(hai) = ((a, a), ∅)
enc(v) = {enc(i) | i ∈ v}

Then enc is an effective simulation. It is easy to find τ ′ by induction on τ .
Furthermore, as shown in Appendix C, e′ can be constructed by induction on e.
To illustrate this, we first introduce some syntactic sugar: we write e1 ∈ κ → e2
for e1 ∈ κ ? e2 : π1 (∅). Intuitively, this expression will be used to verify that the
input to e′ is an encoding of a legal input to e. Otherwise, we become undefined.
We can now for example simulate hei by e′ ∈ atom → ((e′ , e′ ), ∅). We can
simulate he1 : e2 i by
e′1 ∈ atom → (e′1 , {x ∈ atom ? ((x, x), ∅) : x | x ∈ e′2 }).
S
And we can simulate children (e) by {π2 (x) | x ∈ e′ }.

⊓
⊔

Corollary 4. If the well-definedness or semantic type-checking problem is decidable for PENRC[kind], then it is also decidable for pure PERX.
6.3

Well-definedness for pure PENRC[kind]

Consider the following expression:
e = {{z = y ? π1 (z) : y | y ∈ x}) | x ∈ R}
and let the environment σ be defined by
σ(R) = {{a, b}, {c}, {a, b, d}}}

σ(z) = d.

Since there is a set in σ(R) which contains σ(z), we will need to evaluate π1 (σ(z))
at some point, which is undefined. Hence, e(σ) is undefined. Note that we do
not need all elements in σ(R) to reach the state where e(σ) becomes undefined.
Indeed, e is also undefined on the small environment σ ′ where σ ′ (R) = {{d}}
and σ ′ (z) = d.
We generalize this observation in the following general property, proven in
Appendix D. Here, we say that an environment σ is in the set Ek if every set
occurring in σ(x) has cardinality at most k for every x ∈ dom(σ).
Lemma 2 (Small model property for undefinedness). Let e be a PENRC[kind]
expression, let Γ be a type assignment on e, and let σ be an environment compatible with Γ such that e(σ) is undefined. There exists a natural number l which
can be computed from e alone, and an environment σ ′ ∈ El compatible with Γ ,
such that e(σ ′ ) is also undefined.

14

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

We obtain:
Corollary 5. Well-definedness problem for PENRC[kind] is decidable.
Indeed, up to isomorphism (and expressions cannot distinguish isomorphic inputs) there are only a finite number of different input environments in El compatible with Γ . So we can test them all to see if there is a counterexample to
well-definedness.
Also for semantic type-checking we have:
Lemma 3 (Small model property for semantic type-checking). Let e be
a PENRC[kind] expression, let Γ be a type assignment on e such that e is welldefined under Γ , and let τ be a type. Let σ be an environment compatible with
Γ such that e(σ) 6∈ τ . There exists a natural number l which can be computed
from e and τ alone, and an environment σ ′ ∈ El compatible with Γ , such that
also e(σ ′ ) 6∈ τ .
Corollary 6. Semantic type-checking for pure PENRC[kind] is decidable.
6.4

Equivalence and satisfiability

The above decidability results are quite sharp, because equivalence of PENRC
expressions is undecidable. This can be proven in a similar way as Theorem 1.
Of course, containment is then also undecidable. Levy and Suciu [12] have
shown that a “deep” form of containment (known as simulation) is decidable
for PENRC.
Another important problem is satisfiability. For example, the XQuery type
system generates a type error whenever it can deduce that an expression which
is not the empty set expression itself always returns the empty set. As noted
in Section 4, satisfiability is undecidable for PERX− [empty]. For pure PERX,
and PENRC[kind], however, satisfiability can be solved using the small model
property for semantic type-checking. Indeed, a PENRC[kind] expression e is
satisfiable under Γ if, and only if, coll(∅) is an output type for e under Γ . We
point out that, at least for PENRC without union and kind-tests, decidability
of satisfiability already follows from the work of Levy and Suciu cited above.

7

Lists and bags

In this paper we have focused our attention on a set-based abstraction of XQuery.
The actual data model of XQuery is list-based however, and hence it is natural
to ask how our results transfer to such a setting.
Let us denote by RXlist the list-based version of RX, which can be obtained
from RX as follows. The list-based RX data model is obtained by replacing
“set” in the definition of the RX data model by “list”. The list-based semantics
of an expression is obtained from the set-based semantics by replacing every set
operator by the corresponding list operator (i.e., empty set becomes empty list,

Well-Definedness and Semantic Type-Checking

15

union becomes concatenation, and so on). We can similarly define the bag-based
version of RX, which we will denote by RXbag .
We can still simulate the relational algebra in the list- and bag-based versions of PERX− [empty] and PERX− [type]. Hence, well-definedness and semantic
type-checking for these languages is undecidable. It is an open problem however
whether well-definedness and semantic type-checking in the list- and bag-based
versions of PERX− remains undecidable. Indeed, our undecidability proof depends heavily on the fact that set union is idempotent, which is not the case for
list concatenation and bag union.
We can also consider a list-based and bag-based version of PENRC[kind],
to which our decidability results transfer. Hence, well-definedness and semantic
type-checking are decidable for pure PERXlist and pure PERXbag .

References
1. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations Of Databases.
Addison-Wesley, 1995.
2. Noga Alon, Tova Milo, Frank Neven, Dan Suciu, and Victor Vianu. Typechecking
XML views of relational databases. ACM Transactions on Computational Logic,
4(3):315–354, 2003.
3. Noga Alon, Tova Milo, Frank Neven, Dan Suciu, and Victor Vianu. XML with
data values: typechecking revisited. Journal of Computer and System Sciences,
66(4):688–727, 2003.
4. Paul V. Biron and Ashok Malhotra. XML Schema Part 2: Datatypes. W3C Recommendation, May 2001.
5. Scott Boag, Don Chamberlin, Mary F. Fernández, Daniela Florescu, Jonathan
Robie, and Jérôme Siméon. XQuery 1.0: An XML Query Language. W3C Working
Draft, November 2003.
6. Peter Buneman, Shamim A. Naqvi, Val Tannen, and Limsoon Wong. Principles
of programming with complex objects and collection types. Theoretical Computer
Science, 149(1):3–48, 1995.
7. Don Chamberlin, Peter Fankhauser, Daniela Florescu, Massimo Marchiori, and
Jonathan Robie. XML Query Use Cases. W3C Working Draft, November 2003.
8. Ashok K. Chandra and Moshe Y. Vardi. The implication problem for functional and inclusion dependencies is undecidable. SIAM Journal on Computing,
14(3):671–677, 1985.
9. Denise Draper, Peter Fankhauser, Mary F. Fernández, Ashok Malhotra, Kristoffer
Rose, Michael Rys, Jérôme Siméon, and Philip Wadler. XQuery 1.0 and XPath
2.0 Formal Semantics. W3C Working Draft, February 2004.
10. Mary F. Fernández, Daniela Florescu, Alon Levy, and Dan Suciu. Declarative
specification of Web sites with Strudel. The VLDB Journal, 9:38–55, 2000.
11. Mary F. Fernández, Ashok Malhotra, Jonathan Marsh, Marton Nagy, and Norman
Walsh. XQuery 1.0 and XPath 2.0 Data Model. W3C Working Draft, November
2003.
12. Alon Y. Levy and Dan Suciu. Deciding containment for queries with complex objects (extended abstract). In Proceedings of the Sixteenth ACM SIGACT-SIGMODSIGART symposium on Principles of Database Systems, pages 20–31. ACM Press,
1997.

16

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

13. Wim Martens and Frank Neven. Typechecking top-down uniform unranked tree
transducers. In Database Theory - ICDT 2003, volume 2572 of Lecture Notes in
Computer Science, pages 64–78. Springer-Verlag, 2003.
14. Wim Martens and Frank Neven. Frontiers of tractability for typechecking simple
xml transformations. In Proceedings of the Twenty-third ACM SIGACT-SIGMODSIGART Symposium on Principles of Database Systems, pages 23–34. ACM Press,
2004.
15. Tova Milo, Dan Suciu, and Victor Vianu. Typechecking for XML transformers. In
Proceedings of the Nineteenth ACM SIGMOD-SIGACT-SIGART Symposium on
Principles of Database Systems, pages 11–22. ACM Press, 2000.
16. Frank Neven. Personal communication, May 2004.
17. Dan Suciu. Typechecking for semistructured data. In Database Programming
Languages, 8th International Workshop, DBPL 2001, Revised Papers, volume 2397
of Lecture Notes in Computer Science, pages 1–20. Springer-Verlag, 2001.
18. Henry S. Thompson, David Beech, Murray Maloney, and Noah Mendelsohn. XML
Schema Part 1: Structures. W3C Recommendation, May 2001.
19. Limsoon Wong. Querying nested collections. PhD thesis, University of Pennsylvania, 1994.

Well-Definedness and Semantic Type-Checking

A

17

Relational Algebra Simulation

Proposition 3. The relational algebra can be simulated in PERX− [empty] under any interpretation of the “oracle” functions concat and content. Concretely,
for every relational algebra expression φ over database schema S, there exists a
PERX− [empty]-expression e and a type assignment Γ , such that
– e is well-defined under Γ , and,
– e evaluated on an encoding of database D equals an encoding of φ(D).
Proof. In order to focus on the crux of the proof we will assume below that
atoms are expressions in PERX− [empty]. At the end of the proof we illustrate
how we can get rid of this assumption.
There exists a well-known encoding of tuples as unordered trees. For example,
the tuple (A1 : a1 , . . . , An : an ) can be encoded as the element node
hT : {hA1 : {a1 }i, . . . , hAn : {an }i}i.
Here we assume without loss of generality that attribute names are atoms. A
relation can then be encoded as the set of the encodings of its tuples.
We assume without loss of generality that relation names are variables. Let
S be a database schema, and let φ be a relational algebra expression over S. A
database D over S can be encoded as an environment σ such that σ(r) is an
encoding of D(r) for every relation name r.
We say that an expression e with FV (e) = FV (φ) simulates φ if e(σ) is an
encoding of φ(D) whenever σ is an encoding of D. We construct an expression
eφ which simulates φ by induction on φ as follows:4
– If φ = r then eφ = r.
– If φ = σA1 =A2 (ψ) then we define eφ to be
for t in eψ return
for x1 , x2 in children (t) return
if name(x1 ) = A1 and name(x2 ) = A2
and children (x1 ) = children (x2 ) then
t
else
()
– If φ = πA1 ,...,An (ψ) then we define eφ to be
for t in eψ return
elem {T }{
for x in children (t) return
4

Here, we allow to bind multiple variables in one for loop, and also allow boolean
combinations of conditions in an if test. Both features can clearly be simulated in
PERX− [empty].

18

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

if name(x) = A1 or . . . or name(x) = An then
x
else
()
}
– If φ = ψ1 × ψ2 then we define eφ to be (the schema’s of ψ1 and ψ2 are
disjoint):
for t1 in eψ1 , t2 in eψ2 return
elem {T }{children(t1 ), children(t2 )}
– If φ = ρA1 /A2 (ψ) then we define eφ to be
for t in eψ return
elem {T }{
for x in children (t) return
if name(x) = A1 then elem {A2 }{children(x)} else x
}
– If φ = ψ1 ∪ ψ2 then we define eφ as eφ1 , eφ2 .
– If φ = ψ1 − ψ2 then we define eφ as follows.
for t1 in eψ1 return
if f = ∅ then t1 else ()
Here, the subexpression f returns ∅ if t1 6∈ eψ2 , and {t1 } otherwise. Let the
schema of ψ1 and ψ2 be {A1 , . . . , An }, then f is constructed as follows:
for t2 in eψ2 return
for x1 ,. . .,xn in t1 return
for y1 ,. . .,yn in t2 return
if name(x1 ) = A1 and . . . and name(xn ) = An
and name(y1 ) = A1 and . . . and name(yn ) = An
and children (x1 ) = children (y1 )
and . . .
and children (xn ) = children (yn ) then
t
else
()
Note that eφ is well-defined under every input σ which is an encoding of some
D. Furthermore, on such σ, there is never need to evaluate concat or content
because:
– name is always evaluated on a singleton element node, and

Well-Definedness and Semantic Type-Checking

19

– every if-test is between singleton data nodes (and hence, the application of
data on the values which are to be compared can be calculated without using
content).
Let Γ be the type assignment for which for every r ∈ FV (φ)
Γ (r) = coll(elem(coll(elem(single(data))))).
Note that σ is not necessarily an encoding of a database D when σ is compatible with Γ . Hence, eφ is not necessarily well-defined under Γ . However, we
can transform every σ(r) into an input which is an encoding of D(r) for some
database D as follows. Let the schema S(r) = {A1 , . . . , An }.
for t in r return
for x1 , . . . , xn in t return
if name(x) = A1 and . . . and name(xn ) = An then
elem {T }{x1, . . . , xn }
else
()
Note that this expression does not change σ(r) if it is already a valid encoding.
Let e be the expression obtained by replacing every r in eφ by the expression
above. It is easy to verify that now e is well-defined under Γ .
Note We have assumed in the construction above that constant atoms (such
as A1 , . . . , An ) are expressions. This makes the construction easier, but is not
really necessary. We first note that we could have chosen any atom to represent
an attribute Ai , as long as it differs from the atoms representing other attributes.
Hence, we can create for every attribute name Ai thus used a variable xAi with
type single(atom). An environment σ is now an encoding of a database D if
(1) σ(r) is an encoding of D(r) (as before), and (2) σ(xAi ) 6= σ(xAj ) when i 6= j.
Let e′ be the expression obtained from e by replacing Ai by xAi . Using if-tests
we can then evaluate e′ if condition (2) holds, and evaluate () otherwise.
⊓
⊔

B

Well-definedness in PERX−

In this section we give the full proof that well-definedness for PERX− is undecidable.
Theorem 2. Well-definedness for PERX− is undecidable.
Proof. In order to focus on the crux of the proof we will assume below that
atoms are expressions in PERX− [empty]. At the end of the proof we illustrate
how we can get rid of this assumption.
We give a reduction from the implication problem for functional and inclusion
dependencies, which is known to be undecidable [1, 8]. We assume without loss
of generality that the database schema consists of a single relation symbol with

20

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

schema {A1 , . . . , Ak }. A functional dependency φ is a rule X → Y where X and
Y are subsets of {A1 , . . . , Ak }. We say that relation R satisfies φ, denoted by
R |= φ if for all tuples t1 , t2 ∈ R if πX (t1 ) = πX (t2 ) then also πY (t1 ) = πY (t2 ).
An inclusion dependency ψ is a rule of the form [B1 , . . . , Bi ] → [C1 , . . . , Ci ]
where {B1 , . . . , Bi } and {C1 , . . . , Ci } are subsets of {A1 , . . . , Ak }. We say that
relation R satisfies ψ, denoted by R |= ψ if πB1 ,...,Bk (R) ⊆ πC1 ,...,Ck (R).
Let Σ be a set of functional and inclusion dependencies. Let φ1 , . . . , φn be the
functional dependencies in Σ, and let ψ1 , . . . , ψm be the inclusion dependencies
in Σ. Let ρ be an additional target functional dependency. The implication
problem consists of checking for every relation R over {A1 , . . . , Ak } that if R
satisfies every dependency in Σ, then R also satisfies ρ.
We assume without loss of generality that A1 , . . . , Ak are atoms. We will
encode a k-tuple (A1 : a1 , . . . , Ak : ak ) by the element node
hA1 : {hA1 : {a1 }i, . . . , hAk : {ak }i}i.
A relation R is then encoded as the set of the encodings of tuples in R. Let r be
a variable, and let Γ be the type assignment for which
Γ (r) = coll(elem(coll(elem(single(data))))).
Note that σ(r) is not necessarily an encoding of some relation R when σ is
compatible with Γ . For example, suppose that k ≥ 2, and consider
σ(r) = {hA1 : {hA1 : {hai}i}i}.
Then σ ∈ Γ , but there is clearly no instance of R for which σ(r) is an encoding.
However, we can transform every input into an input which is an encoding
of some relation:5
for t1 in r return
for x1 , . . . , xk in t1 return
if name(x1 ) = A1 and . . . and name(xk ) = Ak then
elem {A1 }{x1 , . . . , xk }
else ()
The output of this expression is always a set of element nodes which are encodings of k-ary tuples. In the remainder of this proof we will therefore assume
w.l.o.g. that r contains an actual encoding of some relation r: we can always
replace r by the expression above.
For every functional dependency φ = {B1 , . . . , Bi } → {C1 , . . . , Cj }, we create
the following expression eφ :
for t1 ,t2 in r return
for x1 , . . . , xi , y1 , . . . , yj in t1 return
5

Here, we allow to bind multiple variable in one for loop, and also allow boolean
combinations of conditions in an if test. Both features can clearly be simulated in
PERX− .

Well-Definedness and Semantic Type-Checking

21

for u1 , . . . , ui , v1 , . . . , vj in t2 return
if name(x1 ) = B1 and . . . and name(xi ) = Bi
and name(y1 ) = C1 and . . . and name(yj ) = Cj
and name(u1 ) = B1 and . . . and name(ui ) = Bi
and name(v1 ) = C1 and . . . and name(vj ) = Cj then
if children (x1 ) = children (u1 )
and . . .
and children (xi ) = children (ui )
and (children (y1 ) 6= children (v1 )
or . . .
or children(yj ) 6= children(vj )
) then elem {A1 }{()} else ()
else ()
Note that on input σ for which σ(r) is an encoding of relation R this expression
returns ∅ if R |= φ, and hA1 : ∅i otherwise.
For every inclusion dependency ψ = R : [B1 , . . . , Bi ] ⊆ S : [C1 , . . . , Ci ] we
create the following expression eψ :
for t1 in r return elem {A1 }{
for t2 in r return
for x1 , . . . , xi in t1 return
for y1 , . . . , yi in t2 return
if name(x1 ) = B1 and . . . and name(xi ) = Bi
and name(y1 ) = C1 and . . . and name(yi ) = Ci
and children (x1 ) = children(y1 )
and . . .
and children (xi ) = children (yi )
then elem {A1 }{()} else ()
}, elem {A1 }{elem {A1 }{()}}
Note that on input σ for which σ(r) is an encoding of relation R, this expression
returns {hA1 : {hA1 : ∅ii}} if R |= φ, and {hA1 : {hA1 : ∅i}i, hA1 : ∅i} otherwise.
Let D0 , . . . , Dn , E1 , . . . , Em be different elements of A. We then create the
expression e1 as follows:
elem {A1 }{
elem {D0 }{eρ },elem {D1 }{eφ1 },...,elem {Dn }{eφn },
elem {E1 }{eψ1 }, ..., elem {Em }{eψm }
}
Let f1 , . . . , fn , h be expressions of the form () or elem {A1 }{()}}, and let
g1 , . . . , gm be expressions of the form (elem {A1 }{()}, elem {A1 }{elem {A1 }{()}}),
or elem {A1 }{elem {A1 }{()}}. We call an expression
elem {A1 }{
elem {D0 }{h},elem {D1 }{f1 },...,elem {Dn }{fn },
elem {E1 }{g1 }, ..., elem {Em }{gm}
}

22

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

admissible when, if f1 = · · · = fn = () and g1 . . . gm = elem {A1 }{elem {A1 }{()}},
then h = (). Clearly the number of admissible expressions is finite. Let {i1 , . . . , ik }
be the set of all admissible expressions. Then we define e2 as the expression
i1 , . . . , in .
Note that e1 and e2 are well-defined under Γ . Furthermore, the following
node content type is an output type for e1 and e2 under Γ :
γ := coll(elem(coll(elem(coll(elem(coll(elem(coll(data))))))))).
Also, Σ |= ρ if, and only if, e1 (σ) ⊆ e2 (σ) for every σ ∈ Γ . Hence, Σ |= ρ if, and
only if, (e1 , e2 )(σ) = e2 (σ) for every σ ∈ Γ . Consequently,
e := name(elem {A1 }{e1 ∪ e2 }, elem {A1 }{e2 })
is defined if and only if Σ |= ρ. Furthermore, elem {A1 }{e1 ∪ e2 }, elem {A1 }{e2 })
has output type single(elem(γ)) if, and only if Σ |= ρ.
Note We have assumed in the construction above that constant atoms (such
as A1 , . . . , An ) are expressions. This makes the construction easier, but is not
really necessary. We first note that we could have chosen any atom to represent
an attribute Ai , as long as it differs from the atoms representing other attributes.
Hence, we can create for every attribute name Ai thus used a variable xAi with
type single(atom). An environment σ is now an encoding of a relation R if (1)
σ(r) is an encoding of R (as before), and (2) σ(xA ) 6= σ(xB ) when A 6= B. Let
e′ be the expression obtained from e by replacing every A by xA . Using if-tests
we can then evaluate e′ if condition (2) holds, and evaluate () otherwise.
⊓
⊔

C

Simulating pure PERX in PENRC[kind]

In this section we give the full proof of the simulation of PERX in PENRC[kind].
Lemma 4. The pure PERX can effectively be simulated in PENRC[kind].
Proof.
enc(a) = a
enc(ha : N i) = (a, enc(N ))

enc(hai) = ((a, a), ∅)
enc(v) = {enc(i) | i ∈ v}

We will now verify that enc has the required properties. Let τ be a pure
RX-type. We define the pure NRC-type τ ′ by induction on τ as follows.
atom′ = atom
data′ = (atom × atom) × coll(∅)
elem(ν1 ∪ · · · ∪ νk )′ = atom × coll(ν1′ ∪ · · · ∪ νk′ )
coll(ι)′ = coll(ι′ )
(τ1 ∪ τ2 )′ = τ1′ ∪ τ2′

Well-Definedness and Semantic Type-Checking

23

Obviously, v ∈ τ if, and only if enc(v) ∈ τ ′ . If κ is a pure PERX-kind, then we
define the PENRC-kind κ′ by induction on κ as follows:
atom′ = atom
data′ = (atom × atom) × coll
elem′ = atom × coll
(κ1 ∪ κ2 )′ = κ′1 ∪ κ′2
Obviously, v ∈ κ if, and only if, enc(v) ∈ κ′ .
Let e be a pure PERX-expression. We will define the pure PENRC-expression
e′ by induction on e as follows. We first introduce some syntactic sugar: we write
e1 ∈ κ → e2 for e1 ∈ κ ? e2 : π1 (∅). Intuitively, this expression will be used
to verify that the input to e′ is an encoding of a legal input to e. Otherwise, we
become undefined.
x′ := x
hei′ := e′ ∈ atom → ((e′ , e′ ), ∅)
he1 : e2 i′ := e′1 ∈ atom →
(e′1 , {x ∈ atom ? ((x, x), ∅) : x | x ∈ e′2 })
[
data(e)′ := {x ∈ (atom × atom) × coll ? {π1 (π1 (x))}
: x ∈ atom ? {x} : ∅ | x ∈ e′ }

name(e)′ := π1 (e′ ) ∈ atom → π1 (e′ )
[
children(e)′ := {π2 (x) | x ∈ e′ }

()′ := ∅
(e)′ := e′ ∈ atom ∪((atom × atom) × coll) ∪ (atom × coll) → {e′ }

(e1 , e2 )′ := e′1 ∪ e′2
[
(for x : κ in e1 return e2 )′ := {x ∈ κ′ ? e′2 : ∅ | x ∈ e′1 }

(if e1 eq e2 then e3 else e4 )′ := e′1 = e′2 ? e′3 : e′4

A straightforward induction on e now shows that
1. e(σ) is defined if, and only if e′ (enc(σ)) is defined, and
2. if e(σ) is defined then enc(e(σ)) = e′ (enc(σ)).

D

⊓
⊔

Well-definedness for PENRC[kind]

In this section we give the proof of the small model properties mentioned in
Section 6.3. Whenever we write “expression” we mean PENRC[kind]-expression,
and whenever we write type we mean PENRC-type.

24

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

Let k be a natural number. We write Vk for the set of all values v for which
the cardinality of a set occurring in v is at most k:
Vk = A ∪ (Vk × Vk ) ∪ {v ⊆ Vk | |v| ≤ k}.
We write Ek for the set of all environments σ for which the cardinality of a set
occurring in σ is at most k:
Ek = {σ | σ environment on some X and σ(x) ∈ Vk for all x ∈ X}.
The sub-value relation ⊑ on values is inductively defined by the following
inference rules:
a⊑a

v ⊑ v′
w ⊑ w′
(v, w) ⊑(v ′ , w′ )

for all vi there exists wj such that vi ⊑ wj
{v1 , . . . , vn } ⊑{w1 , . . . , wm }

This relation can be extended component-wise to environments: let σ and σ ′ be
two environments on the same set of variables X, then σ ⊑ σ ′ if σ(x) ⊑ σ ′ (x) for
all x ∈ X.
If u, v, w are values, and u ⊑ w and v ⊑ w, then we define u ⊔ v as follows:
a⊔a = a

(u1 , u2 ) ⊔(w1 , w2 ) = (u1 ⊔ w1 , u2 ⊔ w2 )

v⊔w = v ∪ w

Lemma 5. If u ⊑ w and v ⊑ w, then u ⊑ u ⊔ v, v ⊑ u ⊔ v, and u ⊔ v ⊑ w. Moreover, if u ∈ Vk and v ∈ Vl , then u ⊔ v ∈ Vk+l .
Proof. By a straightforward induction on w.
We first give some characteristics of ⊑ with regard to kinds and types.
Lemma 6. If v ⊑ w then v ∈ κ if, and only if, w ∈ κ.
Proof. By a trivial induction on κ.
Lemma 7. Let τ be a type. If v ⊑ w and w ∈ τ , then v ∈ τ .
Proof. By a trivial induction on τ .
The PENRC has the following monotonicity properties. The proof is by a
straightforward induction.
Lemma 8 (Monotonicity). Let e be an expression, and let σ and σ ′ be environments on FV (e) such that σ ⊑ σ ′ . If e(σ) and e(σ ′ ) are defined, then e(σ) ⊑ e(σ ′ ).
If e(σ) is undefined, then so is e(σ ′ ).
In what follows we will frequently take the minimum min(v) of a value v,
which is obtained by replacing every set occurring in v by the empty set. For
example, min(({a, b}, (a, {{c, d}}))) = (∅, (a, ∅)). Obviously, min(v) ∈ V0 and
min(v) ⊑ v.

Well-Definedness and Semantic Type-Checking

25

Before we are ready to state our small model properties we need one final definition. Let e be an expression, and let k be a natural number. The k-complexity
c(e, k) of e is inductively defined as follows:
c(x, k) = k
c((e1 , e2 ), k) = c(e1 ∪ e2 , k) = c(e1 , k) + c(e2 , k)
[
c(π1 (e′ ), k) = c(π2 (e′ ), k) = c( e′ ) = c(e′ , k)

c({e′ }, k) = k × c(e′ , k)

c(∅, k) = 0
c({e2 | x ∈ e1 }, k) = c(e1 , max(k, c(e2 , k))) + k × c(e2 , k)
c(e1 = e2 ? e3 : e4 , k) = max(c(e3 , k), c(e4 , k))
c(e1 ∈ κ ? e2 : e3 , k) = max(c(e2 , k), c(e3 , k))
Lemma 9 (Small model). Let k be a natural number, let e be an expression,
and let σ be an environment on FV (e) such that e(σ) is defined. Let u ∈ Vk .
If u ⊑ e(σ), then there exists an environment σ ′ ∈ Ec(e,k) with σ ′ ⊑ σ such that
u ⊑ e(σ ′ ).
Proof. Note that since e(σ) is defined, e(δ) is also defined for every δ ⊑ σ by
monotonicity. Moreover, if σ1 ⊑ σ and σ2 ⊑ σ, then σ1 ⊑ σ1 ⊔ σ2 , σ2 ⊑ σ1 ⊔ σ2 ,
and σ1 ⊔ σ2 ⊑ σ by Lemma 5. We will use these facts silently throughout this
proof.
In order to write the proof in a succinct manner, let us define the set
P (u, e, σ, k) by
P (u, e, σ, k) = {σ ′ | σ ′ ∈ Ec(e,k) , σ ′ ⊑ σ, and u ⊑ e(σ ′ )}.
We will prove by induction on e that P (u, e, σ, k) is non-empty.
– If e = x, then we define σ ′ by
′

σ (y) =

(

u
min(σ(y))

if y = x
otherwise

– If e = ∅, then we take σ ′ = min(σ).
– If e = (e1 , e2 ), then e(σ) is a pair. Hence, u = (u1 , u2 ) for some u1 , u2 ∈
Vk . By the induction hypothesis there exist σ1 ∈ P (u1 , e1 , σ, k) and σ2 ∈
P (u2 , e2 , σ, k). Then σ1 ⊔ σ2 ∈ Ec(e1 ,k)+c(e2 ,k) = Ec(e,k) . Then, by monotonicity:
(u1 , u2 ) ⊑(e1 (σ1 ), e2 (σ2 )) ⊑(e1 (σ1 ⊔ σ2 ), e2 (σ1 ⊔ σ2 )) = e(σ1 ⊔ σ2 )
Hence, σ1 ⊔ σ2 ∈ P (u, e, σ, k).

26

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

– If e = e1 ∪ e2 , then e(σ) is a set. Since u ⊑ e(σ) there exists wv ∈ e(σ) with
v ⊑ wv for every v ∈ u. Define
u1 = {v ∈ u | wv ∈ e1 (σ)}
u2 = {v ∈ u | wv ∈ e2 (σ)}
Then u = u1 ∪ u2 , u1 ⊑ e1 (σ), and u2 ⊑ e2 (σ). Moreover, u1 , u2 ∈ Vk . The
result then follows from the induction hypothesis by a reasoning similar to
the previous case.
– If e = π1 (e′ ), then e′ (σ) is a pair (v, w). Let u′ = (u, min(w)). Then u′ ⊑(v, w)
since u ⊑ v and min(w) ⊑ w. Moreover, u′ ∈ Vk since min(w) ∈ V0 . Hence
there exists σ ′ ∈ P (u′ , e′ , σ, k) by the induction hypothesis. Hence, u =
π1 (u′ ) ⊑ π1 (e′ (σ ′ )) = e(σ ′ ). Since Ec(e′ ,k) = Ec(e,k) , σ ′ ∈ P (u, e, σ, k). The
case where e = π2 (e′ ) is similar.
– If e = {e′ } then we discern two cases. If u = ∅, then u ⊑ e(σ ′ ) for any
σ ′ ⊑ σ by monotonicity. Hence, it suffices to take σ ′ = min(σ), which is in
E0 . Otherwise, u contains at least one and at most k elements. Let v ∈ u.
Then v ∈ Vk , and v ⊑ e′ (σ) since u ⊑Fe(σ). By the induction hypothesis there
exists σv ∈ P (v, e′ , σ, k). Let σ ′ = v∈u σv . Then σv ⊑ σ ′ for every v ∈ u,
and σ ′ ⊑ σ. By monotonicity we then have
v ⊑ e′ (σv ) ⊑ e′ (σ ′ ).
And hence u ⊑ e′ (σ ′ ). Moreover, σ ′ ∈ Ek×c(e′ ,k) = c(e, k) by Lemma 5. Hence,
σ′ ∈ P S
(u, e, σ, k).
– If e = e′ then e′ (σ) is a set of sets. For every v ∈ u there exists wv ∈ e(σ)
such that v ⊑ wv since u ⊑ e(σ).
Let e′ (σ) = {z1 , . . . , zn }. Define
[
zj }.
ui = {v ∈ u | wv ∈ zi \
j<i

Note that the cardinality of each of the ui ’s is at most k, and that at most
k of the ui ’s are non-empty. Furthermore, ui ⊑ zi . Let u′ be the set of all
non-empty ui ’s. Then u′ ⊑ e′ (σ) and u′ ∈ Vk . The result then follows from
the induction hypothesis.
– If e = e1 = e2 ? e3 : e4 , then e1 (σ), e2 (σ) ∈ A. Suppose e1 (σ) = e2 (σ), then
u ⊑ e3 (σ). By the induction hypothesis there exists σ ′ ∈ P (u, e3 , σ, k). Then
e1 (σ ′ ) = e1 (σ) = e2 (σ) = e2 (σ ′ ) by monotonicity and hence e(σ ′ ) = e3 (σ ′ ).
We then have by the induction hypothesis that u ⊑ e3 (σ ′ ) = e(σ ′ ). Since
σ ′ ∈ Ec(e3 ,k) ⊆ Ec(e,k) , σ ′ ∈ P (u, e, σ, k). The case where e1 (σ) 6= e2 (σ) is
similar.
– If e = e1 ∈ κ ? e2 : e3 , we discern two cases. If e1 (σ) ∈ κ then u ⊑ e2 (σ).
By the induction hypothesis there exist σ ′ ∈ P (u, e2 , σ, k). By monotonicity,
e1 (σ ′ ) ⊑ e1 (σ). Hence, e1 (σ ′ ) ∈ κ by Lemma 6. Then e(σ ′ ) = e2 (σ ′ ), and
hence u ⊑ e2 (σ ′ ) = e(σ ′ ). Then σ ′ ∈ P (u, e, σ, k) since σ ′ ∈ Ec(e2 ,k) ⊆ Ec(e,k) .
The case where e1 (σ) 6∈ κ is similar.

Well-Definedness and Semantic Type-Checking

27

– If e = {e2 | x ∈ e1 }, then e(σ) is a set. Let v ∈ u. Since u ⊑ e(σ) there exists
wv ∈ e(σ) such that v ⊑ wv . Since e(σ) is obtained by a comprehension over
e1 (σ), there also must exists some zv ∈ e1 (σ) such that v ⊑ wv = e2 (x :
zv , σ). Hence, there exists x : zv′ , σv′ ∈ P (v, e2 , (x : zv , σ), k) by the induction
hypothesis. Let u′ = {zv′ | v ∈ u}. Then u′ contains at most k elements of
Vc(e2 ,k) . Hence, u′ ∈ Vmax(k,c(e2 ,k)) . Moreover, x : zv′ , σ ′ ⊑ x : zv , σ by the
induction hypothesis, so zv′ ⊑ zv , and hence u′ ⊑ e1 (σ).
By applying theFinduction hypothesis again, there exists σ1 ∈ P (u′ , e1 , σ, k).
Let σ ′ = σ1 ⊔ v∈u σv′ . Note that σ1 ⊑ σ ′ , and σv′ ⊑ σ ′ for every v ∈ u.
Furthermore, σ ′ ⊑ σ and the maximum cardinality of a set in σ ′ is bounded
by (Lemma 5):
c(e1 , max(k, c(e2 , k))) + k × c(e2 , k) = c(e, k)
Now u′ ⊑ e1 (σ1 ) ⊑ e1 (σ ′ ) by monotonicity. Hence, for every zv′ there exists
some zv′′ ∈ e1 (σ ′ ) with zv′ ⊑ zv′′ . Then x : zv′ , σv′ ⊑ x : zv′′ , σ ′ , and hence
v ⊑ e2 (x : zv′ , σv′ ) ⊑ e2 (x : zv′′ , σ ′ ) by monotonicity. Since this holds for every v ∈ u, we have u ⊑ e(σ ′ ).
⊓
⊔
Lemma 10. Let e be an expression and σ an environment on FV (e). If e(σ) is
undefined, then there exists σ ′ ∈ Ec(e,1) with σ ′ ⊑ σ such that e(σ ′ ) is undefined.
Proof. The proof is by induction on e. We note again that if e′ (σ) is defined,
then e′ (δ) is also defined for every δ ⊑ σ by monotonicity.
– If e = x, or e = ∅, then there is nothing to prove, since e(σ) is always defined.
– If e = (e1 , e2 ), then either e1 (σ) or e2 (σ) is undefined. The result then follows
by the induction hypothesis. The case where e = {e′ } is similar.
– If e = π1 (e′ ), then either e′ (σ) is undefined, in which case the result follows
from the induction hypothesis, or e′ (σ) is not a pair. Let σ ′ = min(σ). By
monotonicity e′ (σ ′ ) cannot be a pair, and hence e(σ ′ ) is also undefined.
Moreover, σ ′ ∈ E0 ⊆ Ec(e,1) .
– If e = e1 ∪ e2 , then either e1 (σ) is undefined, e2 (σ) is undefined, e1 (σ) is not
a set, or e2 (σ) is not a set. In the first two cases the result follows from the
induction hypothesis. In the third cases, let σ ′ = min(σ). By monotonicity
e1 (σ) cannot be a set, and hence e(σ ′ ) is undefined. Moreover, σ ′ ∈ E0 ⊆
Ec(e,1) . The last case is similar.
S ′
– If e =
e , then either e′ (σ) is undefined, or e′ (σ) is not a set of sets.
In the first case the result follows from the induction hypothesis. In the
latter case we have two possibilities. If e′ (σ) is not a set, then let σ ′ =
min(σ). By monotonicity, e′ (σ ′ ) cannot be a set, and hence e(σ) is undefined.
Moreover, σ ′ ∈ E0 ⊆ Ec(e,1) . If e′ (σ) is a set, but not a set of sets, then
there exist some u ∈ e′ (σ) that is not a set. Then {min(u)} ∈ V1 , and
{min(u)} ⊑ e′ (σ). By Lemma 9 there exists σ ′′ ∈ Ec(e′ ,1) = Ec(e,1) with σ ′′ ⊑ σ
such that {min(u)} ⊑ e′ (σ ′′ ). Hence, e′ (σ) is not a set of sets, and e(σ ′′ ) is
also undefined.

28

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

– If e = e1 = e2 ? e3 : e4 , then we have three possibilities. If e1 (σ) or e2 (σ)
is undefined, then the result follows from the induction hypothesis. If e1 (σ)
and e2 (σ) are defined and e1 (σ) = e2 (σ), then e3 (σ) must be undefined. By
the induction hypothesis, there exists σ ′ ∈ Ec(e3 ,1) ⊆ Ec(e,1) with σ ′ ⊑ σ such
that e3 (σ ′ ) is also undefined. By monotonicity e1 (σ ′ ) = e2 (σ ′ ), and hence
e(σ ′ ) is undefined. If e1 (σ) 6= e2 (σ) the reasoning is similar.
– If e = e1 ∈ κ ? e2 : e3 , then we have three possibilities. If e1 (σ) is undefined,
then the result follows from the induction hypothesis. If e1 (σ) is defined and
e1 (σ) ∈ κ, then e2 (σ) must be undefined. By the induction hypothesis we
have σ ′ ∈ Ec(e2 ,1) ⊆ Ec(e,1) with σ ′ ⊑ σ such that e2 (σ ′ ) is still undefined.
By monotonicity, e1 (σ ′ ) ⊑ e1 (σ), and hence e1 (σ ′ ) ∈ κ by Lemma 6. Hence,
e(σ ′ ) = e2 (σ ′ ) which is undefined. If e1 (σ) is defined, but e1 (σ) 6∈ κ the
reasoning is similar.
– If e = {e2 | x ∈ e1 }, then we have three possibilities.
1. If e1 (σ) is undefined, then the result follows from the induction hypothesis.
2. If e1 (σ) is defined, but is not a set, then let σ ′ = min(σ). By monotonicity,
e1 (σ ′ ) cannot be a set, and hence e(σ ′ ) is undefined. Moreover, σ ′ ∈
Ec(e1 ,1) ⊆ Ec(e,1) .
3. Otherwise, e1 (σ) is defined and a set, but there is some v ∈ e1 (σ)
such that e2 (x : v, σ) is undefined. By the induction hypothesis, there
exists x : u, σ2 ∈ Ec(e2 ,1) with x : u, σ2 ⊑ x : v, σ such that e2 (x :
u, σ2 ) is undefined. Then {u} ∈ Vmax(1,c(e2 ,1)) , and {u} ⊑ e1 (σ). By
Lemma 9 there exists σ1 ∈ Ec(e1,max(1,c(e2 ,1))) with σ1 ⊑ σ such that
{u} ⊑ e1 (σ1 ). Let σ ′ = σ1 ⊔ σ2 . Note that σ1 ⊑ σ ′ and σ2 ⊑ σ ′ . By monotonicity {u} ⊑ e1 (σ ′ ). Hence, there exists some u′ ∈ e1 (σ ′ ) such that
u ⊑ u. Then x : u, σ2 ⊑ x : u′ , σ ′ , and e2 (x : u′ , σ ′ ) is undefined by
monotonicity of undefinedness. Hence, e(σ ′ ) is undefined. Moreover, σ ′ ∈
Ec(e1 ,max(1,c(e2 ,1))+c(e2 ,1)) = Ec(e,1) .
⊓
⊔
Corollary 7 (Small model for undefinedness). Let e be an expression, let
Γ be a type assignment on e, and let σ be an environment compatible with Γ such
that e(σ) is undefined. There exists a natural number l which depends only on e,
and an environment σ ′ ∈ El compatible with Γ such that e(σ ′ ) is also undefined.
Proof. By Lemma 10, there exists σ ′ ∈ Ec(e,k) such that σ ′ ⊑ σ and e(σ ′ ) is
undefined. Moreover, σ ′ ∈ Γ since σ ∈ Γ by Lemma 7.
⊓
⊔
Functions mapping atoms to atoms can naturally be lifted to functions defined on values by extending them element- or components-wise. Indeed, let
f be a function mapping atoms to atoms, then f can be lifted to values by
taking f ((v, w)) = (f (v), f (w)), and f ({v, . . . , w}) = {f (v), . . . , f (w)}. Also,
functions defined on values can be lifted to functions on environments by taking
f (σ)(x) = f (σ(x)).
It is easy to show by induction that the PENRC is generic.
Lemma 11 (Genericity). Let e be an expression, let σ be a environment on
FV (e), and let ρ be a permutation of A. If e(σ) is defined, then e(ρ(σ)) =
ρ(e(σ)). If e(σ) is undefined, then so is e(ρ(σ)).

Well-Definedness and Semantic Type-Checking

29

Theorem 3. Let e be an expression and let Γ be a type assignment on FV (e).
It is decidable to check whether e is well-defined under Γ .
Proof. Suppose that e is not well-defined under Γ . Then there exists some σ
compatible with Γ such that e(σ) is undefined. By Lemma 10 there exists some
σ ′ ∈ Ec(e,1) compatible with Γ with σ ′ ⊑ σ such that e(σ ′ ) is undefined.
Let k be a natural number, and let τ be a type. Let us denote the maximum
number of atoms a value in τ ∩ Vk can mention by rank (τ ∩ Vk ). Then
rank (A ∩ Vk ) = 1
rank ((τ1 × τ2 ) ∩ Vk ) = rank (τ1 ∩ Vk ) + rank (τ2 ∩ Vk )
rank ((τ1 ∪ τ2 ) ∩ Vk ) = max(rank (τ1 ∩ Vk ), rank (τ2 ∩ Vk ))
rank (coll(τ ′ ) ∩ Vk ) = k rank (τ ′ ∩ Vk )
Consequently, the maximum number of atoms an environment in Ec(e,1) compatible with Γ can mention is bounded by
l=

X

rank (Γ (x) ∩ Vc(e,1) ).

x∈FV (e)

Note that l depends only on e and Γ . Let A = {a1 , . . . , al } ⊆ A. Let us denote
the atoms occurring in an environment δ by A(δ). Since the number of different
atoms occurring in σ ′ is at most l, there exists a permutation ρ of A such that
A(ρ(σ ′ )) = ρ(A(σ ′ )) ⊆ A. By genericity, e(ρ(σ ′ )) is also undefined.
Hence, in order to check if e is well-defined under Γ it suffices to enumerate
all environments γ compatible with Γ that mention only atoms in A, and check
whether e(γ) is defined. There are only a finite number of such γ, from which
the result follows.
⊓
⊔
Lemma 12. If v is a value and v 6∈ τ , then there exists a natural number k and
u ∈ Vk such that u ⊑ v and u 6∈ τ .
Proof. Let us define the complexity c(τ ′ ) of a type τ ′ as follows.
c(A) = 0
c(τ1 × τ2 ) = max(c(τ1 ), c(τ2 ))
c(τ1 ∪ τ2 ) = c(τ1 ) + c(τ2 )
c(coll(τ ′ )) = max(1, c(τ ′ ))
Let v be a value with v 6∈ τ . We show that there exists a value u ∈ Vc(τ ) with
u ⊑ v such that u 6∈ τ by induction on τ .
– If τ = A, then take u = v.
– If τ = (τ1 , τ2 ), then v = (v1 , v2 ) and either v1 6∈ τ1 , or v2 6∈ τ2 . We can apply
the induction hypothesis in both cases.

30

Jan Van den Bussche, Dirk Van Gucht, and Stijn Vansummeren

– If τ = τ1 ∪ τ2 , then v 6∈ τ1 and v 6∈ τ2 . By the induction hypothesis there
exist u1 ∈ c(τ1 ) and u2 ∈ c(τ2 ) with u1 ⊑ v and u2 ⊑ v such that u1 6∈ τ1 and
u2 6∈ τ2 . Take u = u1 ⊔ u2 , and suppose u ∈ τ . Then either u ∈ τ1 , or u ∈ τ2 .
If u ∈ τ1 , then also u1 ⊑ u would have to be in τ1 by Lemma 7, which is a
contradiction. If u ∈ τ2 , then also u2 ⊑ u would have to be in τ2 , which is
also a contradiction. Hence, u 6∈ τ . Moreover, u ∈ Vc(τ1 )+c(τ2 ) = Vc(τ ) .
– Finally, if τ = coll τ ′ ), then there exists some v ′ ∈ v such that v ′ 6∈ τ ′ . By the
induction hypothesis there exists u′ ∈ Vc(τ ′ ) such that u′ ⊑ v ′ and u′ 6∈ τ ′ .
Then {u′ } ⊑ v and {u′ } 6∈ τ .
⊓
⊔
Corollary 8 (Small model for semantic type-checking). Let e be an expression, let Γ be a type assignment on e such that e is well-defined under Γ ,
and let τ be a type. Let σ be an environment on e such that e(σ) 6∈ τ . There
exists a natural number l which depends only on e and τ , and an environment
σ ′ ∈ El compatible with Γ such that also e(σ ′ ) 6∈ τ .
Proof. Since e(σ) 6∈ τ , there exists a natural number k and a value u ∈ Vk with
u ⊑ e(σ) such that u 6∈ τ by Lemma 12. By Lemma 9, there exists σ ′ ∈ Ec(e,k)
such that σ ′ ⊑ σ and u ⊑ e(σ ′ ). Since u 6∈ τ , e(σ ′ ) is also not in τ by Lemma 7.
Since σ ∈ Γ , also σ ′ ∈ Γ by Lemma 7.
⊓
⊔

