Expressive Power of Unary Counters

Michael Benedikt^{1} H. Jerome Keisler^{2}

1 Bell Laboratories, 1000 East Warrenville Rd., Naperville, IL 60566, USA, Email:

                          benedikt@bell-labs.com

2 University of Wisconsin, Madison Wisconsin 50375, Email: keisler@math.wisc.edu

Abstract. We compare the expressive power on finite models of two extensions of first order logic L with equality. L(Ct) is formed by adding an operator count{x : φ}, which builds a term of sort N that counts the number of elements of the finite model satisfying a formula φ. Our main result shows that the stronger operator count{t(x) : φ}, where t(x) is a term of sort N, cannot be expressed in L(Ct). That is, being able to count elements does not allow one to count terms. This paper also continues our interest in new proof techniques in database theory. The proof of the unary counter combines a number of modeltheoretic techniques that give powerful tools for expressivity bounds: in particular, we discuss here the use of indiscernibles, the Paris-Harrington form of Ramsey’s theorem, and nonstandard models of arithmetic.

1 Introduction

Most database query languages are based on some version of first-order logic. However, practical query languages such as SQL generally supplement their pure first-order component with certain primitives, among them the ability to count over the database. An active line of research in database theory has been to model the impact of counting on a database language by studying extensions of first-order logic by counting quantifiers [18] [12]. The goal is to characterize the expressive power of various counting languages, and to identify those with and without good analytical and computational properties.

In [18] logics with n-ary counters F O + C^{n} are introduced. A method of proving upper bounds on the complexity of these languages is introduced, relying on an Ehrenfeucht-Fraisse game construction for counting (see also [19]). This technique is used to prove a hierarchy theorem for this sequence of logics, in the case of unnested counters.

Ehrenfeucht-Fraisse games are also exploited in [11] and [12] to get complexity bounds for languages allowing counting quantifiers of the form ∃i.

As opposed to the works cited above, we will consider languages with counting constructs that can interact with arbitrary expressions over the integers. We shall consider three extensions of first order logic formed by adding termbuilding operators which count the number of elements satisfying a formula. The smallest of these is a first-order logic with unary counters, like the language F O + C^{1} considered in [18], but with arbitrary integer predicates applicable to the counters. This language is more similar in spirit to the rich two-sorted languages considered in [15] then to the more restricted ones of [12] and [11]. Although this language is extremely large, we will show some interesting limits on its expressive power by displaying two counting languages with more expressive power. In particular, we will show that it is impossible to count the number of equivalence classes of a binary relation in the language of unary counters, and it is impossible to count the number of connected components of a graph. Our results also serve to show that the ability to count the number of elements satisfying a property does not suffice to count the number of terms.

In the process, we will introduce modifications to the Ehrenfeucht-Fraisse argument that we believe are interesting in its own right. We will make use of two model-theoretic techniques: nonstandard universes and indiscernibles. Indiscernibles and nonstandard models have shown up either implicitly or explicitly in several recent works in database theory [31] [5]. These techniques were recently used to settle a number of other problems concerning the expressive power of query languages [4], and we believe they can be used to simplify the bookkeeping involved in many Ehrenfeucht-Fraisse arguments. We believe these techniques can be particularly helpful for proving expressivity bounds for languages involving aggregates.

As mentioned before, one of the principle reasons for studying the expressive power of query languages is to give insight into the design of languages with desirable properties. At the end of this paper we will apply our main theorem to show that a particular desirable property—the weakest precondition property— fails for a natural database language with unary counters.

Organization: The first section gives the definition of the languages we will deal with in this paper. Section 3 describes the nonstandard framework we use to analyze expressivity of queries, and gives some introductory examples of its usefulness. Section 4 outlines the proof of the main result. Section 5 gives a version of this result for a language similar to the tuple relational calculus with range-restriction, and gives an application of these results to the weakest precondition problem for this language.

2 Preliminaries

We give the notation for first-order logic and several counting languages.

Let L be a first-order language with equality and finitely many relation, function and constant symbols. Let 𝕌 be an infinite set. When we talk about finite L-structures, we will mean structures whose domain is a finite subset of 𝕌. Let Λ be a countable set of relations and functions on the set N of natural numbers which contains at least equality and a constant for each n ∈ N, and remains fixed throughout our discussion.

Our first extension of L, denoted by L(Ct), adds to L the term building operator

count{x : φ(x, …)}

which bounds the variable x, and has a symbol for every element of Λ. The models for L(Ct) are finite structures A = ⟨A, …⟩ with vocabulary L, and the count operator is interpreted in A as the cardinality of the set of all elements x ∈ A which satisfy the formula φ in A. Similarly, the term

τ(y) = count{x : φ(x, y)}

defines a function that for each y returns the cardinality of elements in A satisfying φ(x, y)

More precisely, the language L(Ct) has terms of the two sorts U and N. The terms of sort U are the same as for first order logic; in particular, the variables are of sort U. L(Ct) has the usual first order rules for building formulas, and two additional rules:

– For each formula φ and variable x, count{x : φ} is a term of sort N.

– If t_{1}, …, t_{n} are terms of sort N, then f(t_{1}, …, t_{n}) is a term of sort N for each n-ary function f ∈ Λ, and r(t_{1}, …, t_{n}) is a formula for each n-ary relation r ∈ Λ.

Our second extension of L, denoted by L(T m), adds to L(Ct) the more general term-building operator

