Re-grouping information in a domain theoretic data model

Hermann Puhlmann Fachbereich Mathematik Technische Hochschule Darmstadt D–64289 Darmstadt Germany puhlmann@mathematik.th-darmstadt.de

October 1995

1 Introduction

The success of relational databases is largely due to the easy and intuitive way of putting queries. One does not destinguish between a database relation and the realworld set which is to be described but identifies the one with the other. In this setting, all operations of nested relational algebra or query languages such as SQL can be interpreted in an ad-hoc manner, and in fact that is what the average user does. One drawback of these database systems however is that they do not allow for structured data types nor for partial information.

An attempt of overcoming this whilst keeping as many advantages from the relational model as possible, in particular that of a sound mathematical foundation, was made by Buneman et al. [BJO91] when they suggested to base a database model on Scott-domains. These are ordered sets in which the ordering can be regarded as an order of information contents. A least element incorporates the idea of an element of no information, and order theoretic properties model ways of combining pieces of consistent information.

The concept of a snack, invented by Buneman and investigated in [Nga92, Puh93, JP95], was a breakthrough towards including set-valued types into the domain theoretic setting. As it allows for repeated application of a set-type constructor, the domain theoretic database model is not only a generalization of the relational model, as initially intended, but also a generalization of nested relational databases. These were introduced in the early 1980s by Schek et al. (a nice overview as well as detailed results are given in [Sch88]) who implemented the model in the “Darmstädter Datenbanksystem”. They also enriched relational algebra by two operations “nest”

(ν) and “unnest” (μ) [JS82] which allow the passage between nested relations of different nesting levels.

While the use of relational algebra for simple queries is straightforward, nested relational algebra appears to be less comprehendable. As argued in [Puh91, Puh95] this is due to the lack of a formal semantics of nested databases, and it becomes evident in the composite application of ν and μ. While μ ∘ ν equals the identity, we do not have this for ν ∘ μ. Though this cannot be expected to be satisfied, one would expect ν ∘ μ to be less than the identity if a suitable information ordering is given.

This paper shows how nested database relations can be represented in the domain theoretic database model and operations nest and unnest can be defined within that model such that unnest ∘ nest = id and nest ∘ unnest ≤ id. We thus get a formal semantics of nested databases as well as operations for nesting and unnesting which keep as much information as possible and therefore build the ideal passage between relations of different nesting levels.

The organisation of the paper is as follows: In Section 1 we give a short introduction to nested relational databases. Section 2 illustrates the domain theoretic approach. In particular, the snack-powerdomain which models set-types is defined, and the interpretation of database relations in the new setting is given. We begin Section 3 with giving an intuitive, picture-oriented account of nested snacks (these will model nested relations). After that we turn to defining nest and unnest and proving the result claimed above. Finally we show how the snack representation of a nested relation behaves under unnest and nest in Section 4.

2 Nested Relational Databases

In [JS82], Jaeschke and Schek dismiss the principle that relational databases must be in so-called first-normal-form, i. e. that the domains connected with the attributes must be sets without any further structure. Jaeschke and Schek rather allow an entry in a database relation to be a relation itself. This construction may be applied in a nested manner, leading to the nested relations database model (see [Sch88]).

While in the standard relational model a relational schema is determined by the set of attribute names of a relation, the nested relations model allows for different types of relations with the same attributes. These types differ in the structure in which attributes are nested to sub-relations, and transformations between them can be performed by the operations ν (nest) and μ (unnest).

In order to explain how these operators work, it suffices to consider two attributes A and B and the transformation between relations of the types {A × B} and {A × {B}}. Here we use {·} for building relations, i. e. {A×B} is the type of a (traditional) relation with the two attributes A and B while in {A × {B}} the second attribute is relation-valued with relations with the single attribute B.

So far “relation” meant “database relation”. We may however think of the “relations” in the mathematical sense as well if we keep in mind that database relations are always finite. In this light, objects of type {A × B} are finite subsets of A × B and objects of type {A × {B}} are finite subsets of the product of A and the set of finite subsets of B. Denoting the projection onto A by π_{A} and writing pairs in angle brackets, the functions ν and μ between these two types are given as follows:

ν : {A × B} → {A × {B}}
ν(R) := {⟨a, b̂⟩ | a ∈ π_{A}(R) and b̂ = {b ∈ B | ⟨a, b⟩ ∈ R}}

and

μ : {A × {B}} → {A × B}
μ(S) := {⟨a, b⟩ | ∃⟨a, b̂⟩ ∈ S. b ∈ b̂} .

The transition ν : {A × B} → {A × {B}} pairs each A-value with the set of B-values associated with it. The operation μ : {A × {B}} → {A × B} reverses this by taking an A-value and the associated set of B-values and producing those pairs which have the A-value in the first component and one of the B-values in the second component. In fact, we always have μ∘ν = id [JS82]. The reverse composition ν ∘μ, however, does not equal the identity. This does not come as a surprise since in a nested relation of type {A × {B}} one a ∈ A may occur together with different sets of B-values. This grouping is not respected by ν ∘ μ as the sample relation R illustrates.

R : A  {B}
a_{1}  \begin{matrix}b_{1} \\ b_{2} \end{matrix}

a_{1}  \begin{matrix}b_{2} \\ b_{3} \end{matrix}
a_{2}  ∅

Applying the unnest operator yields

μ(R) : A  B
a_{1}  b_{1}
a_{1}  b_{2}
a_{1}  b_{3}

It emerges that the information on how a_{1} was linked to subsets of B has vanished. Moreover, the information about a_{2} which was linked to the empty set is gone as well. Neither of this information can be recovered by nesting the relation again:

\begin{aligned}νμ(R) : & A & \{B\} \\ & a_{1} & \begin{matrix}b_{1} \\ b_{2} \\ b_{3} \end{matrix} \end{aligned}

The mere fact that the composition ν ∘ μ does not equal the identity is not worrying. In fact, operations such as the projection are specifically made for losing information and thus do not equal the identity as well. However, we believe that in a setting of relations ordered by their information contents, operations which transform relations should always be below (or equal to) the identity function. This corresponds to the idea that by merely operating on the given data we can never gain information which was not present before.

There are several possibilities of endowing relational databases with an information ordering, for instance one could compare relations with the same scheme by “⊆” or “⊇” (for a discussion of this, see [BJO91]). The different possibilities reflect different ways of thinking about the information contents of a database relation. If, however, we adopt one of these ways, we should use it in a unique fashion for relations on all nesting levels. With this in mind, it seems odd that our sample relation loses lines under the process of unnesting and nesting while the remaining relation on the inner level (sets of B-values) increases. Thus, under no suitable interpretation we will have ν ∘ μ ≤ id. Variants of the operations ν and μ as introduced in [Sch88] do not improve this situation.

The underlying problem is the unclear semantics of nested relations. If we use the domain theoretic approach to a semantics of databases which was suggested by Buneman et. al [BJO91] and if we interpret relations as elements of the snack powerdomain [Puh93, JP95, Puh95] we are much better off. In this case it is possible to define functions nest and unnest with nest ∘ unnest ≤ id and unnest ∘ nest = id. Thus, the two functions form an embedding-projection pair, a connection between objects of different nesting levels which loses as little information as possible.

3 The domain theoretic database model

3.1 Froms sets to domains

The domain theoretic approach to modelling databases was introduced by Buneman et al. [BJO91]. Their idea was to replace unstructured sets by Scott-domains to serve as database domains. Scott-domains are algebraic ordered sets with least element in which every directed subset and every (upward) bounded set has a supremum.^{1} Algebraicity means that every element is the supremum of compact elements. They are those elements which are finitely representable. Hence, Scott-domains allow for calculations with finite representations — an indispensible prerequisite of an implementation of the database model on a computer.

