Regular Expression Subtyping for XML Query and
Update Languages
James Cheney

arXiv:0801.0714v1 [] 4 Jan 2008

University of Edinburgh

Abstract. XML database query languages such as XQuery employ regular expression types with structural subtyping. Subtyping systems typically have two
presentations, which should be equivalent: a declarative version in which the
subsumption rule may be used anywhere, and an algorithmic version in which
the use of subsumption is limited in order to make typechecking syntax-directed
and decidable. However, the XQuery standard type system circumvents this issue
by using imprecise typing rules for iteration constructs and defining only algorithmic typechecking, and another extant proposal provides more precise types
for iteration constructs but ignores subtyping. In this paper, we consider a core
XQuery-like language with a subsumption rule and prove the completeness of
algorithmic typechecking; this is straightforward for XQuery proper but requires
some care in the presence of more precise iteration typing disciplines. We extend
this result to an XML update language we have introduced in earlier work.

1 Introduction
The Extensible Markup Language (XML) is a World Wide Web Consortium (W3C)
standard for tree-structured data. Regular expression types for XML [13] have been
studied extensively in XML processing languages such as XDuce [12] and CDuce [1],
as well as projects to extend general-purpose programming languages with XML features such as Xtatic [9] and OCamlDuce [8].
Several other W3C standards, such as XQuery, address the use of XML as a general
format for representing data in databases. Static typechecking is important in XML
database applications because type information is useful for optimizing queries and
avoiding expensive run-time checks and revalidation. The XQuery standard [5] provides
for structural subtyping based on regular expression types.
However, XQuery’s type system is imprecise in some situations involving iteration (for-expressions). In particular, if the variable $x has type1 a[b[]∗ , c[]? ], then the
XQuery expression
for $y in $x/* return $y
has type (b[]|c[])∗ in XQuery, but in fact the result will always match the regular expression type b[]∗ , c[]? . The reason for this inaccuracy is that XQuery’s type system
typechecks a for loop by converting the type of the body of the expression (here, $x/a
1

We use the notation for regular expression types from Hosoya, Vouillon and Pierce [13] in
preference to the more verbose XQuery or XML Schema syntaxes.

with type b[]∗ , c[]? ) to the “factored” form (α1 | . . . |αn )q , where q is a quantifier such
as ?, +, or ∗ and each αi is an atomic type (i.e. a data type such as string or single
element type a[τ ]).
More precise type systems have been contemplated for XQuery-like languages,
including a precursor to XQuery designed by Fernandez, Siméon, and Wadler [7].
More recently, Colazzo et al. [4] have introduced a core XQuery language called µXQ,
equipped with a regular expression-based type system that provides more precise types
for iterations using techniques similar to those in [7]. In µXQ, the above expression can
be assigned the more accurate type b[]∗ , c[]? .
Accurate typing for iteration constructs is especially important in typechecking
XML updates. We are developing a statically-typed update language called F LUX [3] in
which ideas from µXQ are essential for typechecking updates involving iteration. Using
XQuery-style factoring for iteration in F LUX would make it impossible to typecheck
updates that modify data without modifying the overall schema of the database—a very
common case. For example, using XQuery-style factoring for iteration in F LUX, we
would not be able to verify statically that given a database of type a[b[string]∗ , c[]? ],
an update that modifies the text inside some of the b elements produces an output that
is still of type a[b[string]∗ , c[]? ], rather than a[(b[string]|c[])∗ ].
One question left unresolved in previous work on both µXQ and F LUX is the relationship between declarative and algorithmic presentations of the type system (in the
terminology of [14, Ch. 15–16]). Declarative derivations permit arbitrary uses of the
subsumption rule:
Γ ⊢ e : τ τ <: τ ′
Γ ⊢ e : τ′
whereas algorithmic derivations limit the use of this rule in order to ensure that typechecking is syntax-directed and decidable. The declarative and algorithmic presentations of a system should agree. If they do, then declarative typechecking is decidable;
if they disagree, then the algorithmic system is incomplete relative to the high-level
declarative system: it rejects programs that should typecheck.
The XQuery standard circumvented this issue by directly defining typechecking to
be algorithmic. In contrast, neither subsumption nor subtyping were considered in µXQ,
in part because subtyping interacts badly with µXQ’s “path correctness” analysis (as argued by Colazzo et al. [4], Section 4.4). Subsumption was considered in our initial work
on F LUX [3], but we were initially unable to establish that declarative typechecking was
decidable, even in the absence of recursion in types, queries, or updates.
In this paper we consider declarative typechecking for µXQ and F LUX extended
with recursive types, recursive functions, and recursive update procedures. To establish that typechecking remains decidable, it suffices (following Pierce [14, Ch. 16])
to define an algorithmic typechecking judgment and prove its completeness; that is,
that declarative derivations can always be normalized to algorithmic derivations. For
XQuery proper, this appears straightforward because of the use of factoring when typechecking iterations. However, for µXQ’s more precise iteration type discipline, completeness of algorithmic typechecking does not follow by the “obvious” structural induction. Instead, we must establish a stronger property by considering the structure of
regular expression types. We also extend these results to F LUX.
2

The structure of the rest of the paper is as follows. Section 2 reviews regular expression types and subtyping. Section 3 introduces the core language µXQ, discusses
examples highlighting the difficulties involving subtyping in µXQ, and proves decidability of declarative typechecking. We also review the F LUX core update language in
Section 4, discuss examples, and extend the proof of decidability of declarative typechecking to F LUX. Sections 5–6 sketch related and future work and conclude.

2 Background
For the purposes of this paper, XML values are trees built up out of booleans b ∈ Bool =
{true, false}, strings w ∈ Σ ∗ over some alphabet Σ, and labels l, m, n ∈ Lab,
according to the following syntax:
v̄ ::= b | w | n[v]

v ::= v̄, v | ()

Values include tree values v̄ ∈ Tree and forest values v ∈ Val. We write v, v ′ for the
result of appending two forest values (considered as lists).
We consider a regular expression type system with structural subtyping, similar to
those considered in several transformation and query languages for XML [13,4,7]. The
syntax of types and type environments is as follows.
Atomic types
α ::= bool | string | n[τ ]
Sequence types τ ::= α | () | τ |τ ′ | τ, τ ′ | τ ∗ | X
Type definitions τ0 ::= α | () | τ0 |τ0′ | τ0 , τ0′ | τ0∗
Type signatures E ::= · | E, type X = τ0
We call types of the form α ∈ Atom atomic types (or sometimes tree or singular types),
and types τ ∈ Type of all other forms sequence types (or sometimes forest or plural
types). It should be obvious that a value of singular type must always be a sequence
of length one (that is, a tree); plural types may have values of any length. There exist
plural types with only values of length one, but which are not syntactically singular
(for example int|bool). As usual, the + and ? quantifiers can be defined as follows:
τ + = τ, τ ∗ and τ ? = τ |(). We abbreviate n[()] as n[].
Note that in contrast to Hosoya et al. [13], but following Colazzo et al. [4], we
include both Kleene star and type variables. In [13], it was shown that Kleene star can
be translated away by introducing type variables and definitions, modulo a syntactic
restriction on top-level occurrences of type variables. In contrast, we allow Kleene star,
but further restrict type variables. Recursive and mutually recursive declarations are
allowed, but type variables may not appear at the top level of a type definition τ0 : for
example, type X = nil[]|cons(a, X) and type Y = leaf []|node[X, X] are allowed
but type X ′ = ()|a[], X and type Y ′ = b[]|Y ′ , Y ′ are not. The equation for X ′
defines the regular tree language a[]∗ , and would be permitted in XDuce, while that for
Y ′ defines a context-free tree language that is not regular.
An environment E is well-formed if all type variables appearing in definitions are
themselves declared in E. Given a well-formed environment E, we write E(X) for the
3

definition of X. A type denotes the set of values [[τ ]]E , defined as follows.
[[string]]E = Σ ∗
[[bool]]E = Bool
[[()]]E = {()}
[[n[τ ]]]E = {n[v] | v ∈ [[τ ]]E }
[[X]]E = [[E(X)]] [[τ |τ ′ ]]E = [[τ ]]E ∪ [[τ ′ ]]E
[[τ, τ ′ ]]E = {v, v ′ | v ∈ [[τ ]]E , v ′ ∈ [[τ ′ ]]E }
[[τ ∗ ]]E = {()} ∪ {v1 , . . . , vn | v1 ∈ [[τ ]]E , . . . , vn ∈ [[τ ]]E }
Formally, [[τ ]]E must be defined by a least fixed point construction which we take for
granted. Henceforth, we treat E as fixed and define [[τ ]] = [[τ ]]E .
In addition, we define a binary subtyping relation on types. A type τ1 is a subtype
of τ2 (τ1 <: τ2 ), by definition, if [[τ1 ]] ⊆ [[τ2 ]]. Our types can be translated to XDuce
types, so subtyping reduces to XDuce subtyping; although this problem is EXPTIMEcomplete in general, the algorithm of [13] is well-behaved in practice. Therefore, we
shall not give explicit inference rules for checking or deciding subtyping, but treat it as
a “black box”.

3 Query language
We review an XQuery-like core language based on µXQ [4]. In µXQ, we distinguish
between tree variables x̄ ∈ TVar , introduced by for, and forest variables, x ∈ Var ,
introduced by let. We write x̂ ∈ Var ∪ TVar for an arbitrary variable. The other
syntactic classes of our variant of µXQ include booleans, strings, and labels introduced
above, function names F ∈ FSym, expressions e ∈ Expr , and programs p ∈ Prog; the
abstract syntax of expressions and programs is defined as follows:
e ::= () | e, e′ | n[e] | w | x | let x = e in e′ | F (e1 , . . . , en )
| b | if c then e else e′ | x̄ | x̄/child | e :: n | for x̄ ∈ e return e′
p ::= query e : τ | declare function F (x1 :τ1 , . . . , xn :τn ) : τ {e}; p
The distinguished variables x̄ in for x̄ ∈ e return e′ (x̄) and x in let x = e in e′ (x)
are bound in e′ (x). Here and elsewhere, we employ common conventions such as considering expressions containing bound variables equivalent up to α-renaming and employing a richer concrete syntax including parentheses.
To simplify the presentation, we split µXQ’s projection operation x̄/child :: l into
two expressions: child projection (x̄/child) which returns the children of x̄, and node
name filtering (e :: n) which evaluates e to an arbitrary sequence and selects the nodes
labeled n. Thus, the ordinary child axis expression x̄/child :: n is syntactic sugar for
(x̄/child) :: n and the “wildcard” child axis is definable as x̄/child :: ∗ = x̄/child.
Built-in operations such as string equality may be provided as additional functions F .
Colazzo et al. [4] provided a denotational semantics of µXQ queries with the descendant axis but without recursive functions. This semantics is sound with respect to the
typing rules in the next section and can be extended to handle recursive functions using
operational techniques (as in the XQuery standard). However, we omit the semantics
since it is not needed in the rest of the paper.
4

Γ ⊢e:τ
x̄:α ∈ Γ
Γ ⊢ x̄ : α

x:τ ∈ Γ
b ∈ Bool
Γ ⊢ x : τ Γ ⊢ w : string Γ ⊢ b : bool
Γ ⊢ e : τ Γ ⊢ e′ : τ ′ Γ ⊢ e1 : τ1 Γ, x:τ1 ⊢ e2 : τ2
Γ ⊢e:τ
Γ ⊢ () : () Γ ⊢ n[e] : n[τ ]
Γ ⊢ e, e′ : τ, τ ′
Γ ⊢ let x = e1 in e2 : τ2
x̄:n[τ ] ∈ Γ
Γ ⊢ c : bool Γ ⊢ e1 : τ1 Γ ⊢ e2 : τ2
Γ ⊢ e : τ τ :: n ⇒ τ ′
Γ ⊢ if c then e1 else e2 : τ1 |τ2
Γ ⊢ x̄/child : τ
Γ ⊢ e :: n : τ ′
Γ ⊢ e1 : τ1 Γ ⊢ x̄ in τ1 → e2 : τ2 F (τ ) : τ0 ∈ ∆ Γ ⊢ ei : τi Γ ⊢ e : τ τ <: τ ′
Γ ⊢ for x̄ ∈ e1 return e2 : τ2
Γ ⊢ F (e) : τ0
Γ ⊢ e : τ′
Γ ⊢ p prog
F not declared in p F (τ ) : τ0 ∈ ∆ Γ, x : τ ⊢ e : τ0 Γ ⊢ p prog
Γ ⊢ declare function F (τ ) : τ0 {e}; p prog

Γ ⊢e:τ
Γ ⊢ e : τ prog

Fig. 1. Query and program well-formedness rules
τ :: n ⇒ τ ′

Γ ⊢ x̄ in τ → e : τ ′

n[τ ] :: n ⇒ n[τ ]
E(X) :: n ⇒ τ
α 6= n[τ ]
X :: n ⇒ τ
α :: n ⇒ ()
τ1 :: n ⇒ τ2
() :: n ⇒ () τ1∗ :: n ⇒ τ2∗
τ1 :: n ⇒ τ1′ τ2 :: n ⇒ τ2′
τ1 , τ2 :: n ⇒ τ1′ , τ2′
τ1 :: n ⇒ τ1′ τ2 :: n ⇒ τ2′
τ1 |τ2 :: n ⇒ τ1′ |τ2′

Γ ⊢ x̄ in E(X) → e : τ
Γ ⊢ x̄ in () → e : ()
Γ ⊢ x̄ in X → e : τ
Γ, x̄:α ⊢ e : τ
Γ ⊢ x̄ in τ1 → e : τ2
Γ ⊢ x̄ in α → e : τ Γ ⊢ x̄ in τ1∗ → e : τ2∗
Γ ⊢ x̄ in τ1 → e : τ1′ Γ ⊢ x̄ in τ2 → e : τ2′
Γ ⊢ x̄ in τ1 , τ2 → e : τ1′ , τ2′
Γ ⊢ x̄ in τ1 → e : τ1′ Γ ⊢ x̄ in τ2 → e : τ2′
Γ ⊢ x̄ in τ1 |τ2 → e : τ1′ |τ2′

Fig. 2. Auxiliary judgments

3.1 Type system
Our type system for queries is essentially that introduced for µXQ by [4], excluding the
path correctness component. We consider typing environments Γ and global declaration
environments ∆, defined as follows:
Γ ::= · | Γ, x:τ | Γ, x̄:α

∆ ::= · | ∆, F (τ ) : τ0

Note that in Γ , tree variables may only be bound to atomic types. As usual, we assume
that variables in type environments are distinct; this convention implicitly constrains
all inference rules. We also write Γ <: Γ ′ to indicate that dom(Γ ) = dom(Γ ′ ) and
Γ ′ (x̂) <: Γ (x̂) for all x̂ ∈ dom(Γ ).
The main typing judgment for queries is Γ ⊢ e : τ ; we also define a program wellformedness judgment Γ ⊢ p prog which typechecks the bodies of functions. Following
5

[4], there are two auxiliary judgments, Γ ⊢ x̄ in τ → s : τ ′ , used for typechecking
for-expressions, and τ :: n ⇒ τ ′ , used for typechecking label matching expressions
e :: n. The rules for these judgments are shown in Figures 1 and 2.
We consider the typing rules to be implicitly parameterized by a fixed global declaration environment ∆. Functions in XQuery have global scope so we assume that
the declarations for all the functions declared in the program have already been added
to ∆ by a preprocessing pass. Additional declarations for built-in functions might be
included in ∆ as well.
The rules involving type variables in Figure 2 look up the variable’s definition in E.
These judgments only inspect the top-level of a type; they do not inspect the contents
of element types n[τ ]. Since type definitions τ0 have no top-level type variables, both
judgments are terminating. (This was argued in detail by Colazzo et al. [4, Lem. 4.6].)
3.2 Examples
We first revisit the example in the introduction in order to illustrate the operation of the
rules. Recall that x̄/∗ is translated to x̄/child in our core language.
x̄:a[b[]∗ , c[]? ] ⊢ x̄/child : b[]∗ , c[]?

D
x̄:a[b[]∗ , c[]? ] ⊢ ȳ in b[]∗ , c[]? → ȳ : b[]∗ , c[]?

x̄:a[b[]∗ , c[]? ] ⊢ for ȳ ∈ x̄/child return ȳ : b[]∗ , c[]?

where the subderivation D is
x̄:a[b[]∗ , c[]? ], ȳ:b[] ⊢ ȳ : b[]

D=

x̄:a[b[]∗ , c[]], ȳ:c[] ⊢ ȳ : c[]

x̄:a[b[]∗ , c[]? ] ⊢ ȳ in b[] → ȳ : b[]
?

∗

∗

x̄:a[b[]∗ , c[]? ] ⊢ ȳ in c[] → ȳ : c[]
x̄:a[b[]∗ , c[]? ] ⊢ ȳ in c[]? → ȳ : c[]?

∗

x̄:a[b[] , c[] ] ⊢ ȳ in b[] → ȳ : b[]

x̄:a[b[]∗ , c[]? ] ⊢ ȳ in b[]∗ , c[]? → ȳ : b[]∗ , c[]?

Note that this derivation does not use subsumption anywhere. Suppose we wished
to show that the expression has type b[]∗ , (c[]? |d[]∗ ), a supertype of the above type.
There are several ways to do this: first, we can simply use subsumption at the end
of the derivation. Alternatively, we could have used subsumption in one of the subderivations such as x̄:a[b[]∗ , c[]? ], ȳ:c[]? ⊢ ȳ : c[]? , to conclude, for example, that
x̄:a[b[]∗ , c[]? ], ȳ:c[]? ⊢ ȳ : c[]? |d[]∗ . This is valid since c[]? <: c[]? |d[]∗ .
Suppose, instead, that we actually wanted to show that the above expression has
type (b[d[]∗ ]|c[]? )∗ , also a supertype of the derived type. There are again several ways
of doing this. Besides using subsumption at the end of the derivation, we might have
used it on x̄:a[b[]∗ , c[]? ] ⊢ x̄/child : b[]∗ , c[]? to obtain x̄:a[b[]∗ , c[]? ] ⊢ x̄/child :
(b[d[]∗ ]|c[]? )∗ . To complete the derivation, we would then need to replace derivation D
with D′ :
x̄:a[b[]∗ , c[]? ], ȳ:c[] ⊢ ȳ : c[]
x̄:a[b[]∗ , c[]? ], ȳ:b[d[]∗ ] ⊢ ȳ : b[d[]∗ ]
′

x̄:a[b[]∗ , c[]? ] ⊢ ȳ in c[] → ȳ : c[]

D = x̄:a[b[] , c[] ] ⊢ ȳ in b[d[] ] → ȳ : b[d[] ] x̄:a[b[]∗ , c[]? ] ⊢ ȳ in c[]? → ȳ : c[]?
∗

?

∗

∗

x̄:a[b[]∗ , c[]? ] ⊢ ȳ in b[d[]∗ ]|c[]? → ȳ : b[d[]∗ ]|c[]?
x̄:a[b[]∗ , c[]? ] ⊢ ȳ in (b[d[]∗ ]|c[]? )∗ → ȳ : (b[d[]∗ ]|c[]? )∗

6

Not only does D′ have different structure than D, but it also requires subderivations that
were not syntactically present in D.
The above example illustrates why eliminating uses of subsumption is tricky. If subsumption is used to weaken the type of the first argument of a for-expression according
to τ1′ <: τ1 , then we need to know that we can transform the corresponding derivation
D of Γ ⊢ x̄ in τ1 → e : τ2 to a derivation of D′ of Γ ⊢ x̄ in τ1′ → e : τ2′ for some
τ2′ <: τ2 . But as illustrated above, the derivations D and D′ may bear little resemblance
to one another.
Now we consider a typechecking a recursive query. Suppose we have type Tree =
tree[leaf [string]|node[Tree ∗ ]] and function definition
declare function leaves(x : Tree) : leaf [string]∗ {
x/leaf , for z̄ ∈ x/node/ ∗ return leaves(z̄)
};
This uses a construct e/n that is not in core µXQ, but we can expand e/n to for ȳ ∈
e return ȳ/child :: n; thus, we can derive a rule
Γ, ȳ:l[τ ] ⊢ ȳ/child : τ τ :: n ⇒ τ ′
Γ, ȳ:l[τ ] ⊢ ȳ/child :: n : τ ′
Γ ⊢ e : l[τ ] τ :: n ⇒ τ ′
Γ ⊢ e : l[τ ]
Γ ⊢ ȳ in l[τ ] → ȳ/child :: n : τ ′
′
Γ ⊢ e/n : τ
⇐⇒
Γ ⊢ for ȳ ∈ e return ȳ/child :: n : τ ′
Using this derived rule and the fact that x : Tree and the definition of Tree, we
can see that x/leaf : leaf [string] and x/node : node[Tree ∗ ]], and so x/node/∗ :
tree[leaf [string]|node[Tree ∗ ]]∗ . So each iteration of the for-loop can be typechecked
with z̄ : tree[leaf [string]|node[Tree ∗ ]]. To check the function call leaves(z̄), we need
subsumption to see that tree[leaf [string]|node[Tree ∗ ]]∗ <: Tree. It follows that that
leaves(z̄) : leaf [string]∗ , so the for-loop has type (leaf [string]∗ )∗ . Again using
subsumption, we can conclude that
x/leaf , leaves(x/node/∗) : leaf [string], (leaf [string]∗ )∗ <: leaf [string]∗ .
Notice that although we could have used subsumption in several more places, we really
needed it in only two places: when typechecking a function call, and when checking the
result of a function against its declared type.
3.3 Decidability
The standard approach (see e.g. Pierce [14, Ch. 16]) to deciding declarative typechecking is to define algorithmic judgments that are syntax-directed and decidable, and then
show that the algorithmic system is complete relative to the declarative system.
Definition 1 (Algorithmic derivations). The algorithmic typechecking judgments Γ ⊢◮
e : τ and Γ ⊢◮ x̄ in τ0 → e : τ are defined by taking the rules of Figures 1 and 2,
removing the subsumption rule, and replacing the function application rule with
F (τ ) : τ ∈ Γ Γ ⊢◮ ei : τi′
Γ ⊢◮ F (e) : τ
7

τi′ <: τi

It is straightforward to show that algorithmic derivability is decidable and sound
with respect to the declarative system:
Lemma 1 (Decidability). For any x̄, e, n, there exist computable partial functions fn ,
ge , hx̄,y such that for any Γ, τ0 , we have:
1. fn (τ0 ) is the unique τ such that τ0 :: n ⇒ τ .
2. gx (Γ ) is the unique τ such that Γ ⊢◮ e : τ , when it exists.
3. hx̄,e (Γ, τ0 ) is the unique τ such that Γ ⊢◮ x̄ in τ0 → e : τ , when it exists.
Theorem 1 (Algorithmic Soundness). (1) If Γ ⊢◮ e : τ is derivable then Γ ⊢ e : τ
is derivable. (2) If Γ ⊢◮ x̄ in τ0 → e : τ is derivable then Γ ⊢ x̄ in τ0 → e : τ is
derivable.
The corresponding completeness property (the main result of this section) is:
Theorem 2 (Algorithmic Completeness). (1) If Γ ⊢ e : τ then there exists τ ′ <: τ
such that Γ ⊢◮ e : τ ′ . (2) If Γ ⊢ x̄ in τ1 → e : τ2 then there exists τ2′ <: τ2 such that
Γ ⊢◮ x̄ in τ1 → e : τ2′ .
Given a decidable subtyping relation <:, a typical proof of completeness involves showing by induction that occurrences of the subsumption rule can be “permuted” downwards in the proof past other rules, except for function applications. Completeness for
µXQ requires strengthening this induction hypothesis. To see why, recall the following
rules:
∗
Γ ⊢ e1 : τ1 Γ, x:τ1 ⊢ e2 : τ2
Γ ⊢ let x = e1 in e2 : τ2

∗
Γ ⊢ e1 : τ1 Γ ⊢ x̄ in τ1 → e2 : τ2
Γ ⊢ for x̄ ∈ e1 return e2 : τ2

∗
Γ ⊢ e : τ τ :: n ⇒ τ ′
Γ ⊢ e :: n : τ ′

If the subderivation labeled ∗ in the above rules follows by subsumption, however, we
cannot do anything to get rid of the subsumption rule using the induction hypotheses
provided by Theorem 2. Instead we need an additional lemma that ensures that the judgments are all downward monotonic. Downward monotonicity means, informally, that if
make the “input” types in a derivable judgment smaller, then the judgment remains
derivable with a smaller “output” type.
Lemma 2 (Downward monotonicity).
1. If τ1 :: n ⇒ τ2 and τ1′ <: τ1 then τ1′ :: n ⇒ τ2′ for some τ2′ <: τ2
2. If Γ ⊢◮ e : τ and Γ ′ <: Γ then Γ ′ ⊢◮ e : τ ′ for some τ ′ <: τ .
3. If Γ ⊢◮ x̄ in τ1 → e : τ2 and Γ ′ <: Γ and τ1′ <: τ1 then Γ ′ ⊢◮ x̄ in τ1′ → e : τ2′
for some τ2′ <: τ2 .
The downward monotonicity lemma is almost easy to prove by direct structural
induction (simultaneously on all judgments). The cases for (2) involving expressiondirected typechecking are all straightforward inductive steps; however, for the cases
involving type-directed judgments, the induction steps do not go through. The difficulty
is illustrated by the following cases. For derivations of the form
τ1 :: n ⇒ τ2
τ1∗ :: n ⇒ τ2∗

Γ ⊢ x̄ in τ1 → e : τ2
Γ ⊢ x̄ in τ1∗ → e : τ2∗
8

we are stuck: knowing that τ1′ <: τ1∗ does not necessarily tell us anything about a
subtyping relationship between τ1′ and τ1 . For example, if τ1′ = aa and τ1 = a, then we
have aa <: a∗ but not aa <: a. Instead, we need to proceed by an analysis of regular
expression types and subtyping.
We briefly sketch the argument, which involves an excursion into the theory of
regular languages over partially ordered alphabets. Here, the “alphabet” is the set of
atomic types and the regular sets are the sets of sequences of atomic types that are
subtypes of a type τ . The homomorphic extension of a (possibly partial) function h :
Atom ⇀ Type on atomic types is defined as
ĥ(()) = ()
ĥ(α) = h(α)
ĥ(τ ∗ ) = ĥ(τ )∗
ĥ(τ1 , τ2 ) = ĥ(τ1 ), ĥ(τ2 ) ĥ(τ1 |τ2 ) = ĥ(τ1 )|ĥ(τ2 ) ĥ(X) = ĥ(E(X))
(Note again that this definition is well-founded, since type variables cannot be expanded
indefinitely.) If h is partial, then ĥ is defined only on types whose atoms are in dom(h).
We can then show the following general property of partial homomorphic extensions:
Lemma 3. If h : Atom ⇀ Type is downward monotonic, then its homomorphic extension ĥ : Type ⇀ Type is downward monotonic.
It then suffices to show that fn and hx̄,e are partial homomorphic extensions of
downward monotone functions on atomic types; for fn , the required function is simple and obviously monotone, and for hx̄,e (Γ, −), the required generating function is
ge (Γ, x:(−)). Thus, we need to show that ge and hx̄,e are downward monotonic and
that hx̄,e (Γ, −) is the partial homomorphic extension of ge (Γ, x:(−)) simultaneously
by mutual induction. This, finally, is a straightforward induction over derivations. More
detailed proofs are included in the appendix.

4 Update language
We now introduce the core F LUX update language, which extends the syntax of queries
with statements s ∈ Stmt, procedure names P ∈ PSym, tests φ ∈ Test , directions
d ∈ Dir , and two new cases for programs:
s ::= skip | s; s′ | if e then s else s′ | let x = e in s | P (e)
| insert e | delete | rename n | snapshot x in s | φ?s | d[s]
φ ::= n | ∗ | bool | string
d ::= left | right | children | iter
′
p ::= · · · | update s : τ ⇒ τ | declare procedure P (x : τ ) : τ ⇒ τ ′ {s}; p
Updates include standard programming constructs such as the no-op skip, sequential
composition, conditionals, and let-binding. The basic update operations include insertion insert e, which inserts a value into an empty part of the database; deletion
delete, which deletes part of the database; and rename n, which renames a part of the
database provided it is a single tree. The “snapshot” operation snapshot x in s binds
x to part of the database and then applies an update s, which may refer to x. Note that
the snapshot operation is the only way to read from the current database state.
9

Updates also include tests φ?s which test the top-level type of a singular value and
conditionally perform an update, otherwise do nothing. The node label test n?s checks
whether the tree is of type n[τ ], and if so executes s; the wildcard test ∗?s checks that
the value is a tree. Similarly, bool?s and string?s test whether a value is a boolean or
string. The ? operator binds tightly; for example, φ?s; s′ = (φ?s); s′ .
Finally, updates include navigation operators that change the selected part of the
tree, and perform an update on the sub-selection. The left and right operators perform an update (typically, an insert) on the empty sequence located to the left or right
of a value. The children operator applies an update to the child list of a tree value.
The iter operator applies an update to each tree value in a forest.
We distinguish between singular (unary) updates which apply only when the context is a tree value and plural (multi-ary) updates which apply to a sequence. Tests φ?s
are always singular. The children operator applies a plural update to all of the children of a single node; the iter operator applies a singular update to all of the elements
of a sequence. Other updates can be either singular or plural in different situations. Our
type system tracks multiplicity as well as input and output types in order to ensure that
updates are well-behaved.
F LUX updates operate on a part of the database that is “in focus”, which helps ensure that updates are deterministic and relatively easy to typecheck. Only the navigation
operations left, right, children, iter can change the focus. We lack space to formalize the semantics of updates in the main body of the paper; the semantics of updates
is essentially the same as in [3] except for the addition of procedures.
4.1 Type system
In typechecking updates, we extend the global declaration context ∆ with procedure
declarations:
∆ ::= · · · | ∆, P (τ ) : τ1 ⇒ τ2
There are two typing judgments for updates: singular well-formedness Γ ⊢1 {α} s {τ ′ }
(that is, in type environment Γ , update s maps tree type α to type τ ′ ), and plural wellformedness Γ ⊢∗ {τ } s {τ ′ } (that is, in type environment Γ , update s maps type τ to
type τ ′ ). Several of the rules are parameterized by a multiplicity a ∈ {1, ∗}. In addition,
there is an auxiliary judgment Γ ⊢iter {τ } s {τ ′ } for typechecking iterations. The rules
for update well-formedness are shown in Figure 3. We also need an auxiliary subtyping
relation involving atomic types and tests: we say that α <: φ if [[α]] ⊆ [[φ]]. This is
characterized by the rules:
bool <: bool string <: string n[τ ] <: n

n[τ ] <: ∗

Remark 1. In most other XML update proposals (including XQuery! [11] and the draft
XQuery Update Facility [2]), side-effecting update operations are treated as expressions
that return (). Thus, we could perhaps typecheck such updates as expressions of type
(). This would work fine as long as the types of values reachable from the free variables in Γ can never change; however, the updates available in these languages can and
do change the values of variables. Thus, to make this approach sound Γ would to be
10

Γ ⊢a {τ } s {τ ′ }
Γ ⊢a {τ } s {τ ′ } Γ ⊢a {τ ′ } s′ {τ ′′ } Γ ⊢ e : τ Γ, x:τ ⊢a {τ1 } s {τ2 }
Γ ⊢ {τ } skip {τ }
Γ ⊢a {τ } s; s′ {τ ′′ }
Γ ⊢a {τ1 } let x = e in s {τ2 }
a
a
′
Γ ⊢ e : bool Γ ⊢ {τ } s {τ1 } Γ ⊢ {τ } s {τ2 }
Γ, x:τ ⊢a {τ } s {τ ′ }
a

Γ ⊢a {τ } if e then s else s′ {τ1 |τ2 }
Γ ⊢a {τ } snapshot x in s {τ ′ }
Γ ⊢e:τ
Γ ⊢∗ {()} insert e {τ } Γ ⊢a {τ } delete {()} Γ ⊢1 {n′ [τ ]} rename n {n[τ ]}
α <: φ Γ ⊢1 {α} s {τ }
Γ ⊢1 {α} φ?s {τ }
Γ ⊢∗ {()} s {τ ′ }

α 6<: φ

Γ ⊢∗ {τ } s {τ ′ }

Γ ⊢1 {α} φ?s {α} Γ ⊢1 {n[τ ]} children[s] {n[τ ′ ]}
Γ ⊢∗ {()} s {τ ′ }
Γ ⊢iter {τ } s {τ ′ }

Γ ⊢a {τ } left[s] {τ ′ , τ } Γ ⊢a {τ } right[s] {τ, τ ′ } Γ ⊢∗ {τ } iter[s] {τ ′ }
Γ ⊢a {τ1 } s {τ2′ } τ2′ <: τ2 P (τ ) : σ ⇒ σ2 ∈ ∆ σ1 <: σ Γ ⊢ e : τ
Γ ⊢a {τ1 } s {τ2 }
Γ ⊢a {σ1 } P (e) {σ2 }
Γ ⊢iter {τ } s {τ ′ }
Γ ⊢1 {α} s {τ } Γ ⊢iter {E(X)} s {τ } Γ ⊢iter {τ1 } s {τ2 }
Γ ⊢iter {()} s {()} Γ ⊢iter {α} s {τ }
Γ ⊢iter {X} s {τ }
Γ ⊢iter {τ1∗ } s {τ2∗ }
Γ ⊢iter {τ1 } s {τ1′ } Γ ⊢iter {τ2 } s {τ2′ } Γ ⊢iter {τ1 } s {τ1′ } Γ ⊢iter {τ2 } s {τ2′ }
Γ ⊢iter {τ1 , τ2 } s {τ1′ , τ2′ }

Γ ⊢iter {τ1 |τ2 } s {τ1′ |τ2′ }

Γ ⊢ p prog

Γ ⊢∗ {τ1 } s {τ2 }
Γ ⊢ update s : τ1 ⇒ τ2 prog

P not declared in p
P (τ ) : σ1 ⇒ σ2 ∈ ∆ Γ, x:τ ⊢∗ {σ1 } s {σ2 } Γ ⊢ p prog
Γ ⊢ declare procedure P (x : τ ) : τ1 ⇒ τ2 {s}; p prog

Fig. 3. Update and additional program well-formedness rules

updated to take these changes into account, perhaps using a judgment Γ ⊢ s : () | Γ ′ ,
where Γ ′ is the updated type environment reflecting the types of the variables after update s. This approach quickly becomes difficult to manage, especially if it is possible
for different variables to “alias”, or refer to overlapping parts of the data accessible from
Γ , and adding side-effecting functions further complicates matters.
This is not the approach to update typechecking that is taken in F LUX. Updates are
syntactically distinct from queries, and a F LUX update typechecking judgment such as
Γ ⊢a {τ } s {τ ′ } assigns an update much richer type information that describes the
type of part of the database before and after running s. The values of variables bound
in Γ are immutable in the variable’s scope, so their types do not need to be updated.
Similarly, procedures must be annotated with expected input and output types. We do
not believe that these annotations are burdensome in a database setting since a typical
update procedure would be expected to preserve the (usually fixed) type of the database.
11

⊢ c[] : c[]
⊢∗ {()} insert c[] {b[], c[]}
⊢1 {b[]} right insert c[] {b[], c[]}
⊢1 {b[]} b?s′ {b[], c[]}
⊢iter {b[]} b?s′ {b[], c[]}
⊢iter {b[]∗ } b?s′ {(b[], c[])∗ }
∗

′

∗

⊢iter {b[] , c[]} b?s {(b[], c[]) , c[]}

⊢1 {c[]} b?s′ {c[]}
⊢iter {c[]} b?s′ {c[]}

⊢∗ {b[]∗ , c[]} iter [b?s′ ] {(b[], c[])∗ , c[]}
1

⊢ {a[b[]∗ , c[]]} children[s] {a[(b[], c[])∗ , c[]]}
⊢iter {a[b[]∗ , c[]]} a?children[s] {a[(b[], c[])∗ , c[]]}
⊢iter {d[]} a?children[s] {d[]}
⊢iter {a[b[]∗ , c[]], d[]} a?children[s] {a[(b[], c[])∗ , c[]], d[]}
⊢∗ {a[b[]∗ , c[]], d[]} iter [a?children[s]] {a[(b[], c[])∗ , c[]], d[]}

Fig. 4. Example update derivation, where s′ = right insert c[] and s = iter [b?s′ ]
leafupd (string) : Tree ⇒ Tree ∈ ∆

tree[...] <: Tree

1

x:string ⊢ x : string

∗

x:string ⊢ {tree[leaf [string]|node[Tree ]]} leafupd (x) {Tree}
x:string ⊢iter {tree [leaf [string]|node[Tree ∗ ]]} leafupd (x) {Tree}
x:string ⊢iter {Tree} leafupd (x) {Tree}
x:string ⊢iter {Tree ∗ } leafupd (x) {Tree ∗ }
x:string ⊢∗ {Tree ∗ } iter[leafupd (x)] {Tree ∗ }
∗
x:string ⊢ {node[Tree ∗ ]} children[iter[leafupd (x)]] {node[Tree ∗ ]}
x:string ⊢∗ {node[Tree ∗ ]} node?children[iter[leafupd (x)]] {node[Tree ∗ ]}

Fig. 5. Partial derivation for declaration of leafupd

4.2 Examples
The interesting rules are those involving iter, tests, and children, left/right, and
insert/rename/delete. The following example should help illustrate how the rules
work for these constructs. Consider the high-level update:
insert after a/b value c[]
which can be compiled to the following core F LUX statement:
iter [a?children [iter [b? right insert c[]]]]
Intuitively, this update inserts a c after every b under a top-level a. Now consider the
input type a[b[]∗ , c[]], d[]. Clearly, the output type should be a[(b[], c[])∗ , c[]], d[]. To see
how F LUX can assign this type to the update, consider the derivation shown in Figure 4.
12

As a second example, consider the procedure declaration
declare procedure leafupd (x:string) : Tree ⇒ Tree {
iter[children[iter[leaf ?children[delete; insert x];
node?children[iter[leafupd (x)]]]]]
};
This procedure updates all leaves of a tree to x. As with the recursive query discussed in
Section 3.2, this procedure requires subtyping to typecheck the recursive call. We also
need subtyping to check that the return type of the expression matches the declaration.
A partial typing derivation for part of the body of the procedure involving a recursive
call is shown in Figure 5.
4.3 Decidability
To decide typechecking, we must again carefully control the use of subsumption. The
appropriate algorithmic typechecking judgment is defined as follows:
Definition 2 (Algorithmic derivations for updates). The algorithmic typechecking
judgments Γ ⊢◮a {τ } s {τ ′ } and Γ ⊢◮iter {τ } s {τ ′ } are obtained by taking the rules in
Figure 3, removing both subsumption rules, and replacing the procedure call rule with
P (σ) : σ ⇒ σ ′ ∈ ∆ τ <: σ Γ ⊢◮ e : τ
Γ ⊢◮a {τ } P (e) {σ ′ }

τ <: σ

Moreover, all subderivations of expression judgments in an algorithmic derivation of
an update judgment must be algorithmic.
The proof of completeness of algorithmic update typechecking has the same structure as that for queries. We state the main results; proof details are in the appendix.
Lemma 4 (Decidabilty for updates). Let a, s be given. Then there exist computable
functions ja,s and ks such that:
1. ja,s (Γ, τ ) is the unique τ2 such that Γ ⊢◮a {τ1 } s {τ2 }, if it exists.
2. ks (Γ, τ1 ) is the unique τ2 such that Γ ⊢◮iter {τ1 } s {τ2 }, if it exists.
Theorem 3 (Algorithmic soundness for updates). (1) If Γ ⊢◮∗ {τ } s {τ ′ } is derivable
then Γ ⊢◮∗ {τ } s {τ ′ } is derivable. (2) If Γ ⊢◮iter {τ } e {τ ′ } is derivable then Γ ⊢iter
{τ } e {τ ′ } is derivable.
Lemma 5 (Downward monotonicity for updates). (1) If Γ ⊢◮a {τ1 } s {τ2 } and Γ ′ <:
Γ and τ1′ <: τ1 then Γ ′ ⊢◮a {τ1′ } s {τ2′ } for some τ2′ <: τ2 . (2) If Γ ⊢◮iter {τ1 } s {τ2 }
and Γ ′ <: Γ and τ1′ <: τ1 then Γ ′ ⊢◮iter {τ1′ } s {τ2′ } for some τ2′ <: τ2 .
Theorem 4 (Algorithmic completeness for updates). (1) If Γ ⊢a {τ1 } s {τ2 } then
there exists τ2′ <: τ2 such that Γ ⊢◮a {τ1 } s {τ2′ }. (2) If Γ ⊢iter {τ1 } s {τ2 } then there
exists τ2′ <: τ2 such that Γ ⊢◮iter {τ1 } s {τ2′ }.
13

5 Related and future work
This work is directly motivated by our interest in using regular expression types for
XML updates, using richer typing rules for iteration as found in µXQ [4]. Fernandez,
Siméon and Wadler [7] earlier considered an XML query language with more precise
typechecking for iteration, but this proposal required many more type annotations than
XQuery, µXQ or F LUX do; we only require annotations on function or procedure declarations.
For brevity, the core languages in this paper omitted many features of full XQuery,
such as the descendant, attribute, parent and sibling axes. The attribute axis is straightforward since attributes always have text content. In µXQ, the descendant axis was supported by assigning x̄/descendant-or-self the type formed by taking the union
of all tree types that are reachable from the type of x̄. XQuery handles other axes by
discarding type information. Our algorithmic completeness proof still appears to work
if these axes are added.
We are also interested in extending the path correctness analysis introduced by Colazzo et al. to F LUX. In the update setting, a natural form of path correctness might be
that there are no statically “dead” updates.
F LUX represents a fundamental departure from the other XML update language
proposals of which we are aware (such as XQuery! [10] and the draft W3C XQuery
Update Facility [2]). To the best of our knowledge, static typechecking and subtyping
have yet to be considered for such languages and seem likely to encounter difficulties for
reasons we outlined in Section 4.1 and discussed in more depth in [3]. In addition, F LUX
satisfies many algebraic laws that can be used to rewrite updates without first needing
to perform static analysis, whereas a sophisticated analysis needs to be performed in
XQuery! even to determine whether two query expressions can be reordered. We believe
that this will enable aggressive update optimizations.
On the other hand, XQuery! and related proposals are clearly more expressive than
F LUX, and have been incorporated into XML database systems such as Galax [6]. Although we currently have a prototype that implements the typechecking algorithm described here as well as the operational semantics described in [3], further work is needed
to develop a robust implementation inside an XML database system that could be used
to compare the scalability and optimizability of F LUX with other proposals.

6 Conclusions
Static typechecking is important in a database setting because type (or “schema”) information is useful for optimizing queries and avoiding expensive run-time checks or
re-validation. The XQuery standard, like other XML programming languages, employs
regular expression types and subtyping. However, its approach to typechecking iteration
constructs is imprecise, due to the use of “factoring” which discards information about
the order of elements in the result of an iteration operation such as a for-loop. While
this imprecision may not be harmful for typical queries, it is disastrous for typechecking
updates that are supposed to preserve the type of the database.
In this paper we have considered more precise typing disciplines for XQuery-style
iterative queries and updates in the core languages µXQ and F LUX respectively. In order
14

to ensure that these type systems are well-behaved and that typechecking is decidable, it
is important to prove the completeness of an algorithmic presentation of typechecking
in which the use of subtyping rules is limited so that typechecking remains syntaxdirected. We have shown how to do so for the core µXQ and F LUX languages, and
believe the proof technique will extend to handle other features not included in the
paper. These results provide a solid foundation for subtyping in XML query and update
languages with precise iteration typechecking rules and for combining them with other
XML programming paradigms based on regular expression types.

References
1. Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. CDuce: an XML-centric
general-purpose language. In ICFP ’03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, pages 51–63, New York, NY, USA, 2003.
ACM Press.
2. Don Chamberlin, Daniela Florescu, and Jonathan Robie. XQuery update facility. W3C
Working Draft, July 2006. http://www.w3c.org/TR/xqupdate/.
3. James Cheney. L UX: A lightweight, statically typed XML update language. In ACM SIGPLAN Workshop on Programming Language Technology and XML (PLAN-X 2007), pages
25–36, 2007.
4. Dario Colazzo, Giorgio Ghelli, Paolo Manghi, and Carlo Sartiani. Static analysis for path
correctness of XML queries. J. Funct. Program., 16(4-5):621–661, 2006.
5. Denise Draper, Peter Fankhauser, Mary Fernndez, Ashok Malhotra, Kristoffer Rose, Michael
Rys, Jérôme Siméon, and Philip Wadler. XQuery 1.0 and XPath 2.0 formal semantics. W3C
Recommendation, January 2007. http://www.w3.org/TR/xquery-semantics/.
6. Mary F. Fernández, Jérôme Siméon, Byron Choi, Amélie Marian, and Gargi Sur. Implementing XQuery 1.0: The Galax experience. In VLDB, pages 1077–1080, 2003.
7. Mary F. Fernandez, Jérôme Siméon, and Philip Wadler. A semi-monad for semi-structured
data. In ICDT ’01: Proceedings of the 8th International Conference on Database Theory,
pages 263–300, London, UK, 2001. Springer-Verlag.
8. Alain Frisch. OCaml + XDuce. In ICFP ’06: Proceedings of the eleventh ACM SIGPLAN
international conference on Functional programming, pages 192–200, New York, NY, USA,
2006. ACM Press.
9. Vladimir Gapeyev, François Garillot, and Benjamin C. Pierce. Statically typed document
transformation: An Xtatic experience. In Giuseppe Castagna and Mukund Raghavachari, editors, PLAN-X, pages 2–13. BRICS, Department of Computer Science, University of Aarhus,
2006.
10. G. Ghelli, K. Rose, and J. Siméon. Commutativity analysis in XML update languages. In
Dan Suciu and Thomas Schwentick, editors, ICDT, pages 374–388, January 2007.
11. Giorgio Ghelli, Christopher Re, and Jérôme Siméon. XQuery!: An XML query language
with side effects. In EDBT Workshops, volume 4254 of Lecture Notes in Computer Science,
pages 178–191. Springer, 2006.
12. Haruo Hosoya and Benjamin C. Pierce. XDuce: A statically typed XML processing language. ACM Trans. Internet Technology, 3(2):117–148, 2003.
13. Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. Regular expression types for
XML. ACM Trans. Program. Lang. Syst., 27(1):46–90, 2005.
14. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.

15

A

Proofs from Sections 3.3 and 4.3

A.1 Regular languages and homomorphisms
We assume familiarity with the theory of regular expressions and regular languages; in
this case, we consider types τ ∈ Type to be regular languages over atomic types α ∈
Atom. The language L(τ ) denoted by a type is therefore a set of sequences ω ∈ Atom ∗
of atomic types, where L : Type → Atom ∗ is defined as follows:
L(()) = {()}
L(α) = {α′ | α′ <: α}
L(τ, τ ′ ) = L(τ ) • L(τ ′ ) = {ω, ω ′ | ω ∈ L(τ ), ω ′ ∈ L(τ ′ )}
L(τ |τ ′ ) = L(τ ) ∪ L(τ ′ )
∞
[
L(τ )n
L(τ ∗ ) = L(τ )∗ =
i=0

L(X) = L(E(X))
Note that this definition differs slightly from the usual definition of the language of a
regular expression, in that we include all subtypes of atomic types α in L(α).
It is straightforward to show the following useful properties of L:
Lemma 6. L(τ ) = {ω | ω <: τ }
Proof. For both directions, proof is by induction on the structure of τ . For the forward
direction, we have:
– Case (): immediate
– Case α: Suppose ω ∈ L(α). Clearly ω = α′ <: α for some atomic α′ .
– Case τ1 , τ2 : Suppose ω ∈ L(τ1 , τ2 ). By definition, ω = ω1 , ω2 where ωi ∈ L(τi )
for i ∈ {1, 2}. Then by induction ωi <: τi for i ∈ {1, 2}. Thus ω1 , ω2 <: τ1 , τ2 .
– Case τ1 |τ2 : Suppose ω ∈ L(τ1 |τ2 ). By definition, ω = ωi where ω ∈ L(τi ) for
some i ∈ {1, 2}. Then by induction ω <: τi for some i ∈ {1, 2}. Thus ω <: τ1 |τ2 .
– Case τ ∗ : Suppose ω ∈ L(τ ∗ ). By definition, ω = ω1 , . . . , ωn where n ≥ 0 and
ωi ∈ L(τ ) for all i ∈ {1, . . . , n}. Then by induction ωi <: τ for all i ∈ {1, . . . , n}.
Thus ω = ω1 , . . . , ωn <: τ, . . . , τ <: τ ∗ .
– Case X: Immediate by induction.
For the reverse direction, we have:
– Case (): immediate, since we must have ω = () ∈ L(())
– Case α: Suppose ω <: α. Clearly ω = α′ <: α for some atomic α′ , so ω ∈ L(α).
– Case τ1 , τ2 : Suppose ω <: τ1 , τ2 . Then since ω is atomic we must have ω = ω1 , ω2
where ωi <: τi for i ∈ {1, 2}. Thus ω = ω1 , ω2 ∈ L(τ1 ) • L(τ2 ) = L(τ1 , τ2 ).
– Case τ1 |τ2 : Since ω is atomic, ω <: τ1 |τ2 implies that ω <: τ1 or ω <: τ2 . Thus
ω ∈ L(τ1 ) ∪ L(τ2 ) = L(τ1 |τ2 ).
– Case τ ∗ : Since ω is atomic, we must have ω = ω1 , . . . , ωn where ωi <: τ ; hence
ω = ω1 , . . . , ωn ∈ L(τ )∗ = L(τ ∗ ).
16

– Case X: Immediate by induction.
Lemma 7. If v ∈ [[τ ]], then there exists a ω ∈ L(τ ) such that v ∈ [[ω]].
Proof. Induction on the structure of v, τ .
– Case (), (): Immediate; ω = () works.
– Case v̄, α: Immediate; ω = α works.
– Case v, (τ1 , τ2 ): We must have v = v1 , v2 where vi ∈ [[τi ]], for i ∈ {1, 2}. Then by
induction we have ωi ∈ L(τi ) with vi ∈ [[ωi ]]; this implies v ∈ [[ω1 , ω2 ]] ⊆ [[τ1 , τ2 ]].
– Case v, τ1 |τ2 : Without loss of generality, suppose v ∈ [[τi ]]. Then by induction we
have ω ∈ L(τi ) ⊆ L(τ1 |τ2 ) such that v ∈ [[ω]] ⊆ [[τ1 |τ2 ]].
– Case v, τ ∗ : If v = (), then ω = () works. Otherwise we must have v = v1 , . . . , vn
where vi ∈ [[τ ]]. Then by induction we have ωi ∈ L(τ ) with vi ∈ [[ω]]; this implies
that ω1 , . . . , ωn ∈ L(τ ∗ ) and v ∈ [[ω1 , . . . , ωn ]] ⊆ [[τ ∗ ]].
– Case X: Immediate by induction.
Lemma 8. For any τ, τ ′ , τ <: τ ′ if and only if L(τ ) ⊆ L(τ ′ )
Proof. In the forward direction, if τ <: τ ′ , then let ω ∈ L(τ ) be given. Then ω <: τ <:
τ ′ . Thus, ω ∈ L(τ ′ ).
In the reverse direction, suppose that L(τ ) ⊆ L(τ ′ ). Suppose v ∈ [[τ ]]. Via Lemma 7,
choose ω such that v ∈ [[ω]] and ω ∈ L(τ ). Since L(τ ) ⊆ L(τ ′ ), we have that ω <: τ ′ ,
so v ∈ [[ω]] ⊆ [[τ ′ ]]. We conclude that [[τ ]] ⊆ [[τ ′ ]] so by definition τ <: τ ′ .
We now recall properties of homomorphisms of regular type expressions. A (partial)
homomorphism h : Type → Type (or h : Type ⇀ Type) is a (partial) function
satisfying
h(()) = ()
h(τ, τ ′ ) = h(τ ), h(τ ′ )
h(τ |τ ′ ) = h(τ )|h(τ ′ )
h(τ ∗ ) = h(τ )∗
h(X) = h(E(X))
In particular, we consider (partial) homomorphisms that are generated entirely by their
behavior on atoms, that is, given a (partial) function k : Atom → Type, we construct
the unique (partial) homomorphism k̂ agreeing with k by taking k̂(α) = k(α) (when
defined) and using the above equations in all other cases.
We say that a (partial) function F : X ⇀ Y on ordered sets X, Y is downward
closed if whenever x′ ≤X x, and F (x) exists, then F (x′ ) also exists; a downward
closed function is downward monotonic if in addition F (x′ ) ≤Y F (x).
In the following, we use the notation F [−] : P(X) ⇀ P(Y ) for the partial function
on sets obtained by lifting F : X ⇀ Y ; F [S] is defined and equals {F (s) | s ∈ S}
provided F is defined on each element of S. It is easy to show that this operation is
downward monotonic with respect to set inclusion and preserves totality (if F is total
then F [−] is total also).
17

We need a second auxiliary function, namely the set of atoms appearing in a type.
This is given by A : Type → P(Atom), defined as follows:
A(()) = {}
A(α) = {α′ | α′ <: α}
A(τ, τ ′ ) = A(τ ) ∪ A(τ ′ )
A(τ |τ ′ ) = A(τ ) ∪ A(τ ′ )
A(τ ∗ ) = A(τ )
A(X) = A(E(X))
The following fact about A will be needed:
Lemma 9. If τ <: τ ′ then A(τ ) ⊆ A(τ ′ ).
S
Proof. Note that A(τ ) = B[L(τ )] where B : Atom ∗ → P(Atom) is defined by
B(()) = {}
B(αω) = {α′ | α′ <: α} ∪ B(ω)

S
and : P(P(Atom))
→ P(Atom) is the usual flattening operator on sets. All three
S
functions , B[−], L are monotonic.
Lemma 10. Let h : Atom ⇀ Type be given. If h(α) is defined for each α ∈ A(τ )
then ĥ(τ ) is defined.

Proof. By structural induction on τ . The base case τ = α is by definition of ĥ(α) =
h(α). The remaining cases are straightforward because ĥ is a homomorphism.
Lemma 11. If h : Atom ⇀ Type is downward closed, and ĥ(τ ) is defined, then h(α)
is defined for every α ∈ A(τ ).
Proof. By structural induction on τ . For the base case τ = α, we need downward
closedness to conclude that h(α) is defined for each α′ <: α. The remaining cases are
straightforward because ĥ is a homomorphism.
Lemma 12. If h : Atom ⇀ Type is downward closed, then ĥ is downward closed.
Proof. Let τ ′ <: τ be given such that ĥ(τ ) is defined. Then by Lemma 11, h(α) is
defined on every α ∈ A(τ ). But A(τ ′ ) ⊆ A(τ ) (Lemma 9) so by Lemma 10, ĥ(τ ′ ) is
defined.
Lemma 13. Suppose h : Atom ⇀ Type is downward monotonic. Then for any τ ∈
dom(ĥ),
[
L[ĥ[L(τ )]] = L(ĥ(τ ))
(1)
Proof. By induction on the structure of τ .
18

– τ = (). Then
[
[
[
[
L[ĥ[L(())]] =
L[ĥ[{()}]] =
L[{ĥ(())}] =
L[{()}]
[
= {L(())} = L(()) = L(ĥ(()))
S
– τ = α. We need to show that L[h[L(α)]] = L(h(α)).
[
[
L[h[L(α)]] =
L[h[{α′ | α′ <: α}]]
[
=
L[{h(α′ ) | α′ <: α}]
[
= {L(h(α′ )) | α′ <: α}
′
Now since h is downward monotonic and defined on α,
S for each′ α <:′ α we have
′
′
that h(α ) <: h(α). Thus, L(h(α )) ⊆ L(h(α)), so {L(h(α )) | α <: α} =
L(h(α)), as desired.
– τ = τ1 , τ2 . Then
[
[
[
L[ĥ[L(τ1 , τ2 )]] =
L[ĥ[L(τ1 ) • L(τ2 )]] =
L[ĥ[L(τ1 )] • ĥ[L(τ2 )]]
[
 [

[
=
L[ĥ[L(τ1 )]] • L[ĥ[L(τ2 )]] =
L[ĥ[L(τ1 )]] •
L[ĥ[L(τ2 )]]

= L(ĥ(τ1 )) • L(ĥ(τ2 )) = L(ĥ(τ1 ), ĥ(τ2 )) = L(ĥ(τ1 , τ2 ))

– τ = τ1 |τ2 . Then
[
[
[
L[ĥ[L(τ1 |τ2 )]] =
L[ĥ[L(τ1 ) ∪ L(τ2 )]] =
L[ĥ[L(τ1 )] ∪ ĥ[L(τ2 )]]
[
 [

[
=
L[ĥ[L(τ1 )]] ∪ L[ĥ[L(τ2 )]] =
L[ĥ[L(τ1 )]] ∪
L[ĥ[L(τ2 )]]
= L(ĥ(τ1 )) ∪ L(ĥ(τ2 )) = L(ĥ(τ1 )|ĥ(τ2 )) = L(ĥ(τ1 |τ2 ))

– τ = τ ∗.
[

L[ĥ[L(τ ∗ )]] =

[

L[ĥ[L(τ )∗ ]] =

[

L[ĥ[L(τ1 )]∗ ]
∗
[
[
L[ĥ[L(τ )]]
=
L[ĥ[L(τ1 )]]∗ =

= L(ĥ(τ1 ))∗ = L(ĥ(τ )∗ ) = L(ĥ(τ ∗ ))
– τ = X: Immediate by induction.

Theorem 5. If h : Atom ⇀ Type is downward monotonic, then ĥ is downward monotonic.
Proof. Let τ ′ <: τ be given such that ĥ(τ ) is defined. By Lemma 12, ĥ(τ ′ ) is defined.
We must show that ĥ(τ ′ ) <: ĥ(τ ). Since τ ′ <: τ , by Lemma 8 we have L(τ ′ ) ⊆
S
S
L(τ ). It follows from the monotonicity of , L[−] and ĥ[−] that L[ĥ[L(τ ′ )]] ⊆
S
L[ĥ[L(τ )]]. By Lemma 13, we have that L(ĥ(τ ′ )) ⊆ L(ĥ(τ )), but by Lemma 6 this
implies that ĥ(τ ′ ) <: ĥ(τ ).
19

A.2 Proving algorithmic completeness
The two key properties which ensure that occurrences of the subsumption rule can be
eliminated from derivations are uniqueness of algorithmic types and downward monotonicity of the algorithmic judgments.
Uniqueness, discussed already in proving decidability of the algorithmic judgments
(Lemma 1 and Lemma 4), simply means that if the “inputs” to a judgment are fixed,
then there is at most one “output” type derivable by algorithmic judgments; thus, the
judgments define partial functions. Recall that for fixed x̄, e, n, a, s, we defined:
1.
2.
3.
4.
5.

fn (τ1 ) as the unique τ2 such that τ1 :: n ⇒ τ2 .
ge (Γ ) as the unique τ such that Γ ⊢◮ e : τ (if it exists).
hx̄,e (Γ, τ1 ) as the unique τ2 such that Γ ⊢◮ x̄ in τ1 → e : τ2 (if it exists).
ja,s (Γ, τ1 ) as the unique τ2 such that Γ ⊢◮a {τ1 } s {τ2 } (if it exists).
ks (Γ, τ1 ) as the unique τ2 such that Γ ⊢◮iter {τ1 } s {τ2 } (if it exists).

Downward monotonicity of the type judgments corresponds precisely to downward
monotonicity of the above functions (where we use the subtyping order on context arguments Γ defined in Section 3.1.) To prove downward monotonicity of the type-directed
f, h, k, we need to make use of the characterization of downward monotonicity for
partial homomorphic extensions established in the last section.
Proposition 1 (Downward Monotonicity).
1. For every n, the function fn is downward monotonic.
2. For every e and x̄, the functions ge and hx̄,e are downward monotonic, and hx̄,e (Γ, −)
is the partial homomorphic extension of ge (Γ, x̄:(−)).
3. For every s and a, the functions ja,s and ks are downward monotonic, and ks (Γ, −)
is the partial homomorphic extension of j1,s (Γ, −).
Proof. For part (1), we just need to show that fn is generated by the function

n[τ ] α = n[τ ]
α 7→
() otherwise
which is obviously downward monotonic.
For part (2), proof is by induction on the structure of e. For each e, we first show
downward monotonicity of ge by inspecting derivations. We show a few representative
examples:
– Case (var): If the derivation is of the form
x̂:τ ∈ Γ
Γ ⊢◮ x̂ : τ
then we have x̂ : τ ′ ∈ Γ ′ where τ ′ <: τ , hence may derive:
x̂:τ ′ ∈ Γ ′
Γ ⊢◮ x̂ : τ ′
20

– Case (let): If the derivation is of the form
Γ ⊢◮ e1 : τ1 Γ, x:τ1 ⊢◮ e2 : τ2
Γ ⊢◮ let x = e1 in e2 : τ2
then by induction we have Γ ′ ⊢◮ e1 : τ1′ for some τ1′ <: τ1 and since Γ ′ <: Γ ,
we have Γ ′ , x:τ1′ <: Γ, x:τ1 , so also by induction Γ ′ , x:τ1′ ⊢◮ e2 : τ2′ for some
τ2′ <: τ2 . To conclude, we derive
Γ ′ ⊢◮ e1 : τ1′ Γ ′ , x:τ1′ ⊢◮ e2 : τ2′
Γ ′ ⊢◮ let x = e1 in e2 : τ2′
– Case (for): If the derivation is of the form
Γ ⊢◮ e1 : τ1 Γ ⊢◮ x̄ in τ1 → e2 : τ2
Γ ⊢◮ for x ∈ e1 return e2 : τ2
then by induction we have Γ ′ ⊢◮ e1 : τ1′ for some τ1′ <: τ1 . Using the downward
monotonicity of hx̄,e2 , we can obtain τ2′ <: τ2 such that Γ ⊢◮ x̄ in τ1′ → e2 : τ2′ .
To conclude, we derive
Γ ′ ⊢◮ e1 : τ1′ Γ ′ ⊢◮ x̄ in τ1′ → e2 : τ2′
Γ ′ ⊢◮ for x ∈ e1 return e2 : τ2′
Showing that hx̄,e is downward monotonic is immediate once we show that hx̄,e (Γ, −)
is the partial homomorphic extension of ge (Γ, x̄:(−)) for any Γ . The latter property can
be proved by induction on the structure of derivations of Γ ⊢ x̄ in τ1 → e : τ2 . The
cases involving regular expression constructs or variables are straightforward, and the
base case
Γ, x̄:α ⊢ e : τ
Γ ⊢ x̄ in α → e : τ
is also straightforward since hx̄,e (Γ, τ ) = ge (Γ, x̄:τ ) by definition.
Similarly, for part (3), j and k, the proof is by induction on derivations. The cases
involving j are straightforward; the case involving ⊢iter is similar to that for for above.
To show ks (Γ, −) is the partial homomorphic extension of j1,s (Γ, −) and hence that ks
is downward monotonic, the proof is by simultaneous induction on derivations, just as
for g and h above.
By rewriting the above proposition in terms of judgments, we can conclude:
Theorem 6 (Downward monotonicity).
1. If τ1 :: n ⇒ τ2 and τ1′ <: τ1 then τ1′ :: n ⇒ τ2′ for some τ2′ <: τ2
2. If Γ ⊢◮ e : τ and Γ ′ <: Γ then Γ ′ ⊢◮ e : τ ′ for some τ ′ <: τ .
3. If Γ ⊢◮ x̄ in τ1 → e : τ2 and Γ ′ <: Γ and τ1′ <: τ1 then Γ ′ ⊢◮ x̄ in τ1′ → e : τ2′
for some τ2′ <: τ2 .
4. If Γ ⊢◮a {τ1 } s {τ2 } and Γ ′ <: Γ and τ1′ <: τ1 then Γ ′ ⊢◮a {τ1′ } s {τ2′ } for some
τ2′ <: τ2 .
21

5. If Γ ⊢◮iter {τ1 } s {τ2 } and Γ ′ <: Γ and τ1′ <: τ1 then Γ ′ ⊢◮iter {τ1′ } s {τ2′ } for
some τ2′ <: τ2 .
Finally, taking Γ = Γ ′ and τ1 = τ1′ in parts 2–5 above, we conclude:
Theorem 7 (Algorithmic completeness).
1.
2.
3.
4.

If Γ
If Γ
If Γ
If Γ

⊢ e : τ then there exists τ ′ <: τ such that Γ ⊢◮ e : τ ′ .
⊢ x̄ in τ1 → e : τ2 then there exists τ2′ <: τ2 such that Γ ⊢◮ x̄ in τ1 → e : τ2′ .
⊢a {τ1 } s {τ2 } then there exists τ2′ <: τ2 such that Γ ⊢◮a {τ1 } s {τ2′ }
⊢iter {τ1 } s {τ2 } then there exists τ2′ <: τ2 such that Γ ⊢◮iter {τ1 } s {τ2′ }

22