count{t(x, …) : φ(x, …)}

where φ is a formula and t(x, …) is a term of sort N. In a model A, it counts the number of distinct values of t(x, …) such that x satisfies φ in A. Thus we always have

count{t(x, …) : φ(x, …)} ≤ count{x : φ(x, …)}.

Our third extension, L(Ct, N), adds to L(Ct) variables of sort N and quantifiers over variables of sort N. The language L(Ct, N) was considered in [18]. The main object of study in that paper was a language like L(Ct, N) which had counts over n-tuples of variables of sort U, but did not allow nesting of counts.

In this paper we shall show that L(T m) and L(Ct, N) are proper extensions of L(Ct).

We remark that quantifiers of sort U can be eliminated from each of the languages L(Ct), L(T m), and L(Ct, N). An existential quantifier can be eliminated by replacing a formula ∃xφ(x, …) by ¬count{x : φ(x, …)} = 0.

In a vocabulary L with function symbols, one might also consider the term builder

count{s(x, …) : φ(x, …)}

where the term s is of sort U. This term builder is already definable in L(Ct), because the equation

count{s(x, …) : φ(x, …)} = count{z : ∃x(z = s(x, …) ∧ φ(x, …))}

holds in all finite models.

3 Model-theoretic techniques and expressive bounds

We discuss here some model-theoretic techniques that are helpful for giving expressive bounds, and which will be used in the main result of Section 4.

3.1 Nonstandard Models

The work in [4] made use of nonstandard models and indiscernibles as techniques for analyzing expressivity bounds. In this paper we will discuss these techniques in more detail.

The naive approach to showing that a property Q is not expressible in some language L is to get two models that agree on all sentences of L, but disagree on Q. The problem immediately encountered in applying this technique in finitemodel theory is the following: Any two finite models which satisfy the same sentences of a first order language L are isomorphic, and thus satisfy the same sentences of any reasonable logic, including L(Ct), L(T m), and L(Ct, N). The standard technique for circumventing this problem is via Ehrenfeucht-Fraisse games ([10], [9]). One decomposes the sentences of the logic into countably many fragments L_{n}, and then constructs for each n two finite models M_{n} and N_{n} agreeing on fragment L_{n} but disagreeing on Q.

Here, we give an alternative to this construction. Inexpressibility bounds are obtained by constructing two hyperfinite (meaning, informally for now, “infinitely large finite”) models M and N agreeing on all queries in L, but disagreeing on Q. The first virtue of this technique is as a way of abstracting away from the bookkeeping involved in Ehrenfeucht-Fraisse constructions. For example, if one is interested in showing the inexpressibility of connectivity within pure first-order logic, one need only look at the two hyperfinite graphs G_{1} and G_{2}, where G_{1} is a single hyperfinite cycle, while G_{2} is the union of two hyperfinite cycles. A single game argument shows these two to be elementarily equivalent in first-order logic, but only one is connected, hence connectivity is not first-order definable.

The above example may appear to make the technique of nonstandard models useful more as a convenience than as an essential tool. However, the technique becomes particularly useful when dealing with expressivity results for higherorder logics. We will defer a more detailed discussion of the use of nonstandard models in higher-order languages to the full paper. The use of nonstandard universes (as opposed to elementary extensions) allows one to work with hyperfinite extensions of traditional aggregates constructs such as Counts, Sums, and set formers. For example, consider the query Q over complex objects (see [6],[30], [23], [21]) asking whether a given set of sets A contains two sets of differing parity. One can show this query to be inexpressible in the nested relational algebra [23], a higher-order analog of the relational algebra, by considering a natural counterexample: two hyperfinite structures S_{1} and S_{2}, the first consisting of two hyperfinite sets of differing parity, the second consisting of two hyperfinite sets of the same parity. This argument can be formalized in a straightforward way using the definitions below, and can be easily generalized to higher-order queries.

Arguments such as this are difficult to formalize using the ‘flat’ ultraproduct or elementary extension constructions. On the other hand, direct constructions using ultraproducts, when available, are often more concrete and more accessible in terms of exposition than the use of a nonstandard universe(compare, for example [4] and [29]).

In the previous paragraph, we spoke informally of hyperfinite structures. We now give some formal definitions, following the exposition in [4]:

For any set S, the superstructure V (S) over S is defined as V (S) = ⋃_{n<ω} V_{n}(S) where V_{1}(S) = S, and V_{n+1}(S) = V_{n}(S) ∪ {X | X ⊂ V_{n}(S)}.

We will work with the structure ⟨V (S), ∈⟩ considered as a structure for the first-order language for the epsilon relation. A bounded-quantifier formula in this language is a formula built up from atomic formulas by the logical connectives and the quantification: ∀X ∈ Y, ∃X ∈ Y, where X and Y are variables.

A nonstandard universe consists of a pair of superstructures V (S) and V (Y) and a mapping ∗ : V (S) → V (Y) which is the identity when restricted to S (i.e. ^{∗}x = x for each x in S) and which satisfies

1. Y = ^{∗}S.

2. (Transfer Principle) For any bounded quantifier formula ϕ(v_{1}, …, v_{n}) and any list a_{1}, …, a_{n} of elements from V (S), ϕ(a_{1}, …, a_{n}) is true in V (S) if and only if ϕ(^{∗}a_{1}, …,^{∗}a_{n}) is true in V (Y).