The ordering of a Scott-domain is interpreted as an order of information: The larger elements contain more information, the maximal elements are those of total information whereas non-maximal elements incorporate partially specified objects. These are approximations to those maximal elements which are above them.

1See e. g. [AJ95] for an introduction into domain theory.

Database tuples will then be replaced by compact elements of a domain, allowing us to represent partial information in the database by taking non-maximal elements of the domain.

To provide the reader with a better intuition of the more complicated issues which we deal with later, we will offer pictorial representations of (Scott-)domains in the sequel. As usual, a domain D is drawn as an upside-down triangle. The bottom corner corresponds to the bottom (least) element of the domain, and x ≤ y means that we can reach y from x by somehow going up within the triangle. The maximal elements of the domain thus correspond to the top side of the triangle, and the upper set ↑x generated by one element can be thought of as a little triangle with its top side being part of the top side of the triangle which stands for the domain:

⊥  ↑x x  D y

3.2 Snacks as approximations of sets

By using domains rather than unstructured sets it is possible to work with partial information in a database. However, as the picture stands, we only know how to represent partiality with respect to individual elements. But database relations are sets of such elements, and the spirit of [BJO91] calls for a domain of approximations to sets. To this end, Buneman invented the notion of a snack, and various aspects of the snack-powerdomain were studied in [Nga92, Puh93, JP95, Puh95]. Snacks formalize the idea of approximating sets of maximal elements of a given domain by giving an outer bound and specific information about individual elements. Let us first give the precise definition:

Definition 3.1 A snack on a domain D is a pair (U, L) where U is a compact open subset of D and L is a finite set of nonempty compact open subsets of D such that L ⊆ U for all L ∈ L and L is an antichain w. r. t. subset-inclusion.

Note that the compact open subsets of a domain are exactly those upper sets which are generated by finitely many compact elements of the domain. Because of this, the building blocks of a snack can be represented by a finite amount of information; this is essential if we think of an implementation on a computer.

A typical snack looks like the following:

L_{1}  D  L_{2} U

We think of the set U as an outer bound of the approximated set S, thus S being a subset of U ∩ D_{max}. The sets L ∈ L (in our case L_{1} and L_{2}) specify individual elements of S in the sense that in each L ∈ L there must be an element of S. From this it is clear that L ⊆ U since this element cannot be outside the outer bound U.

With this interpretation in mind the following order relation on snacks is easy to understand:

Definition 3.2 The set of snacks on a domain is ordered by

(U, L) ⊑ (U′, L′)
⟺ U ⊇ U′ and for all L ∈ L there is some L′ ∈ L′ such that L ⊇ L′ .

The definition simply says that in order to get a better approximation one has to shrink the outer bound and each of the sets L which specify individual elements of the approximated set. Note that the introduction of “new” sets L′ ∈ L′ which are not related to the sets L ∈ L is allowed so that one may add information about further elements of the approximated set.

The following picture illustrates the snack-ordering: The snack (U′, {L′_{1}, L′_{2}, L′_{3}}) is better than the previously shown snack (U, {L_{1}, L_{2}}).

L′_{1}  ^{L′_{3}} D ^{L′_{2}}  ^{U′}

In the domain theoretic model, database relations will be replaced by snacks (the next passage will say how), but with this construction we can do more, namely we can include a type-constructor “set of” into the database type system. This is the basis of interpreting nested relations, as we will see later. To lay the foundation of this we cite from [Puh93]:

Definition 3.3 Let D be a domain. The snack powerdomain of D is the ideal completion of the ordered set S(D) of snacks on D.

Theorem 3.4 The snack powerdomain of a Scott-domain is a Scott-domain.

This is fine since it ensures that we do not leave the world of Scott-domains by applying the snack-construction. In the following, however, we do not need to use the ideals of snacks themselves. We take advantage of the fact that an algebraic domain is completely determined by its compact elements. Hence we can stick to the ordered set of snacks S(D) to do all relevant calculations.

3.3 Interpreting database relations

Just as database tuples are replaced by elements of a domain, we now replace database relations by snacks on the ground domain. There is a standard interpretation of database relations in this new setting, such that we can regard the domain theoretic database model as an extension to the relational model.

For this, database relations are interpreted as being the sets which are to be approximated, i. e. they are considered as totally specified. The set of potential entries of a relation R is enriched with a bottem element, yielding a flat domain. If R consists of the tuples a_{1}, …, a_{n} then we identify R with the snack ({a_{1}, …, a_{n}}, {{a_{1}}, …, {a_{n}}}). The only set S which is approximated by this snack is R itself, since S must be a subset of R = {a_{1}, …, a_{n}} and each of the elements a_{1}, …, a_{n} must be in S.

3.4 Interpreting nested relations

In order to interpret nested relations within the domain theoretic database model we can restrict ourselves to the two type-constructors “product” (×) and “set of” ({·}).^{2} On the domain theoretic side these constructors are interpreted as cartesian product resp. the snack powerdomain. As the category of Scott domains is closed under both constructions, we do not leave the scope of our model by these means.

With × and {·} we are able to build the types of nested relations. For this exposition we restrict ourselves to relations with two attributes A and B. The flat relation with both attributes will have entries out of A × B, and in the domain theoretic model, the relation is a snack on A × B, i. e. an element of S(A × B). The nested relation with B-nests is of type {A × {B}} i. e. an approximation of a set whose elements are pairs, consisting of an element of A and an approximation of a subset of B. In case we start with a (traditional) nested relation where we take all sets which occur as totally specified sets, we may wish to omit the word “approximation”. This is reflected by the fact that the snack representation of these relations will be maximal in the associated powerdomain. This representation is gained by applying the construction which we gave above in a nested manner. We illustrate this by the sample relation from Section 2:

2A richer type system is discussed in [JP95].

R : A  {B}
a_{1}  \begin{matrix}b_{1} \\ b_{2} \end{matrix}

a_{1}  \begin{matrix}b_{2} \\ b_{3} \end{matrix}
a_{2}  ∅

At first, we give the snacks that correspond to the sets of B-values:

subset of B corresponding snack
{b_{1}, b_{2}}  ({b_{1}, b_{2}}, {{b_{1}}, {b_{2}}})
{b_{2}, b_{3}}  ({b_{2}, b_{3}}, {{b_{2}}, {b_{3}}})
∅  (∅, ∅)

These snacks are now paired with the respective A-values. Out of the resulting pairs we then build the snack that corresponds to the nested relation. Its U-part is

{⟨a_{1}, ({b_{1}, b_{2}}, {{b_{1}}, {b_{2}}})⟩, ⟨a_{1}, ({b_{2}, b_{3}}, {{b_{2}}, {b_{3}}})⟩, ⟨a_{2}, (∅, ∅)⟩} .

For the L-part we have to make a set L ∈ L out of each of these pairs. Hence, the L-part is

{{⟨a_{1}, ({b_{1}, b_{2}}, {{b_{1}}, {b_{2}}})⟩}, {⟨a_{1}, ({b_{2}, b_{3}}, {{b_{2}}, {b_{3}}})⟩}, {⟨a_{2}, (∅, ∅)⟩}}.

We also give the definition for the general case:

Definition 3.5 The snack representation O^{S} of an object O (i. e. a tuple or relation) of a nested relational database is recursively defined as follows:

• If O is a relation R then R^{S} := ({r^{S} | r ∈ R}, {{r^{S}} | r ∈ R}),