An element of V (Y) is standard if it is in the image of the ∗-map. An element of V (Y) is internal if it is in the downward transitive closure of the standard sets under ∈. Elements of V (Y) that are not internal are called external. An internal map is a map whose graph is an internal set.

We will assume that our universe also satisfies the following

3. (Countable Saturation Principle) For every standard A, and every countable collection Σ(x, v) of bounded-quantifier formulas, and for every vector c of internal sets, if every finite subset of Σ(x, c/v) is satisfied in V (Y) by some element of A, then Σ(x, c/v) is satisfied by an element of A.

We will often omit the ∗ when convenient: for example, if < is an ordering on a set A, x_{1} and x_{2} are elements of ^{∗}A, then we will write x_{1} < x_{2} rather than x_{1}^{∗}< x_{2}. Similarly, if Q is a query on schema SC, and M is a ^{∗}-database (an element of the set ^{∗}DB , where DB is the set of databases for SC), then we will refer to q(M) rather than ^{∗}q(M).

For our proofs we almost always take the base set S of our superstructure V (S) to be the disjoint union of the domain 𝕌 from which our finite structures are taken and ℕ.

By a ^{∗}-finite set we mean any set in the ^{∗}-image of the collection of finite subsets of some standard set. Equivalently, an internal set B is ^{∗}-finite if there is an internal bijection of B onto an initial segment of ^{∗}ℕ. In particular, we can talk about ^{∗}-finite structures, which will have their underlying domains being contained in the ^{∗}-image of the finite powerset of 𝕌. By the transfer principle, such sets B have a well-defined cardinality, which is a (possibly nonstandard) positive integer, as well as a well-defined parity, sum, etc. By a hyperfinite set, we mean a ^{∗}-finite set whose cardinality is not a standard integer. We similarly talk about hyperfinite structures, orderings etc. to mean those whose cardinality is a nonstandard integer.

We can now talk formally about hyperfinite structures. However, we cannot assume in general that the semantic function for a given logic will agree with the semantics obtained by considering the structure “externally”. However, for first-order logic, we have the following result:

Proposition 1. [4] Let L be a language for which each symbol is internal, and let M be an L-structure such that the domain of M is internal and the interpretation of each symbol in L is internal. Let ϕ(x) be a formula of L that has standard finite cardinality (i.e. number of symbols). Then the internal satisfaction predicate ^{∗}⊧ agrees with the external satisfaction predicate ⊧ on ϕ. That is, if c is a finite sequence of parameters from M, then M ^{∗}⊧ ϕ(c) iff M ⊧ ϕ(c).

Given the above proposition we will not distinguish the two kinds of satisfaction predicates when we are dealing with finitary first-order ϕ’s.

The nonstandard technique is now based on the following simple proposition:

Proposition 2. [4] The following are equivalent for any boolean query Q on finite structures:

– There are two hyperfinite ^{∗} − structures that agree on every query in the first-order language L but disagree on ^{∗}Q

– Q is not expressible in L

Given this proposition, it is easy to formalize the inexpressibility arguments mentioned in the beginning of this section: We can form, for example, a graph consisting of two hyperfinite chains (such a graph exists by transfer plus saturation), and show, by a single Ehrenfeucht game, that this graph , considered as an infinite structure, is elementarily equivalent to any graph consisting of a single hyperfinite cycle. The inexpressibility result now follows from Proposition 2.

3.2 Indiscernibles

Although the use of nonstandard models eliminates the need to construct countably many counterexample models, and relieves some of the combinatorial burden in a game argument, it may still be difficult to reason about elementary equivalence in an arbitrary hyperfinite structure.

To relieve the amount of analysis necessary in analyzing elementary equivalence, we will often want to restrict our attention to models whose algebraic structure is “as simple as possible”. Indiscernibility is a method for capturing the intuition that the domain of our structures should have no unnecessary algebraic dependencies among its elements. This idea is implicit in many of the Ramseytheoretic constructions used in Ehrenfeucht-Fraisse constructions [24],[31].

We now define indiscernibles formally. Let I be any ordered set. A sequence B = ⟨B_{i}⟩_{i∈I}, whose elements come from an infinite L-structure M is indiscernible if for every formula ϕ(x), ϕ is satisfied in M by either every increasing (in the order on I) subsequence of B or by no increasing subsequence of B. Indiscernibles are discussed at length in [8].

Within an indiscernible set, the logical structure of the model reduces to a simple ordering. Indiscernibles were used in algorithms for eliminating constraints from constraint queries in [4] [31] and [24].

An infinite set of indiscernibles need not exist in an arbitrary infinite structure. For example, considering the structure M = ⟨N, +, <⟩, we easily see that there can be no indiscernible set of size bigger than 1! However, it is easy to show, using saturation, that for any infinite structure, there is an infinite set of indiscernibles in the nonstandard extension ^{∗}M: this makes the use of indiscernibles particularly powerful in conjunction with nonstandard methods.

In this work, we will consider the use of indiscernibles in collapsing logics with counting quantifiers to first-order logics. The construction in the next section will give an example of the use of indiscernibles to reduce every formula in the language L(Ct) to a first-order formula. Since several previous expressibility bounds on aggregates make use of some sort of “Count Elimination” [21],[22], we hope to investigate this eliminability phenomenon in more generality in forthcoming work.

4 Nonstandard Models and Unary Counters

Consider the logics L(Ct), L(T m), and L(Ct, N) defined in Section 2. We are interested in investigating the relative expressive powers of these languages, using the techniques mentioned above. In particular, we wish to show that L(Ct) cannot express important properties expressible in L(T m), and L(Ct, N).

Our plan, of course, will be to find two nonstandard models which satisfy the same sentences of L(Ct) but do not satisfy the same sentences of L(T m) or of L(Ct, N).

Our first result will show that the language of unary counters L(Ct) cannot count the number of equivalence classes in an equivalence relation, while L(Ct, N) can express this. We will now fix a particular first-order language L^{0} in what follows.

Definition 1. Let the language L^{0} have one unary predicate symbol S and one binary predicate symbol E. Let θ be the sentence

count{count{y : E(x, y)} : x = x} = count{z : S(z)}

of L^{0}(T m).

If E is an equivalence relation, θ says that the number of distinct sizes of equivalence classes of E is equal to the number of elements of S.

Definition 2. Let θ^{+} be the following sentence of L^{0}(Ct, N):

∀i[∀j(Bit(j, i) ⇔ ∃x count{y : E(x, y)} = j) ⇒ Setcard(i) = count{z : S(z)}],

where i, j are variables of sort N, Bit(j, i) is true exactly when the jth bit of the binary representation of i is set, and Setcard(i) is the cardinality of the set coded by the binary representation of i.

Since our arithmetic permits arbitrary functions on the integers, the predicates Bit and Setcard are certainly expressible. Note that θ^{+} expresses the same property as θ, that is, for every finite model C for L^{0}, C satisfies θ if and only if it satisfies θ^{+}. The sentence θ^{+} does not have nested counts.

We shall prove the following theorem, which shows that neither θ nor θ^{+} is expressible in L^{0}(Ct), so that both L(T m) and L(Ct, N) are proper extensions of L(Ct).

Theorem 1. For every sentence φ of L^{0}(Ct) there is a finite model C in which θ is not equivalent to φ: i.e., the unary counter language cannot express θ.

As mentioned above, our plan will be to find two nonstandard models which satisfy the same sentences of L^{0}(Ct) but do not satisfy the same sentences of L^{0}(T m) or of L^{0}(Ct, N).

We let N be the structure with universe set N and a symbol for +, ×, and every relation and function in the set Λ. For each ^{∗}finite model A for L, each term t and formula φ of L(T m) is interpreted in the natural way, using the functions and relations on the extension ^{∗}N. Terms of sort N are interpreted as functions with values in ^{∗}N.

Our goal is to prove the following.

Theorem 2. There exist ^{∗}finite models A and B which satisfy the same sentences of L^{0}(Ct) such that θ is false in A but true in B.

Given this theorem, the inexpressibility of θ in L^{0}(Ct) now follows from the general results of the previous section.

The proof of this theorem will give a canonical example of the use of indiscernibles and nonstandard universes together. We will first show that a special set of indiscernibles exists, and then make use of them to prove Theorem 2.

We use the usual notation for intervals in ^{∗}N; for example,

(J, K] = {x ∈ ^{∗}N : J < x and x ≤ K}.

By a ^{∗}finite sequence in ^{∗}N we mean an an element of the star-image of the finite sequences in N. By the transfer principle, each ^{∗}finite sequence in ^{∗}N is a function d = ⟨d_{1}, …, d_{H}⟩ from the interval (0, H] into ^{∗}N for some hyperinteger H ∈ ^{∗}N.

Lemma 1. There is a strictly increasing ^{∗}finite sequence d = ⟨d_{1}, …, d_{H}⟩ in ∗N such that 0 < d_{1} < H and d is indiscernible in ^{∗}N; that is, any two finite increasing subsequences of d satisfy the same first order formulas in ^{∗}N.

Corollary 1. H and d_{1} are infinite, and \frac{d_{J}}{d_{J−1}} is infinite for each J ∈ (1, H] (i.e. for each standard integer n, d_{J} > n · d_{J−1}) for each J ∈ (1, H]).

The proofs are in the appendix.

We now define the ^{∗}finite structures A and B for L^{0}.

Definition 3. Let A = ⟨A, E, S⟩ where A = (0, d_{H}], E is the equivalence relation on A with equivalence classes (d_{J−1}, d_{J}], J ∈ (0, H], and S = (0, d_{1}]. Let K = d_{1}, and let B = ⟨B, F, S⟩ where B = (0, d_{K}], F = E ∩ B × B, and S is as before.

Lemma 2. The sentence θ is false in A and true in B .

Proof: by inspection.

Lemma 3. A and B satisfy the same sentences of L^{0}(Ct).

The proof is quite involved, and can be found in the appendix.

5 Applications to weakest preconditions

We now outline a version of the previous results for a language L′ whose concrete syntax is closer to existing database languages. The description we give below is based on the tuple relational calculus with range restriction [1], and on our analysis of the PRL constraint language [16] [17].

We have a signature {R_{1}, …, R_{n}}, and for each i ≤ n a finite set of attribute symbols A_{i}. The arity of R_{i} is the cardinality of A_{i}. For each R_{i} we also fix an infinite set U_{i}. We now define our language L′:

We have variables of sort i for each i ≤ n , and an integer sort. A formula will be built out of atomic formulas of the form:

– x.a = y.b where x and y are variables of the same sort i, and a and b are symbols in A_{i}, or of the form