• if O is a tuple t = ⟨t_{1}, …, t_{n}⟩ then t^{S} := ⟨t_{1}^{S}, …, t_{n}^{S}⟩,

• if O is an element g of a database ground domain, then g^{S} := g.

4 Nesting and unnesting snacks

4.1 Understanding nested snacks

In the previous section we saw how nested relations are represented in the domain theoretic model. We used snacks for the construction of set-valued types and got representations of nested relations as maximal elements in the snack-powerdomain. We now turn from maximal to arbitrary elements in the snack-powerdomain. They incorporate database entries of partial information. The aim of the following is to give an intuitive account of the quite involved structures which occur.

First of all, we do the step from the triangle picture for a single domain to a picture of the product of two domains A and B. This is given by an upside-down four-sided pyramid. The base of the pyramid comes on top and corresponds to the maximal elements of A×B. It can be thought of as coordinatized in the two directions by maximal elements of A resp. B. Without investigating the more complex interior structure of the pyramid (if seen as the product of the triangles for A and B) we can think of the elements ⟨a, b⟩ ∈ A × B as points in the pyramid, and the upper set ↑⟨a, b⟩ generated by a point as a little four-sided pyramid within the large pyramid for A × B. Its base is a rectangular part of the base of that pyramid, and one side of the rectangle corresponds to ↑a ∩ A_{max}, the other to ↑b ∩ B_{max}:

⟨a, b⟩ B_{max}↑b ∩ B_{max}  A_{max} ↑a ∩ A_{max}

Finitely generated upper sets as they are used in the construction of snacks are the union of finitely many four-sided pyramids and therefore form some kind of an upsidedown roof (or a collection of roofs). The shadow they cast on the base of the pyramid (i. e. their intersection with the base) is a finite union of rectangular polygons. In order to make statements about a set M ⊆ A_{max} × B_{max} which is approximated by a snack (U, L) it suffices to look at the pyramid’s base and these shadows. Here is an example:

A^{max} (L_{1})_{max} B_{max}  U_{max} x_{3}  x_{1} (L_{2})_{max} x_{2}  x_{4}

The set M = {x_{1}, …, x_{4}}, for example, is approximated by (U, {L_{1}, L_{2}}) since all elements of M are in U and for each L ∈ L = {L_{1}, L_{2}} there is an element of M which is in L, viz. x_{1} for L_{1} and x_{2} for L_{2}.

The pictures drawn and thought of so far stem from simultaneously considering the A- and the B-component of the elements. In nested relational databases, nesting along B (i. e. making B-nests) results in a different way of looking at the situation. Now each A-value is given together with the set of B-values associated with it. Intuitively, we change from a set of points to a set of lines:

B  A  B  A

In the presence of partiality, things become more involved. In a first step, we introduce partiality for B-values, i. e. every A-value will be given together with a snack that approximates the set of B-values that go with it. However, also the A-values are only known approximatively. Again, we express this by using a snack. It will give upper and lower bounds for the set of pairs ⟨a, (U^{B}, L^{B})⟩ that approximate lines (rather than elements) of the approximated subset of (A × B)_{max}.

In order to clarify these ideas, let us look at the structure and the interpretation of a nested snack. It will be of the form (U^{A{B}}, L^{A{B}}) where L^{A{B}} consists of finitely many sets L^{A{B}}. These and the set U^{A{B}} are upper sets in A × S(B) which are generated by finitely many pairs of the form ⟨a, (U^{B}, L^{B})⟩, i. e. an element a ∈ A together with a snack on B.

For a pictorial presentation of this situation we will draw U^{A{B}} and each L^{A{B}} ∈ L^{A{B}} in a separate picture. Each of the generating pairs of these sets casts a shadow of the following form on (A × B)_{max}:

B_{max}  A^{max}

The A-direction of the shadow corresponds to ↑a ∩ A_{max}, the B-direction of the large rectangle to (U^{B})_{max}. The shaded rectangles which are within the large rectangle correspond to the sets L^{B} ∈ L^{B}. For each such set L^{B} we get one shaded region where the A-direction is again ↑a ∩ A_{max} and the B-direction is (L^{B})_{max}. We call this picture a “stripe”.

The sets U^{A{B}} and L^{A{B}} are gotten by composing the stripes of the generating pairs into one picture:

B_{max}  A^{max}

As the example shows, the stripes of the generating pairs may intersect, and the sets L^{B} may be empty, resulting in a stripe without shaded subregions. Another effect which may occur (but cannot be drawn) is that there may be pairs ⟨a, (∅, ∅)⟩. In this case, the “stripe” vanishes because there is no intersection of ∅ with B_{max}.

The interpretation of a union of stripes depends on whether it stems from the set U^{A{B}} or a set L^{A{B}}.

We first investigate the case where U^{A{B}} is the underlying set. The nested snack is a two-step approximation of a set M of lines {a} × B′ (with a ∈ A_{max} and B′ ⊆ B_{max}). In the first step, given by the snack on the outer level, the possible A-values of these lines are determined. Our picture of the shadow cast by U^{A{B}} says that all lines which are in M must have one of the A-values covered by projection of the union of stripes onto A_{max}. It remains to find the sets B′ ⊆ B_{max} which are possibly going with the A-value. This second step of approximation is made by the individual stripes. Every possible A-value stems from one of the stripes in the picture. The set B′ must be within the B-extension of that stripe, and within the B-extension of each shaded region of the stripe there must be an element of B′. We can summarize this by saying that the U^{A{B}}-picture does not tell us anything about the existence of lines. It only restricts the set of possible lines in two ways: Firstly, with respect to the possible A-values, and secondly with respect to the sets B′ which are allowed for an A-value.

We now look at the case where our picture stems from a set L^{A{B}}. Now the picture gives information about a line that must exist in M. Its A-value must be within the A-extension of one of the stripes. Once we choose the stripe, this determines the set B′ which is associated to the A-value in the same way as in our first case: The set B′ must be within the B-extension of the stripe and it must meet each of the shaded regions.

Thus, the collection L^{A{B}} of sets L^{A{B}} determines a lower bound of the set M by giving an approximation to a collection of indiviual lines which are guaranteed to be in M.

4.2 Nesting snacks

Hopefully, you now have a good intuition of nested snacks so that we can go on and discuss how to nest a snack on a product A × B to get B-nests. We start with a snack (U, L) on A × B. This is to be converted to a snack (U^{A{B}}, L^{A{B}}) of the kind which we discussed in the previous section.

Before we go on we fix a piece of notation:

Definition 4.1 For a subset R ⊆ A × B and an element a ∈ A we define

[a]R := {b ∈ B | ⟨a, b⟩ ∈ R} .

At first we determine U^{A{B}}. The snack (U, L) approximates a set M ⊆ (A×B)_{max} in its “point”-representation, and each m ∈ M must be in U ∩ (A × B)_{max}. If we change to the “line”-representation M̄ of M, we must make sure that all the lines are within U ∩ (A × B)_{max}. This means that the union of the stripes which correspond to elements of U^{A{B}} must be U ∩ (A × B)_{max}. Hence, given an A-value a, we take those B-values as elements of U^{B} which are in U-relation with a, i. e. those b ∈ B with ⟨a, b⟩ ∈ U. We do not impose any restriction in the sense of shaded regions. Any information concerning guaranteed elements will be dealt with later. Thus, for an a ∈ A, we get the pair ⟨a, ([a]U, ∅)⟩ as an element of U^{A{B}}. Note that we do not need to restrict the A-values. If there is no matching B-value for some a ∈ A, we will simply get the pair ⟨a, (∅, ∅)⟩, the shadow of which is empty. You may check yourself that this construction works in general, however here is an example for a set U and its transformation to the set U^{A{B}}:

A_{max} ↑{b_{3}, b_{4}} ∩ B_{max} ↑b_{1} ∩ B_{max} ↑b_{2} ∩ B_{max} B_{max}  ↑a_{1} ∩ A^{max} ↑a_{2} ∩ A_{max}  ↑{b_{1}, b_{2}} ∩ B_{max} ↑b_{4} ∩ B_{max} A_{max} ↑b_{3} ∩ B_{max} B_{max}  ↑a_{2} ∩ A_{max} ↑a_{1} ∩ A^{max}

We have

U = ↑{⟨a_{1}, b_{1}⟩, ⟨a_{1}, b_{2}⟩, ⟨a_{2}, b_{3}⟩, ⟨a_{2}, b_{4}⟩} .

The generators of U^{A{B}} then are

⟨a_{1}, (↑{b_{1}, b_{2}}, ∅)⟩ and ⟨a_{2}, (↑{b_{3}, b_{4}}, ∅)⟩

but also

⟨⊥_{A}, (∅, ∅)⟩ and ⟨a_{1} ∨ a_{2}, (↑{b_{1}, b_{2}, b_{3}, b_{4}}, ∅)⟩ .

While the first two generators do not come as a surprise, the third and the fourth generator need some explanation. The pair ⟨⊥_{A}, (∅, ∅)⟩ expresses that there is no B-values which is paired with the least element of A. As far as the shadows are concerned it is not needed, but in the spirit of the approximation of lines which we gave above, we have to include it. The shadow of the pair ⟨a_{1}∨a_{2}, (↑{b_{1}, b_{2}, b_{3}, b_{4}}, ∅)⟩ seems to be covered by the first two generators. However, they do not allow for really long lines which extend over the whole of the shaded region. If we did not include this fourth generator, we would have to split up these long lines artificially into two shorter lines which are covered by the first two generating pairs.

Let us now turn to determining L^{A{B}}. It will consist of finitely many sets L^{A{B}} each of which is generated by finitely many “stripes”. Each L ∈ L informs us of an element that is guaranteed to belong to the approximated set M. We can now turn this into information about a line that belongs to the line representation M̄ of M. Thus, for each L ∈ L we get one set L^{A{B}} ∈ L^{A{B}}, and now we will explicate how this transformation is done.

Given an L ∈ L, the line which we guarantee may actually be a very short line, consisting of one point only. As we have only approximative information of the whereabouts of this point, the set L^{A{B}} may nevertheless have to deal with larger regions. The first question is: For which A-values do we include a stripe into L^{A{B}}? As we are speaking of guaranteed elements of M resp. M̄, we only want those a ∈ A to appear which — together with some b ∈ B — form a pair ⟨a, b⟩ ∈ L. Given an a of that kind, we ask for the maximal extension of B-values that go with a. This is determined by the set of B-values which are connected with a in the set U. Hence, the B-extension of an a-stripe is given by [a]U. We now have to determine the shaded regions of the a-stripe. As the set L gives rise to just one guaranteed point, we can at most guarantee one B-value to go with a and hence have only one shaded region. In fact, this is to be thought of as a guaranteed B-value only in case that the guaranteed A-value happens to be the one whose stripe we are about to construct. The B-values of this single shaded region are gotten out of L: They are those b ∈ B which are in L-relation with a, i. e. the stripe we want to construct is cast as a shadow by the pair ⟨a, ([a]U, {[a]L})⟩. As said above, we have to do this for all a ∈ π_{1}(L), such that L ∈ L is translated into

{⟨a, ([a]U, {[a]L})⟩ | a ∈ π_{1}(L)} .

This completes our construction of the nesting operator, which we summarize by giving the function definition:

nest : S(A × B) → S(A × S(B))
nest(U, {L_{1}, …, L_{k}})
:= (↑{⟨a, ([a]U, ∅)⟩ | a ∈ A},
{↑{⟨c, ([c]U, {[c]L_{i}})⟩ | c ∈ π_{1}(L_{i})} | i = 1, …, k}) .

For the more critical reader who does not believe in the intuitive approach, we now give a proof that the nest-operation is well formed. We start with collecting a number of useful results. By fst(·) and snd(·) we denote the first resp. second component of a snack.

Proposition 4.2 If U ⊆ A × B is an upper set and a an element of A, then [a]U is an upper set in B.

Proposition 4.3 If a ≤ a′ in A and U ⊆ A × B is an upper set then [a]U ⊆ [a′]U.

Proof: With ⟨a, b⟩ ∈ U we also have ⟨a′, b⟩ ∈ U because U is an upper set.

Proposition 4.4 If U is an open set in A × B then so is [a]U in B.

Proof: A directed supremum ^{⋁ ↑}_{i∈I} b_{i} is in [a]U if and only if ^{⋁ ↑}_{i∈I}⟨a, b_{i}⟩ is in U.

Proposition 4.5 For every a ∈ A and every finitely generated upper set U ⊆ A × B the set M := [a]U is a finitely generated upper set in B. If the generators of U are {⟨a_{1}, b_{1}⟩, …, ⟨a_{n}, b_{n}⟩} then M = ↑{b_{i} | a ≥ a_{i}, i ∈ {1, …, n}}.

Proof: If ⟨a, b⟩ ∈ U then there is some i ∈ {1, …, n} with ⟨a, b⟩ ≥ ⟨a_{i}, b_{i}⟩. Therefore M = {b | ⟨a, b⟩ ∈ U} ⊆ ↑{b_{i} | a ≥ a_{i}, i ∈ {1, …, n}}. Of course we have b_{i} ∈ M for all i with a ≥ a_{i}. As M is an upper set (Lemma 4.2), the desired equality is shown.

Proposition 4.6 If U ⊆ A × B is a compact upper set and a is an element of A, then [a]U is a compact upper set in B.

Proof: The Hofmann-Mislove Theorem [HM81, KP94] tells us that U is the filtered intersection of its open neighbourhoods O_{i} (i ∈ I). The set [a]U = [a](⋂_{i∈I} O_{i}) = ⋂_{i∈I}([a]O_{i}) is again a filtered intersection of open sets, i. e. a compact upper set.

Proposition 4.7 If U ⊆ A × B is a finitely generated upper set then there are only finitely many sets [a]U. If U is generated by the finite set M and {a_{1}, …, a_{n}} = π_{1}(M) then the sets [a]U are those subsets of B which are in relation to a supremum of a subset of {a_{1}, …, a_{n}}.

Proof: Let a ∈ A and ǎ := ⋁{a_{i} | a_{i} ≤ a, i ∈ {1, …, n}}. We have ǎ ≤ a and [ǎ]U ⊆ [a]U because of Proposition 4.3. If b is in [a]U, that is if ⟨a, b⟩ ∈ U then there is some ⟨a_{i}, b_{i}⟩ ∈ M which is below ⟨a, b⟩. Then ⟨ǎ, b⟩ ≥ ⟨a_{i}, b⟩ ≥ ⟨a_{i}, b_{i}⟩ from which we learn⟨ǎ, b⟩ ∈ U. This shows [ǎ]U = [a]U.

Proposition 4.8 If L and L′ are subsets of A×B and if there is some ⟨a, b⟩ ∈ L\L′ then

[a]L ⊈ [a]L′ .

Proposition 4.9 If L and L′ are compact opens in A × B satisfying L ⊈ L′ then there is some a ∈ π_{1}(L) such that [a]L ⊈ [a′]L′ for all a′ ≤ a.

Proof: There is an element ⟨a, b⟩ ∈ L \ L′. As L′ is an upper set, there is no a′ ≤ a such that the pair ⟨a′, b⟩ belongs to L′. Consequently, b ∈ [a]L \ [a′]L′.