– P (τ_{1}, …, τ_{n}), where P is an integer predicate and the τ_{j} are terms of type integer.

Formulae are built up by the logical connectives and quantifications:

– ∀x ∈ R_{i} ϕ(x)

– ∃x ∈ R_{i} ϕ(x), where x has sort i

Terms are built up via composition from atomic terms, which are of one of the forms:

1. f(x), where f is a symbol for some function from tuples of integers to integers,and x is a tuple of variables of integer sort. The corresponding language L′(Ct) adds the ability to form terms from formulas via the rule:

2. Count{x ∈ R_{i} : ϕ(x)}, where x has sort i and ϕ is a formula.

The language L′(T m) further supplements this by permitting

3. Count{τ(x) : x ∈ R_{i} ∧ ϕ(x)} where τ is a term.

A structure for L′ consists of an assignment to each relational variable R_{i} of a finite collection of elements of the set of functions U_{i}^{A_{i}} (i.e. tuples). Satisfaction relative to an assignment of variables is defined exactly as in the language L(Ct) above.

Let our signature have two relations R and S, and let R have attributes a and b, while S has attributes c and d . Then we have that:

Theorem 3. The L′(T m) sentence θ′ given by count{x.a : x ∈ R ∧ x = x} = count{z ∈ S : z = z} is not expressible in L′(Ct).

The proof is found in the appendix.

5.1 Preconditions and Definable transactions

Let L be any of the standard logical languages (first-order logic, infinitary logic, etc.). We let s(L) denote the sentences of L. We will talk about a database (that is, a finite structure as in the previous section) satisfying a sentence or open formula of L: we mean this in the usual sense. By a transaction on databases, we mean simply any function mapping databases to databases. In the following discussion, we will let D range over databases for a particular signature, and T denote the set of database transactions for this signature. We let T ERM(L) denotes the set of terms of L and for Γ a collection of terms and D a database, we let Γ (D) denote all elements obtained from applying terms in Γ to elements in the underlying set of D. That is:

Γ (D) = {τ(y) : y ⊂ D and τ ∈ Γ }

We now discuss two classes of transactions on finite models associated with L. The definitions are taken from [3].

The class WPC(L) (transactions with weakest preconditions with respect to L) is defined as

{T ∈ T | ∃ recursive f_{T} : s(L) → s(L) s.t.
∀D ∀α ∈ s(L) : T (D) ⊧ α ⇔ D ⊧ f_{T} (α)}

A transaction T has weakest preconditions for L if we can statically determine whether the database resulting from T will satisfy a constraint in L.

The set of L-definable transactions is the collection

DEF(L) = {T | ∀R ∃ L formula β_{R}(x)
∃ Γ ⊂ T ERM(L) such that
∀D : ∀t ⊂ Γ (D) D ⊧ β_{R}(t) ⇔ T (D) ⊧ R(t)}

The class of definable transactions are those that can be expressed using a finite set of L terms and L formulae.

In [3] it is observed that for first-order languages, we have containment, DEF(L) ⊂ WPC(L). That is, definable transactions all admit weakest preconditions. This is a desirable closure property for a query language to possess. [3] investigates weakest preconditions over a number of logics, and over a number of transaction languages. In [17],[3], and [16] applications of weakest precondition closure to database integrity maintenance are discussed.

Given the importance of weakest precondition closure for database query languages, it is important to see if natural extensions of the relational calculus, such as L′(Ct), posess this closure property. It follows from the main result of this paper that containment does NOT hold for the language L′(Ct).

Corollary 2. There are L′(Ct)-definable transactions that do not posess weakest preconditions over L′(Ct).

The proof of the corollary is in the appendix.

6 Conclusions and future work

Languages with aggregate constructs are not nearly so well understood as the relational calculus. In particular, issues of optimization, complexity, safety, and expressiveness remain open for many models of aggregation. We are interested in developing a usable set of rewrite-rules for simplifying languages such as L(Ct) and L(T m), and getting semantic characterizations of the definable transactions that are available (along the lines of Gaifman’s locality theorem [13] or the bounded degree property of [21]).

We are interested in studying the relationship of the language L(T m) to various other counting languages (those discussed, for example, in [18]). In particular, it would be helpful to know whether languages with binary counters can express all sentences of L(T m), and similarly for n-ary counters.

Techniques for proving expressiveness bounds on query languages are hard to come by. We’ve presented here one technique for analyzing expressivity of query languages, based on the use of indiscernibles and nonstandard models, that we believe can be useful outside of the context of aggregates. In particular, we hope to investigate the interaction of these techniques with the use of Ehrenfeucht games for logics with counting [18] [14].

Questions in this work were motivated by considering the closure under weakest preconditions of various extensions of first-order logic. The closure of a specification language under weakest-preconditions of definable transactions is helpful for integrity constraint maintenance [3],[26],[27]. It is therefore important to find logics that include aggregate operators that have this closure property, are of manageable complexity, and allow for optimization and analysis. The results of this paper show that L(Ct) is not closed under weakest-preconditions, and we suspect that the same is true for L(T m). We would like to discover natural weakest-precondition closed logics containing these languages.

References

1. S. Abiteboul, R. Hull and V. Vianu. Foundations of Databases. Addison-Wesley, 1995.

2. J. Barwise (Ed.) Handbook of Mathematical Logic. North-Holland Elsevier 1977.