Proposition 4.10 Let L and L′ be compact open subsets of A × B which are not in ⊆-relation and which are contained in the compact open set. Then the subsets

↑{⟨c, ([c]U, {[c]L})⟩ | c ∈ π_{1}(L)} (1)

and

↑{⟨c, ([c]U, {[c]L′})⟩ | c ∈ π_{1}(L′)} (2)

of A × S(B) are not in ⊆-relation.

Proof: Following Proposition 4.9, there is some ĉ ∈ π_{1}(L) such that [ĉ]L ⊈ [c′]L′ for all c′ ≤ ĉ. Hence there cannot be an element in (2) which is less or equal ⟨ĉ, ([ĉ]U, {[ĉ]L})⟩. Therefore (1) ⊈ (2). Our claim follows because of the symmetry of the situation.

We now come to the main result about the function nest.

Lemma 4.11 The function nest maps each snack (U, {L_{1}, …, L_{k}}) on A × B to a snack on A × S(B).

Proof: Using Propositions 4.4 and 4.6 we see that [a]U is compact open for all a ∈ A (and hence for all a ∈ π_{1}(L_{i}), i = 1, …, k) and [c]L_{i} is compact open for all c ∈ π_{1}(L_{i}) (i = 1, …, k). Because of ∅ ≠ L_{i} ⊆ U we have ∅ ≠ [c]L_{i} ⊆ [c]U for c ∈ π_{1}(L_{i}) for i = 1, …, k. As the snacks on the inner level of the result under nest have an empty or one-element second component, we do not need to check whether these components are antichains. Hence, the snacks on the inner level are well formed.

On the outer level, we do not need all a ∈ A resp. c ∈ π_{1}(L_{i}) for generation. Using Proposition 4.7 we see that finitely many suffice. Their compactness follows from the compactness of the building components.

It is easy to see that the sets in the second component of nest(U, {L_{1}, …, L_{k}}) are nonempty and contained in the first component. They are nonempty since so are the sets L_{i} (i = 1, …, k) and they are contained in the first component because π_{1}(L_{i}) ⊆ A and ⟨c, ([c](U), ∅)⟩ ≤ ⟨c, ([c]U, {[c]L_{i}})⟩ for all i = 1, …, k and c ∈ π_{1}(L_{i}).

Finally, Proposition 4.10 shows that the second component of the result of nest is an antichain w. r. t. ⊆.

This proves that nest maps snacks on A × B to well-formed snacks on A × S(B).

Lemma 4.12 The function nest is monotone.

Proof: Let (U, L) and (U′, L′) be snacks on A × B such that (U, L) ⊑ (U′, L′). For every a ∈ A we have [a]U ⊇ [a]U′. Hence it follows that fst(nest(U, L)) ⊇ fst(nest(U′, L′)). For every L ∈ L there is some L′ ∈ L′ with L′ ⊆ L and for all c ∈ π_{1}(L′) we have

([c]U, {[c]L}) ⊑ ([c]U′, {[c]L′}) .

Furthermore, π_{1}(L) ⊇ π_{1}(L′), i. e. c ∈ π_{1}(L) for all c ∈ π_{1}(L′). Therefore we can conclude

↑{⟨c, ([c]U, {[c]L})⟩ | c ∈ π_{1}(L)} ⊇ ↑{⟨c, ([c]U′, {[c]L′})⟩ | c ∈ π_{1}(L′)} .

For every set in snd(nest(U, L)) we thus found a smaller set in snd(nest(U′, L′)). This proves nest(U, L) ⊑ nest(U′, L′).

4.3 Unnesting snacks

In order to nest a traditional database relation, one has to know the entire relation that is to be nested. In contrast to this, the unnest operation can be performed stepwise. One takes the tuples of the nested relation seperately. A pair that consists of some a ∈ A and a set of B-values is transformed into the set of pairs ⟨a, b⟩ with b being one of the B-values. The result of the unnest operation then is the union of all sets which we obtain in this way.

In case of domain theoretic databases we can proceed in a very similar way. For this we use the characterization of the snack-powerdomain as a free algebra [Puh93]. We start with introducing the relevant operations on snacks.

Definition 4.13 The formal union on the set S(D) of snacks on a domain D is given by

∪ : S(D) × S(D) → S(D) ,
(U, L) ∪ (U′, L′) := (U ∪ U′, MIN^{⊆}(L ∪ L′))

where MIN^{⊆} selects those sets which are minimal under subset inclusion.

The snack (∅, ∅) is a neutral element w. r. t. ∪.

Any two snacks on a domain have an infimum. We include this explicitly as an operation:

Lemma 4.14 The operation

⊓ : S(D) × S(D) → S(D)
(U, L) ⊓ (U′, L′) = (U ∪ U′, MIN^{⊆}({L ∪ L′ | L ∈ L, L′ ∈ L′}))

builds the infimum of two snacks.

We incorporate the algebraic properties of these operations in the following definitions.

Definition 4.15 An ordered algebra is an algebra with an order relation on the carrier set and operations which are monotone w. r. t. this order.

Definition 4.16 A snack algebra is an ordered algebra (M, ⊑) with two semilattice operations ∪ , ⊓ : M × M → M and a constant e ∈ M such that for all r, s, t ∈ M:

\begin{aligned}r ⊓ s & ⊑ & r \\ e ∪ r & = & r \\ (r ∪ s) ⊓ t & = & (r ⊓ t) ∪ (s ⊓ t) \end{aligned}

A snack-algebra homomorphism is a monotone function that preserves ∪, ⊓ and e.

One easily checks that the set of snacks on a domain together with ∪, ⊓ and (∅, ∅) (playing the role of e) is a snack algebra.

The key to our unnest operation is that every snack can be built out of primitive snacks by means of ∪ and ⊓. The primitive snacks are called “singletons”:

Definition 4.17 Let x be a compact element of the domain D. The singleton of x is the snack {|x|} := (↑x, {↑x}).

Lemma 4.18 Every snack s on a domain D can be built out of singletons by means of ∪, ⊓, and (∅, ∅).

If s = (U, {L_{1}, …, L_{k}}), U = ↑{u_{1}, …, u_{n}} and L_{i} = ↑{l_{i1}, …, l_{im_{i}}} (i = 1, …, k; m_{i} ∈ ℕ for i = 1, …, k), then

s = ({|u_{1}|} ⊓ … ⊓ {|u_{n}|} ⊓ (∅, ∅)) ∪
({|l_{11}|} ⊓ … ⊓ {|l_{1m_{1}}|}) ∪ … ∪ ({|l_{k1}|} ⊓ … ⊓ {|l_{km_{k}}|}) .

The algebraic characterization of the snack-powerdomain can be stated as follows:

Theorem 4.19 The set S(D) of snacks on a domain D together with ∪, ⊓, and (∅, ∅) is the free snack algebra generated by the ordered set KD of compact elements of D, i. e. for every snack algebra A and every monotone mapping f : KD → A, there is a uniquely determined snack-algebra homomorphism f^{+} : S(D) → A such that f^{+} ∘ {| · |} = f.

This enables us to define an unnest operation stepwise. Rather than unnesting a snack on A × S(B) right away, we take an element of K(A) × S(B) and transform it into a snack on A × B by pairing the generating elements of the snack on B with the compact element from A (hence the name pw, pairwith):

Definition 4.20 Let ⟨a, (U, {L_{1}, …, L_{k}})⟩ be in KA × S(B). We define

pw(⟨a, (U, {L_{1}, …, L_{k}})⟩) := (↑a × U, {↑a × L_{1}, … ↑a × L_{k}}) .

Proposition 4.21 The function pw maps elements of KA×S(B) to snacks on A×B and is monotone.

Proof: As a is in KA, the set ↑a is compact open in A. The products of ↑a with the compact opens U, L_{1}, …, L_{k} from B are compact open in A × B. The remaining requirements for snacks on A × B follow from the fact that (U, {L_{1}, …, L_{k}}) is a snack on B.

Monotonicity of pw is also easily seen.

Using Theorem 4.19 we get a snack-algebra homomorphism pw^{+} : S(A × S(B)) → S(A × B) which we call unnest:

Definition 4.22 The function unnest is the uniquely determined extension of pw to a snack-algebra homomorphism from S(A × S(B)) to S(A × B), as given by Theorem 4.19:

unnest(↑{⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩}, {↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{im_{i}}, D_{im_{i}}⟩} | i = 1, …, k})

= (pw(⟨a_{1}, B_{1}⟩) ⊓ … ⊓ pw(⟨a_{n}, B_{n}⟩) ⊓ (∅, ∅))

∪ ⋃ ; −_{i=1}^{k} (pw(⟨c_{i1}, D_{i1}⟩) ⊓ … ⊓ pw(⟨c_{im_{i}}, D_{im_{i}}⟩)) .

In order to unnest a concretely given snack, the following representation is more useful: Lemma 4.23 The function unnest satisfies

unnest(↑{⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩}, {↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{im_{i}}, D_{im_{i}}⟩} | i = 1, …, k})

= ( ⋃_{j=1}^{n}(↑a_{j} × fstB_{j}), MIN^{⊆} ⋃_{i=1}^{k}{ ⋃_{j=1}^{m_{i}}(↑c_{ij} × ℓ(j)) | ℓ:{1, …, m_{i}} ⟶^{⊙} ⋃_{j=1}^{m_{i}} sndD_{ij}}),

where ℓ:{1, …, m_{i}} ⟶^{⊙} ⋃_{j=1}^{m_{i}} sndD_{ij} is a choice function, i. e. ℓ(j) ∈ sndD_{ij}. Proof: We have

(pw(⟨a_{1}, B_{1}⟩) ⊓ … ⊓ pw(⟨a_{n}, B_{n}⟩) ⊓ (∅, ∅))

∪ ⋃ ; −_{i=1}^{k} (pw(⟨c_{i1}, D_{i1}⟩) ⊓ … ⊓ pw(⟨c_{im_{i}}, D_{im_{i}}⟩))

= ( ⋃_{j=1}^{n}(↑a_{j} × fstB_{j}), ∅) ∪ ⋃ ; −_{i=1}^{k} ( ⋃_{j=1}^{m_{i}}(↑c_{ij} × fstD_{ij}),

MIN^{⊆}{ ⋃_{j=1}^{m_{i}}(↑c_{ij} × ℓ(j)) | ℓ:{1, …, m_{i}} ⟶^{⊙} ⋃_{j=1}^{m_{i}} sndD_{ij}})

= ( ⋃_{j=1}^{n}(↑a_{j} × fstB_{j}), MIN^{⊆} ⋃_{i=1}^{k}{ ⋃_{j=1}^{m_{i}}(↑c_{ij} × ℓ(j)) | ℓ:{1, …, m_{i}} ⟶^{⊙} ⋃_{j=1}^{m_{i}} sndD_{ij}}) .

The last step is correct since ⋃_{j=1}^{m_{i}}(↑c_{ij} ×fstD_{ij}) ⊆ ⋃_{j=1}^{n}(↑a_{j} ×fstB_{j}) for i = 1, …, k.

4.4 Nest and unnest combined

Now we prove that nest and unnest form, as promised, an embedding-projection pair. Lemma 4.24 For the functions nest and unnest as defined above we have the identity unnest ∘ nest = id. Proof: Let (U, {L_{1}, …, L_{k}}) ∈ S(A × B). Then

unnest(nest(U, {L_{1}, …, L_{k}}))

= unnest(↑{⟨a, ([a]U, ∅)⟩ | a ∈ A},
{↑{⟨c, ([c]U, [c]L_{i}})⟩ | c ∈ π_{1}(L_{i})} | i = 1, …, k}).

For the unnest operation, we can handle the two components of the outer snack seperately. Proposition 4.7 guarantees the existence of a finite subset Ǎ of A with

↑{⟨a, ([a]U, ∅)⟩ | a ∈ A} = ↑{⟨a, ([a]U, ∅)⟩ | a ∈ Ǎ} .

Moreover, for every a ∈ A there is some ǎ ∈ Ǎ with ǎ ≤ a and [a]U ⊆ [ǎ]U. The first component of the snack that is to be unnested is therefore transformed to

⋃_{a∈Ǎ} (↑a × [a]U) = ⋃_{a∈A} (↑a × [a]U) ⊇ ⋃_{a∈A} ({a} × [a]U) = U.

As U is an upper set, the reverse inclusion is also seen to hold.

Just as for the first component we find a finite set Č_{i} for the i^{th} set in the second component such that Č_{i} generates π_{1}(L_{i}) and that this i^{th} set is generated by the pairs ⟨c, ([c]U, {[c]L_{i}})⟩ with c ∈ Č_{i}. Note that the second components of the occuring snacks have only one element. Hence, there is only one choice function and this set is transformed to

{ ⋃_{c∈Č_{i}}(↑c × [c]L_{i})} .

That this equals L_{i} is seen with the same argumentation as in the case of U.

Therefore the second component of the result of unnest is MIN^{⊆}({L_{1}, …, L_{k}}). This equals {L_{1}, …, L_{k}} because the sets L_{1}, …, L_{k} form an antichain w. r. t subsetinclusion.

This completes the proof.

In order to prepare the next result we show:

Proposition 4.25 Let U_{1}, …, U_{n} be subsets of B and a_{1}, …, a_{n} elements of A. Furthermore, let c ≥ a_{i} and V ⊆ U_{i} for some i ∈ {1, …, n}. Then

[c]( ⋃_{j=1}^{n}(↑a_{j} × U_{j})) ⊇ V .

Proof: We have

[c]( ⋃_{j=1}^{n}(↑a_{j} × U_{j})) ⊇ [c](↑a_{i} × U_{i}) = U_{i} ⊇ V .

Lemma 4.26 For the functions nest und unnest we have

nest ∘ unnest ≤ id .

Proof: We apply nest ∘ unnest to an element of S(A × SB)) and introduce abbreviations for some sub-terms:

nest(unnest(↑{⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩}, {↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{i_{mi}}, D_{i_{mi}}⟩} | i = 1, …, k}))

= nest(\underbrace{⋃_{j=1}^{n}(↑a_{j} × fstB_{j})}_{U}, MIN^{⊆}(\underbrace{⋃_{i=1}^{k}\{⋃_{l=1}^{m_{i}}(↑c_{il} × ℓ(l)) | ℓ:\{1, …, m_{i}\} ⟶^{⊙} ⋃_{l=1}^{m_{i}} sndD_{il}\}}_{L})) .

The proof is now done in several steps. Step 1: We show that fst(nest(U, MIN^{⊆}(L))) ⊇ ↑{⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩}.

Because of fst(nest(U, L)) = ↑{⟨a, [a]U), ∅)⟩ | a ∈ A} it suffices to prove

([a_{i}]U, ∅) ⊑ B_{i}

for i = 1, …, n. For the second component there is nothing to do since this is empty for the snack on the left hand side. It remains to show

[a_{i}]( ⋃_{j=1}^{n}(↑a_{j} × fstB_{j})) ⊇ fst(B_{i}) .