3. M. Benedikt, T. Griffin, and L. Libkin Verifiable Properties of Database Transactions In Proceedings of 15th ACM Symposium on Principles of Database Systems, pages 117–128, Montreal Canada, June 1996.

4. M. Benedikt, G. Dong, L. Libkin, L. Wong. Relational Expressive Power of Constraint Query Languages. In Proceedings of 15th ACM Symposium on Principles of Database Systems, pages 5–17, Montreal Canada, June 1996.

5. M. Benedikt and L. Libkin. On the Structure of queries in constraint query languages. In Proceedings of 11th IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey 1996.

6. P. Buneman, S. Naqvi, V. Tannen, L. Wong. Principles of programming with complex objects and collection types. Theoretical Computer Science, 149(1):3–48, September 1995.

7. A. Calò and J. Makowsky. The Ehrenfeucht-Fraïssé Games for Transitive Closure Logic. Manuscript, 1991

8. C. C. Chang and H. Jerome Keisler. Model Theory, Third Edition. North-Holland Elsevier 1990.

9. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer Verlag, 1995.

10. A. Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamentae Mathematicae, 49:129–141, 1961.

11. K. Etessami. Counting Quantifiers, Successor Relations, and Logarithmic Space. In Proceedings of 10th IEEE Conference on Structure in Complexity Theory, May 1995, pages 2–11.

12. K. Etassami and N. Immerman. Tree Canonization and Transitive Closure. Tenth Annual IEEE Symposium on Logic in Computer Science. 1995.

13. H. Gaifman. On local and nonlocal properties. In J. Stern, editor, Logic Colloquium ’81, pages 105–135. North -Holland, 1982.

14. Gradel, E. and Otto, M. Inductive Definability with Counting on Finite Structures. In E. Borger (ed.), Computer Science Logic,Selected Papers from CSL ’92 LNCS 702 Springer (1993), 231-247.

15. Erich Gradel and Yuri Gurevich. Metafinite Model Theory In Logic and Computational Complexity, International Workshop LCC’94 Indianapolis, IN,313-366.

16. T. Griffin and H. Trickey. Integrity Maintenance in a Telecommunications Switch. In IEEE Data Engineering Bulletin V. 17, No. 2., June 1994

17. T. Griffin, H. Trickey, and C. Tuckey. Update Constraints for Relational Databases. Technical Memorandum AT&T Bell Laboratories, 1992

18. S. Grumbach and C. Tollu. On the Expressive Power of Counting. Fourth International Conference on Database Theory. 1992.

19. N. Immerman and E.S. Lander. Describing graphs: a first-order approach to graph canonization. In A. Selman, editor, Complexity Theory Retrospective, pages 59-81. Springer-Verlag, 1990.

20. C. Karp. Finite Quantifier Equivalence. In The Theory of Models, edited by J. Addison, L. Henkin, and A. Tarski, North-Holland 1965, 407-412.

21. L. Libkin and L. Wong. New techniques for studying set languages, bag languages and aggregate functions. In Proceedings of the 13th Conference on Principles of Database Systems, Minneapolis MN, May 1994, pages 155–166.

22. L. Libkin and L. Wong. On representation and querying incomplete information in databases with bags Information Processing Letters 56 (1995) 209-214

23. G. Ozsoyoglu, Z. M. Ozsoyoglu, V. Matos. Extending relational algebra and relational calculus with set-valued attributes and aggregate functions, ACM Transactions on Database Systems 12, No. 4 (1987), 566–592.

24. J. Paredaens, J. Van den Bussche, and D. Van Gucht. First-order queries on finite structures over the reals. In Proceedings of 10th IEEE Symposium on Logic in Computer Science, San Diego, California, pages 79–87, 1995.

25. J. Paredaens and D. Van Gucht. Converting nested relational algebra expressions into flat algebra expressions. ACM Transaction on Database Systems, 17(1):65–93, March 1992.

26. X. Qian. An effective method for integrity constraint simplification. In Fourth International Conference on Data Engineering, 1988.

27. X. Qian. The Deductive Synthesis of Database Transactions. PhD thesis, Stanford University, 1989.

28. N. Rescher Plurality quantification. Journal of Symbolic Logic, vol. 27 (1962) 373-374.

29. O.Belagradek, A. Stolboushkin, M. Tsaitlin. On order-generic queries. Manuscript. To appear.

30. V. Tannen, Tutorial: Languages for collection types, in “Proceedings of 13th Symposium on Principles of Database Systems,” Minneapolis, May 1994.

31. J. Van Den Bussche and M. Otto. First-order queries on databases embedded in an infinite. structure Technical Report, University of Antwerp, October 1995.

32. L. Wong. Normal forms and conservative properties for query languages over collection types. in “Proceedings of 12th ACM Symposium on Principles of Database Systems,” Washington D. C., May 1993.

APPENDIX

Proofs

We will prove the remaining lemmas used to prove Theorem 2.

Hereafter we let d = ⟨d_{1}, …, d_{H}⟩ be as in Lemma 1, and put d_{0} = 0.

A Proof of corollary 1

By indiscernibility, d_{1} is infinite, and thus H is infinite. Since d is strictly increasing and d_{1} < H, we have 2d_{1} ≤ d_{H}. By indiscernibility, 2d_{J−1} ≤ d_{J} for each J ∈ (1, H], and by indiscernibility again, 2^{n}d_{J−1} ≤ d_{J} for each J and each finite n. □