But this is an immediate consequence of proposition 4.25. Step 2: For every M ∈ snd(nest(U, MIN^{⊆}(L))) we have to find an i ∈ {1, …, k} such that M ⊇ ↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{im_{i}}, D_{im_{i}}⟩}. This means that for every L_{•} ∈ MIN^{⊆}(L) we have to find an i ∈ {1, …, k} with

↑{⟨c, ([c]U, {[c]L_{•}})⟩ | c ∈ π_{1}(L_{•})} ⊇ ↑{⟨c_{i1}, D_{i1}⟩, …, ⟨c_{im_{i}}, D_{im_{i}}⟩} . (∗)

We do not restrict ourselves to those elements of L which are minimal w. r. t. ⊆. Instead we show the existence of such a number i for all L_{•} ∈ L.

For every L_{•} ∈ L, there is a natural candidate for the i ∈ {1, …, k} which we are looking for. The set L is the union of certain sets which are distinguished by a parameter between 1 and k. The parameter of that subset of L that contains L_{•} is the number we are looking for.

We now assume that i ∈ {1, …, k} is such that

L_{•} ∈ {⋃_{l=1}^{m_{i}}(↑c_{il} × ℓ(l)) | ℓ:{1, …, m_{i}} ⟶^{⊙} ⋃_{l=1}^{m_{i}} sndD_{il}} ,

and ℓ_{•}:{1, …, m_{i}} ⟶^{⊙} ⋃_{l=1}^{m_{i}} sndD_{il} is given such that L_{•} = ⋃_{l=1}^{m_{i}}(↑c_{il} × ℓ_{•}(l)).

In order to show (∗), we first verify c_{ij} ∈ π_{1}(L_{•}) for all j ∈ {1, …, m_{i}}.

For all j ∈ {1, …, m_{i}} we have

π_{1}(L_{•}) = π_{1}(⋃_{l=1}^{m_{i}} ↑c_{il} × ℓ_{•}(l)) ⊇ π_{1}(↑c_{ij} × ℓ_{•}(l)) .

Because of ℓ_{•}(j) ≠ ∅ it follows that c_{ij} ∈ π_{1}(↑c_{ij} × ℓ_{•}(j)). This yields c_{ij} ∈ π_{1}(L_{•}). To reach our aim of proving (∗) it now remains to show

([c_{ij}]U), {[c_{ij}]L_{•})}) ⊑ D_{ij}

for all j ∈ {1, …, m_{i}}.

We do this seperately for the two components of the snacks.

\underline{Step 2a}: We show: [c_{ij}]U ⊇ fst(D_{ij}).

There is some ⟨ǎ, B̌⟩ ∈ {⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩} with ⟨ǎ, B̌⟩ ≤ ⟨c_{ij}, D_{ij}⟩ since the first component of a snack is a superset of each element of its second component. Therefore ǎ ≤ c_{ij} and fstD_{ij} ⊆ fstB̌. Consequently, fst(B_{1}), …, fst(B_{n}), a_{1}, …, a_{n}, c_{ij} and fst(D_{ij}) meet the requirements of proposition 4.25, and the desired result follows.

\underline{Step 2b}: We have to show that there is some L_{D} ∈ snd(D_{ij}) with

[c_{ij}]L_{•} ⊇ L_{D} .

We have

L_{•} = ⋃_{l=1}^{m_{i}}(↑c_{il} × ℓ_{•}(l)) ,

where ℓ_{•}(l) ∈ snd(D_{il}) for each l ∈ {1, …, m_{i}}. If we choose L_{D} = ℓ_{•}(j) then the desired result follows directly with Proposition 4.25.

This completes Step 2 and the entire proof.

5 A comparison with nested relational algebra

In this section we investigate how snack-representations of nested relations are transformed by means of nest and unnest. Because of unnest ∘ nest = id, no snackrepresentation of a nested relation will be altered by this composition of the two operations. We thus concentrate on the other composition, i. e. nest ∘ unnest, and proceed as follows: We first give a new presentation of snacks which is easier to read. After that we show how nested snacks which represent a nested relation are unnested. From that we can finally move to nesting the flat snacks again and comparing the result with the effects of nested relational algebra. As throughout the paper, we will consider relations with attributes A and B where in the nested relations the nested attribute is B.

In order to obtain a more readable presentation of snacks, we introduce a new notation: For a snack (U, L) we tag the set U by a □ and each L ∈ L by a ♢. This is in line with the interpretation of □ and ♢ in modal logic: We take the elements of the approximated set as possible worlds, then □U says that each element must satisfy U, i. e. be in U, and ♢L says that there must be an element which is in L.^{3} We do not require the tagged sets to be upper sets but take the given elements as a (not necessarily minimal) set of generators. Thus, a snack (U, {L_{1}, …, L_{k}} with generators u_{1}, …, u_{n} (for U) and l_{i1}, …, l_{im_{i}} (for L_{i}) can be represented as a collection of tagged relations:

□: u_{1} ; ⋮ ; u_{n}  ♢: l_{11} ; ⋮ ; l_{1m_{1}} … ♢: l_{k1} ; ⋮ ; l_{km_{k}}

3A more detailed account of the use of □ and ♢ in a logical representation of the snack powerdomain can be found in [JP95, Puh95].

In nested snacks, each tuple of a tagged relation will have a part which itself is a collection of tagged relations. When we go about to unnest a nested snack of this kind, we may proceed stepwise, as shown in Section 4.3.

The first step is to apply the function pw to the individual tuples of the tagged relations of the outer level. Generally, these tuples look like the following:

a □: u_{1} ; ⋮ ; u_{n}  ♢: l_{11} ; ⋮ ; l_{1m_{1}} … ♢: l_{k1} ; ⋮ ; l_{km_{k}}

By means of pw these are transformed to the following snack:

□: a u_{1} ; ⋮ ; a u_{n}  ♢: a l_{11} ; ⋮ ; a l_{1m_{1}} … ♢: a l_{k1} ; ⋮ ; a l_{km_{k}}

The result of unnesting a nested snack is now obtained by putting these pieces together as in Definition 4.22. In doing so, it matters where the tuple comes from. If it stems from a relation tagged with □ then it adds to the first component of the resulting snack, i. e. the relation that will also be tagged with □. In this case, the tuples ⟨a, u_{1}⟩, …, ⟨a, u_{n}⟩ will belong to this first component. All the tuples which come from a sub-relation with a ♢ are not used.

If the tuple however comes from one of the relations that have a ♢ then the □-subrelations will not be needed. Instead, those parts which also have a ♢ on the inner level will contribute to the result of unnesting. Fortunately, we do not have to discuss how this is done in general. The nested snacks which we will be interested in, viz. those which are a representation of a nested database relation, have a very special structure. In these snacks, all relations which are tagged with a ♢ have exactly one element because we interpret each element of a database relation as giving information about an element that is guaranteed to be in the set which is described by the relation. So each element makes a singleton ♢-set. By analyzing the formula in Lemma 4.23, one verifies that in this situation each pair ⟨a, l_{ij}⟩ from the above snack will finally form a one-tuple ♢-tagged relation in the result of unnest.

This leads to the following result:

Lemma 5.1 If {⟨a_{1}, B_{1}⟩, …, ⟨a_{n}, B_{n}⟩} is a nested relation of type {A × {B}} then its snack representation is unnested to

□( ⋃_{i=1}^{n}({a_{i}} × B_{i})), { ♢ {⟨a, b⟩} | ⟨a, b⟩ ∈ ⋃_{i=1}^{n}({a_{i}} × B_{i})} .

Note that, just as with nested relational algebra, those tuples with empty subrelations will vanish when the nested snack is unnested.

To illustrate the effect of the unnest operation, let us once again look at the sample relation from Section 2.

R : A  {B}
a_{1}  \begin{matrix}b_{1} \\ b_{2} \end{matrix}

a_{1}  \begin{matrix}b_{2} \\ b_{3} \end{matrix}
a_{2}  ∅

We already gave its snack representation in Section 3.4. In our new notation it looks as follows:

□:  a_{1}  \begin{aligned}□: & b_{1} \\ & b_{2} \end{aligned}  ♢: b_{1}  ♢: b_{2}

a_{1}  \begin{aligned}□: & b_{2} \\ & b_{3} \end{aligned}  ♢: b_{2}  ♢: b_{3}
a_{2}  □ : ∅

♢:  a_{1}  \begin{aligned}□: & b_{1} \\ & b_{2} \end{aligned}  ♢: b_{1}  ♢: b_{2}

♢:  a_{1}  \begin{aligned}□: & b_{2} \\ & b_{3} \end{aligned}  ♢: b_{2}  ♢: b_{3}

♢:  a_{2}  □ : ∅

The result of unnesting this snack is:

\begin{aligned}□: & a_{1} & b_{1} \\ & a_{1} & b_{2} \\ & a_{1} & b_{3} \end{aligned}  ♢: a_{1} b_{1}  ♢: a_{1} b_{2}  ♢: a_{1} b_{3}

This is exactly the snack representation of μ(R), the result of unnesting R by means of Schek’s unnest operation μ. In fact, one easily checks that this is true in general:

Theorem 5.2 Let R be a nested relation of type {A × {B}} and R^{S} be its snack representation. Then unnest(R^{S}) is the snack representation of μ(R).

The difference is made in nesting the relation again. A closer look at the nest operation reveals that there is no snack (U, L) such that nest(U, L) is the snack representation of a nested database relation.

For our example, nest(unnest(R)) is given by

□: a_{1}  \begin{aligned}□: & b_{1} \\ & b_{2} \\ & b_{3} \end{aligned}

⊥  □ : ∅

♢: a_{1}  \begin{aligned}□: & b_{1} \\ & b_{2} \\ & b_{3} \end{aligned}  ♢: b_{1}

♢: a_{1}  \begin{aligned}□: & b_{1} \\ & b_{2} \\ & b_{3} \end{aligned}  ♢: b_{2}

♢: a_{1}  \begin{aligned}□: & b_{1} \\ & b_{2} \\ & b_{3} \end{aligned}  ♢: b_{3}

Let us conclude with a few remarks on this result. First of all, the □-component contains the tuple that we get as a result of νμ(R) by means of the nested relational algebra operations. So it might seem that nested relations have to be equipped with the □-meaning in order to satisfy ν ∘ μ ≤ id. But if we did so, the problem of vanishing tuples with empty sub-relations would remain. In order to capture these we have to include the tuple ⟨⊥, □ : ∅⟩. In the absence of a least element ⊥ we would have to include the tuples ⟨a, □ : ∅⟩ for all a ∈ A. If A happened to be infinite then we would leave the realm of finite relations. In so far, the order structure with a least element is crucial for a definition of nesting and unnesting operations which build an embedding-projection pair.

The ♢-components, finally, practically do not build nests at all since each of the elements b_{1}, b_{2} and b_{3} gives rise to a seperate ♢-component. But this is sound if we think of each database entry as a piece of information about objects which are guaranteed to exist.

The result of our operations is only natural if we recall that unnesting is bound to destroy all information on how the B-values were grouped in the original relation. When we nest the unnested relation again, the most we can say is that the B-groups going with a_{1} are nonempty subsets of the set {b_{1}, b_{2}, b_{3}}, and that each of these elements must occur in one B-group. Clearly, this is what the nested snack from above says.

6 Conclusion

There are two main aspects one has to focus on when using domains for generalizing relational databases. The first is that the domain theoretic model must allow for the datatypes of databases. For relational databases, these are certain ground types and the two type-constructors “finite product” and “set of”. While the ground types can be modelled as flat domains, the type-constructors are given by the product of domains and the snack powerdomain. As these can be applied repeatedly, we are even able to model the nested relations model. This was already mentioned in [JP95].

The second aspect is to find meaningful operations for the generalized model. It is desirable that these operations include conservative extensions of (nested) relational algebra. There is no difficulty in generalizing the relational projection. As observed by Buneman [BJO91], this can be done by domain theoretic projection functions. In this paper we defined the operations nest and unnest. The unnesting operation turns out to be a conservative extension to Jaeschke and Schek’s unnesting operator μ. However, we cannot expect nest to be an extension of their nesting operator ν since we argued that ν has no satisfactory semantics. Instead we define nest and unnest such that they preserve as much information as possible: nest as a domain theoretic embedding preserves all information contained in its argument whereas unnest loses only those pieces of information which need the richer structure of nested snacks in order to be represented.

Domain theoretic databases originally came along with the promise that they would allow for a representation and processing of partial information. Although we did not discuss the effect of nest and unnest on snack representations of partial data, it is now possible to study this with respect to domain-theoretic representations of various sorts of null values and otherwise structured data.

What remains is to find suitable generalizations of the relational “select” and “join” operations. While we believe that selections may successfully be modelled as suprema with snacks that incorporate the filter formula of the selection, the generalization of natural join seems to be a more demanding task. For this one will at first have to find a formal semantics of the join operation such as to check the definition of the operation with respect to this semantics. Another approach could be to define a function that, in composition with certain projections, satisfies the various conditions of losless joins. If that were successful, a possible semantics of natural join might emerge from the definition.

References

[AJ95] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3. Clarendon Press, 1995.

[BJO91] P. Buneman, A. Jung, and A. Ohori. Using powerdomains to generalize relational databases. Theoretical Computer Science, 91:23–55, 1991.

[HM81] K. H. Hofmann and M. Mislove. Local compactness and continuous lattices. In B. Banaschewski and R.-E. Hoffmann, editors, Continuous Lattices, Proceedings Bremen 1979, volume 871 of Lecture Notes in Mathematics, pages 209–248. Springer Verlag, 1981.

[JP95] A. Jung and H. Puhlmann. Types, logic, and semantics for nested databases. Electronic Notes in Theoretical Computer Science, (1), 1995. Proceedings of the 11th Conference on Mathematical Foundations of Programming Semantics.

[JS82] G. Jaeschke and H.-J. Schek. Remarks on the algebra of non first normal form relations. In Proceedings of the ACM SIGACT/SIGMOD Symposium on Principles of DBS, 1982.

[KP94] K. Keimel and J. Paseka. A direct proof of the Hofmann-Mislove theorem. Proceedings of the AMS, 120:301–303, 1994.

[Nga92] Teow-Hin Ngair. Convex Spaces as an Order-theoretic Basis for Problem Solving. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, July 1992.

[Puh91] H. Puhlmann. A Semantics for Generalized Database Relations. Master’s thesis, Imperial College of Science, Technology and Medicine, London, 1991.

[Puh93] H. Puhlmann. The snack powerdomain for database semantics. In A. M. Borzyszkowski and S. Sokołowski, editors, Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, pages 650–659, 1993.

[Puh95] H. Puhlmann. Die Snack-Potenzkonstruktion: Grundlage einer Semantik genesteter Datenbanken. PhD thesis, Technische Hochschule Darmstadt, July 1995. 88pp.

[Sch88] M. H. Scholl. Das Modell geschachtelter Relationen. Dissertation, Fachbereich Informatik, Technische Hochschule Darmstadt, 1988.