B Proof of lemma 3

We have count{x : S(x)} = d_{1} in both A and B. In A,

count{count{y : E(x, y)} : x = x} = H > d_{1},

so θ fails in A. In B,

count{count{y : E(x, y)} : x = x} = d_{1},

so θ holds in B. □

It remains to show that A and B satisfy the same sentences of L^{0}(Ct). In order to do this we introduce an auxiliary first order vocabulary L^{1} and corresponding models A^{1} and B^{1}.

Definition 4. Let f : A → (0, H] be the function such that f(x) = J whenever J ∈ (0, H] and x ∈ (d_{J−1}, d_{J}]. Let L^{1} be a first order vocabulary with countably many unary relations min_{n}(x), max_{n}(x) for n ∈ N and countably many binary relations x ⪯_{n} y for n ∈ N. Let A^{1} be the model for L^{1} with universe A such that

– A^{1} ⊧ min_{n}(x) iff f(x) ≤ n,

– A^{1} ⊧ max_{n}(x) iff H − n ≤ f(x),

– A^{1} ⊧ x ⪯_{n} y iff f(x) + n ≤ f(y).

Let B^{1} be the model for L^{1} with universe B such that

– B^{1} ⊧ min_{n}(x) iff f(x) ≤ n,

– B^{1} ⊧ max_{n}(x) iff K − n ≤ f(x), – B^{1} ⊧ x ⪯_{n} y iff f(x) + n ≤ f(y).

Lemma 4. For every formula φ(x) of L^{0}(Ct) there is a formula φ^{1}(x) of L^{1}(Ct) such that for all a in A, A ⊧ φ[a] if and only if A^{1} ⊧ φ^{1}[a], and for all b in B, B ⊧ φ[b] if and only if B^{1} ⊧ φ^{1}[b].

Proof: Put

(x = y)^{1} = (x = y),
E(x, y)^{1} = (x ⪯_{0} y ∧ y ⪯_{0} x),
S(x)^{1} = min_{1}(x).

Then use the formation rules in the obvious way to define φ^{1} for arbitrary φ. □

Definition 5. Let a ≡_{0} b mean that |a| = |b| and (A^{1}, a) and (B^{1}, b) satisfy the same atomic formulas of L^{1}. We use a similar notation for pairs of tuples which are both in A or in B.

Lemma 5. A^{1} and B^{1} satisfy the same sentences of L^{1}. In fact, a ≡_{0} b if and only if (A^{1}, a) and (B^{1}, b) satisfy the same formulas of L^{1}.

Proof: Using the fact that we have ⪯_{n} as an atomic relation in the language for each n, and the fact that A^{1} and B^{1} are countably saturated, we derive that the relation a ≡_{0} b has the back and forth property. It follows that whenever a ≡_{0} b, player ∃ has a winning strategy in the Ehrenfeucht-Fraisse game with ω moves between (A^{1}, a) and (B^{1}, b). In addition, we have that the empty sequences from each model are ≡_{0}-equivalent, since there are no atomic sentences in L^{1}. Thus (A^{1}, a) and (B^{1}, b) are elementarily equivalent by Karp’s theorem in [20]. □

The argument in the above lemma can also be used to show that the complete first order theory of A^{1} and B^{1} admits elimination of quantifiers, but we shall not need that fact.

Lemma 6. Let Γ (x) be a set of quantifier-free formulas of L^{1} maximal consistent with the theory of A^{1} and let ψ(x, y) be a quantifier-free formula in L^{1}. Let s = domain(vecx) ∪ {min, max}. There exist

α_{1}, …, α_{m} ∈ s, β_{1}, …, β_{m} ∈ {−1, 1}, γ_{1}, …, γ_{m} ∈ Z, δ ∈ Z

such that whenever (A^{1}, a) satisfies Γ (x),

count{y : ψ(a, y)} = δ + ∑_{j=1}^{m} β_{j}d_{f(a_{α_{j}})+γ_{j}},  (1)

and whenever (B^{1}, b) satisfies Γ (x),

count{y : ψ(b, y)} = δ + ∑_{j=1}^{m} β_{j}d_{f(b_{α_{j}})+γ_{j}},  (2)

with the convention that f(a_{min}) = f(b_{min}) = 0, f(a_{max}) = H, and f(b_{max}) = K.

Proof: Given Γ (x), any quantifier-free formula ψ(x, y) of L^{1} says that either y belongs to a subset of {x_{i} : i < |x|}, or y ∉ {x_{i} : i < |x|} and f(y) belongs to a finite union of disjoint “intervals” with endpoints at a finite distance from elements of

{f(x_{i}) : i ∈ s}.

In the model (A, a), such an interval will have the form (u + γ, u′ + γ′] where γ, γ′ ∈ Z and u, u′ belong to {f(x_{i}) : i ∈ s}. The number of elements y of A such that f(y) belongs to such an interval is equal to the difference d_{u′+γ′} − d_{u+γ}. A similar computation holds for (B, b). □

We now prove our main lemma, which shows that in the models A^{1} and B^{1} both quantifiers and counts can be eliminated.

Lemma 7. For each formula φ of L^{1}(Ct) there is a quantifier-free formula φ^{1} of L^{1} such that

A^{1} ⊧ φ ⇔ φ^{1}, B^{1} ⊧ φ ⇔ φ^{1}.

Proof: We argue by induction on the complexity of φ. As remarked earlier, we may assume without loss of generality that φ has no quantifiers, because the existential quantifier ∃xψ(x, …) may be replaced by ¬count{x : ψ(x, …)} = 0. The hard case of the induction is the case where φ has the form

r(count{y : ψ_{i}(x, y)} : i ≤ j)

for some j-ary relation r on N. For simplicity we let j = 1, so that

φ = r(count{y : ψ(x, y)}).

By inductive hypothesis we have a quantifier-free formula ψ^{1}(x, y) of L^{1} which is equivalent to ψ in both models.

Claim 1. Suppose a ≡_{0} b. Then (A^{1}, a) ⊧ φ if and only if (B^{1}, b) ⊧ φ. Proof of Claim 1: By the preceding lemma, (A^{1}, a) satisfies equation (1) and

(B^{1}, b) satisfies the corresponding equation (2). The claim now follows by the indiscernibility of the sequence d in ^{∗}N.

Claim 2. There is a quantifier-free formula φ^{1}(x) of L^{1} such that A^{1} ⊧ φ ⇔ φ^{1}.

Proof of Claim 2: Let Σ(x) be the set of all quantifier-free formulas σ(x) of L^{1} such that A^{1} ⊧ φ ⇒ σ. Suppose A^{1} ⊧ Σ[a]. Then the set of formulas

{φ(x)} ∪ {η(x) : η is quantifier-free in L^{1} and A^{1} ⊧ η[a]}

is finitely satisfiable in A^{1}. Since^{∗}N is saturated, this set of formulas is satisfiable in A^{1} by some tuple c. Then A^{1} ⊧ φ[c] and a ≡_{0} c. By Lemma 5 and the saturation of ^{∗}N, there exists b in B such that a ≡_{0} b ≡_{0} c. By Claim 1, (B^{1}, b) ⊧ φ and (A^{1}, a) ⊧ φ. Thus every tuple which satisfies Σ in A^{1} satisfies φ. Since ^{∗}N is saturated, there is a finite conjunction φ^{1}(x) of formulas in Σ(x) such that A^{1} ⊧ φ ⇔ φ^{1}, and the claim is proved.

Now let b be a tuple in B. By Lemma 5 and the saturation of ^{∗}N, there exists a in A such that a ≡_{0} b. By Claim 2, A^{1} ⊧ (φ ⇔ φ^{1})[a]. By Claim 1, B^{1} ⊧ (φ ⇔ φ^{1})[b]. □

Corollary 3. A^{1} and B^{1} satisfy the same sentences of L^{1}(Ct). Moreover, A and B satisfy the same sentences of L^{0}(Ct).

This completes the proof of Lemma 3, and hence Theorem 2.

C Proof of Theorem 3

Proof: Fix some bijection K from the universe for tuples of S to the universe of R. Let M be the class of L′ models of the form M′ = ⟨R, S⟩ which satisfy

– the sets {x.a : x ∈ R}, {x.b : x ∈ R}, {x.c : x ∈ S}, are pairwise disjoint.

– x.c = x.d for each x ∈ S

– x.c ≠ y.c for distinct x, y in S.

– For each x in S, K(x.c) is in R

We define a mapping F that maps M to models for the language L^{0} defined previously. F (M′) is defined to have domain equal to R, the predicate S is interpreted by the K-image of the attributes of the relation S in M′ , and the interpretation of the binary predicate E is defined by

xEy ↔ x.a = y.a

We also define a mapping G from formulae and terms of L(Ct) to formulae and terms (respectively) of L′(Ct) as follows:

G(x.a = y.a) = xEy, where x and y are any two variables of sort R, (not necessarily distinct).

G(x.c = y.c) = G(x.d = y.d) = G(x.c = y.d) = G(x.d = y.c) = x = y , where x, y have sort S.

G(x.att1 = y.att2) = false, for all attribute/sort combinations not listed above.

G(P (τ_{1}, …, τ_{n})) = P (G(τ_{1}), …, G(τ_{n}))

G(∀x ∈ R ϕ(x)) = ∀x G(ϕ(x))

G(∃x ∈ R ϕ(x)) = ∃x G(ϕ(x))

G(∀x ∈ S ϕ(x)) = ∀x S(x) ∧ G(ϕ(x))

G(∃x ∈ S ϕ(x)) = ∃x S(x) ∧ G(ϕ(x))

G(f(x)) = f(x),

G(Count{x ∈ R : ϕ(x)}) = Count{x : G(ϕ(x))},

Proposition 3.

– The maps F and G are surjections.

– M′ ⊧ ϕ(x) ⇔ F (M′) ⊧ G(ϕ(x))

Proof: 1) is proved by inspection. 2) is proved by straightforward induction on complexity.

Theorem 3 now follows, since if there were a formula of L′(Ct) expressing exactly those models that satisfy θ′, then by applying the inverse of G to this formula we would get a sentence of L(Ct) expressing exactly those models satisfying θ , contradicting the main theorem of the previous section.

D Proof of Corollary 2

Consider the transaction T on structures for the signature SC defined above as follows:

R ⇐ Π_{a}(R) S ⇐ S Then T is clearly L(Ct)-definable. The precondition of the L′(Ct)-sentence: count{y ∈ R : y = y} = count{z : S(z)} is exactly the sentence θ′ of Theorem 3 cited above, which is not expressible

in L′(Ct).