Dual Tableaux for Relational Databases

Abstract

We present a calculus TRL of typed relations introduced in [MO04] which is intended to be a formal tool both for representing relational databases [Cod70] and also for reasoning with them. Typed relations are heterogeneous relations, i.e., the objects related with a relation may range over different domains. Three features of this calculus distinguish it from the calculus of ordinary relations in the Tarski-style.

1 Introduction

We present a calculus TRL of typed relations introduced in [MO04] which is intended to be a formal tool both for representing relational databases [Cod70] and also for reasoning with them. Typed relations are heterogeneous relations, i.e., the objects related with a relation may range over different domains. Three features of this calculus distinguish it from the calculus of ordinary relations in the Tarski-style.

First, associated with each relation is its type, which is a finite subset of a set whose members are interpreted as attributes. In this way we cope with the fact that database relations are determined by (finite) subsets of a set of attributes. Therefore, the relations of the calculus are relative in the sense suggested in [Orł88] and [DO02].

Second, as with ordinary relations, each typed relation has an arity, which is the cardinality of its type. However, for any n ≥ 1, the order of the elements in the n-tuples belonging to a relation does not matter. This reflects the well-known property of database relations that the order of the attributes in the data table is immaterial. Tuples are treated as mappings that assign to an attribute an element of its domain.

Third, the calculus is comprised of relations of various arities and some operations may act on relations of not necessarily the same arity.

The basic operations on typed relations are intersection, complement, product, and projection. The other typical operations used in relational databases, namely, union, complement of a relation with respect to another relation, natural join, division, and selection are definable in terms of these basic operations. Analogous to the logics of binary relations, formulas of the logic of typed relations are built with typed relational terms and a string of object variables and/or constants of the appropriate length. We present a dual tableau for this logic and prove its completeness.

Next, following [BO97], we discuss a relational representation of database dependencies. All the typical dependencies can be expressed in terms of indiscernibility relations in the set of tuples of a relation in a relational database. Along these lines, any relation generated from indiscernibility relations with the operations from algebras of binary relations may be regarded as a generalized database dependency. This allows us to apply a rule extension of the dual tableau of logic RL(1, 1′) to the verification of these dependencies and their implications. Since indiscernibility relations are equivalence relations we have to add the rules reflecting reflexivity, symmetry, and transitivity to the rules of the system for RL(1, 1′). The dual tableau obtained in this way is sound and complete.

2 The Calculus of Typed Relations

Let Ω be an infinite set whose elements are referred to as attributes. To each a ∈ Ω there is associated a non-empty set D _a called the domain of attributea. Types of relations, usually denoted by capital letters A, B,…, etc., are finite subsets of Ω, including the empty set; clearly, if A and B are types, then A ∪B, A ∩ B, and A − B are types. A ⊎ B denotes the union of disjoint sets A′ and B′ obtained from A and B, respectively, by renaming their elements, if necessary. Consequently, card(A) = card(A′), card(B) = card(B′), and $A\prime \cap B\prime = \varnothing$. In particular, A ⊎ A is the union of two disjoint sets each of which has the same cardinality as A. This understanding of ⊎ allows us to assume that ⊎ is commutative and associative and that $A \uplus \varnothing = A$. It is a common practice in database systems to rename attributes as needed. To enable renaming, we assume that for every attribute a ∈ Ω, there are infinitely many attributes a _i such that ${D}_{{a}_{i}} = {D}_{a}$. When forming A ⊎ B, if a′ ∈ A′ and b′ ∈ B′ correspond to a ∈ A and b ∈ B, respectively, it is necessary that D _a′ = D _a and D _b′ = D _b . The set of all types will be denoted by ${\mathbb{T}}_{\Omega }$. Our definition of the disjoint union involves renaming implicitly.

Let D _A = ⋃{D _a : a ∈ A}; then in particular, ${D}_{\varnothing } = \varnothing$. A tuple of type A is a map u : A → D _A such that for every a ∈ A, u(a) ∈ D _a . The collection of all tuples of type A is called the relation 1^A; for each a ∈ Ω the collection of tuples of type {a} is denoted by 1^a. Let ${1}^{\varnothing } =\{ e\}$, where e is the empty tuple. For each a ∈ Ω, ${D}_{a}\neq \varnothing$; therefore ${1}^{a}\neq \varnothing$. Consequently, ${1}^{A}\neq \varnothing$ for all $A \in {\mathbb{T}}_{\Omega }$.

The above definitions imply that 1^{A ⊎ B} = { t : ∃u ∈ 1^A, ∃v ∈ 1^B such that if a ∈ A then t(a) = u(a) and if b ∈ B then t(b) = v(b)}. Observe that we have defined ⊎ so that 1^{A ⊎ B} = 1^{B ⊎ A}, 1^{A ⊎ (B ⊎ C)} = 1^{(A ⊎ B) ⊎ C}, and if B ⊆ A, then ${1}^{A} = {1}^{B\uplus (A-B)}$. We often denote tuples t ∈ 1^{A ⊎ B} by uv, and say t = uv, where u ∈ 1^A and v ∈ 1^B. Clearly, uv is a mapping, uv : A ⊎ B → D _{A ⊎ B} , where D _{A ⊎ B} = D _A ∪D _B . Our notation uv is analogous to the relational database notation for unions of sets of attributes: uv is the union of two mappings, where a mapping is understood as a set of pairs satisfying the well known functionality requirements. Thus uv = vu; similarly, (uv)w = u(vw). Finally, for any $A \in {\mathbb{T}}_{\Omega }$, and for any u ∈ 1^A, $ue = eu = u$.

A relation R is said to be of type Awhenever it is a subset of 1^A.

The basic operations on typed relations are as follows. Let $A,B \in {\mathbb{T}}_{\Omega }$:

• Intersection ( ∩ )

  Let R, S ⊆ 1^A; then $R {\cap }^{A}S{ \mathrm{df} \atop =} \{u \in {1}^{A} : u \in R$ and u ∈ S}.

• Projection (Π)

  Let B ⊆ A and let R ⊆ 1^A; then ${\Pi }_{B}^{A}R{ \mathrm{df} \atop =} \{u \in {1}^{B} : \exists v \in {1}^{A-B}$ such that uv ∈ R}.

• Product ( ×)

  Let R ⊆ 1^A and S ⊆ 1^B; then $R {\times }^{A\uplus B}S{ \mathrm{df} \atop =} \{uv \in {1}^{A\uplus B} : u \in {1}^{A}$, v ∈ 1^B, u ∈ R, and v ∈ S}.

• Complement ( − )

  Let R ⊆ 1^A; then ${-}^{A}R{ \mathrm{df} \atop =} ({1}^{A}-R) =\{ u \in {1}^{A} : u\not\in R\}$.

We define the constant 0^A as follows: ${0}^{A}{ \mathrm{df} \atop =} { -}^{A}{1}^{A}$. Clearly, ${0}^{A} = \varnothing$ for all $A \in {\mathbb{T}}_{\Omega }$. Union, R ∪^A S, and complement of S with respect to R, R − ^A S, can easily be defined in terms of the above operations. Other operations are typically used in databases; we give their set theoretic definition and the corresponding expression in terms of the above four basic operations:

• Natural join ( ⊳ ⊲ )

  Let R ⊆ 1^A and S ⊆ 1^B; then R ⊳ ⊲ ^{A ∪B} $S{ \mathrm{df} \atop =} \{uvw \in {1}^{A\cup B} : u \in {1}^{A-(A\cap B)}$, v ∈ 1^{A ∩ B}, w ∈ 1^{B − (A ∩ B)}, uv ∈ R, and vw ∈ S}.

  The corresponding term of the calculus of typed relations is:

  $$(R {\times }^{A\uplus (B-(A\cap B))}{1}^{B-(A\cap B)}) {\cap }^{A\uplus (B-(A\cap B))}(S {\times }^{B\uplus (A-(B\cap A))}{1}^{A-(B\cap A)}).$$

• Division ( ÷ )

  Let B ⊆ A, let R ⊆ 1^A and S ⊆ 1^B, S≠0^B; then $R {\div }_{B}^{A}S{ \mathrm{df} \atop =} \{t \in {1}^{A-B} : \forall s \in S$, ts ∈ R}.

  The representation in the calculus of typed relations is:

  $${\Pi }_{A-B}^{A}R{-}^{A-B}({\Pi }_{ A-B}^{A}(({\Pi }_{ A-B}^{A}R {\times }^{(A-B)\uplus B}S){-}^{A}R)).$$

A general notion of selection operation, namely select S in R is defined for any B ⊆ A, S ⊆ 1^B and R ⊆ 1^A as follows. Its application to such S and R yields the tuples ut ∈ R such that u ∈ S. We give its set theoretic definition and an equivalent formulation in terms of the four basic operations:

• Selection (σ)

  Let B ⊆ A, let R ⊆ 1^A and let S ⊆ 1^B; then ${\sigma }_{B}^{A}(S,R){ \mathrm{df} \atop =} \{ut \in {1}^{A} : u \in {1}^{B}$, t ∈ 1^{A − B}, u ∈ S, and ut ∈ R}.

  The representation in the calculus of typed relations is:

  $$(S {\times }^{B\uplus (A-B)}{1}^{A-B}) {\cap }^{A}R.$$

Now, we define a binary operation, ${\odot }_{a,b}$, which is useful to represent entailment. Let R, S ⊆ 1^A and let a, b ∈ A, a≠b. Then:

$$R {\odot }_{a,b}S{ \mathrm{df} \atop =} ({1}^{A-\{a,b\}} \times {\Pi }_{ a}^{A}R) \times {\Pi }_{ b}^{A}S.$$

In [IL84] it is shown that the operations of Codd’s relational algebra [Cod70] may be defined in terms of intersection, complement, and cylindrification. It follows that Codd’s relational algebra can be treated as a disguised version of cylindric set algebra. The approach to relational databases via cylindrification operation has the advantage that all operations are total, since all relations are of the same type. The disadvantage of this approach is that all relations are forced to be of the same arity, and in real-life databases query checking is computationally more efficient if we use relations with varying arities. Moreover, there is no completeness theorem for the cylindrical version of relational database theory. For this reason, we choose to develop a typed calculus, with the four basic operations defined above. Other operations definable in terms of intersection, projection, product, and complement include the update operations (see [Ngu91]) and other joins.

We can easily see that with typed relations we can express all of the fundamental notions of relational database theory: schema – a set of attributes, relation over a schema – a typed relation, tuple and database – a set of typed relations. We often write explicitly the types of both the operations and their argument relations, although some typing information may be redundant.

Some arithmetics laws of the calculus of typed relations are listed in the following propositions. The proofs can be found in [MO06].

Proposition 6.2.1 (Properties of Π _B ^A).

For all $A,B \in {\mathbb{T}}_{\Omega }$ and for all R,S ⊆ 1 ^A , if B ⊆ A, then:

• 1. ${\Pi }_{B}^{A}({1}^{A}) = {1}^{B},$ ${\Pi }_{B}^{A}({0}^{A}) = {0}^{B};$

• 2. ${\Pi }_{B}^{A}(R {\cup }^{A}S) = {\Pi }_{B}^{A}R {\cup }^{B}{\Pi }_{B}^{A}S$;

• 3. ${\Pi }_{B}^{A}(R {\cap }^{A}S) \subseteq {\Pi }_{B}^{A}R {\cap }^{B}{\Pi }_{B}^{A}S$;

• 4. ${-}^{B}{\Pi }_{B}^{A}R \subseteq {\Pi }_{B}^{A}({-}^{A}R)$;

• 5. ${\Pi }_{A}^{A}R = R$;

• 6. ${\Pi }_{\varnothing }^{A}R \subseteq {1}^{\varnothing }$ and if R≠0 ^A , then ${\Pi }_{\varnothing }^{A}R = {1}^{\varnothing }$.

Proposition 6.2.2 (Properties of ${\sigma }_{B}^{A}$).

For all $A,B \in {\mathbb{T}}_{\Omega }$ , for all R ⊆ 1 ^A , and for all S,T ⊆ 1 ^B , if B ⊆ A, then:

• 1. ${\sigma }_{B}^{A}(S {\cup }^{B}T,R) = {\sigma }_{B}^{A}(S,R) {\cup }^{A}{\sigma }_{B}^{A}(T,R)$

• 2. ${\sigma }_{B}^{A}(S,R {\cup }^{A}T) = {\sigma }_{B}^{A}(S,R) {\cup }^{A}{\sigma }_{B}^{A}(S,T)$;

• 3. ${\sigma }_{B}^{A}(S {\cap }^{B}T,R) = {\sigma }_{B}^{A}(S,R) {\cap }^{A}{\sigma }_{B}^{A}(T,R)$

• 4. ${\sigma }_{B}^{A}(S,R {\cap }^{A}T) = {\sigma }_{B}^{A}(S,R) {\cap }^{A}{\sigma }_{B}^{A}(S,T)$;

• 5. ${\sigma }_{B}^{A}({-}^{B}S,R) \subseteq {-}^{A}{\sigma }_{B}^{A}(S,R)$

• 6. ${\sigma }_{B}^{A}({0}^{B},R) = {0}^{A}$;

• 7. ${\sigma }_{B}^{A}(S,{0}^{A}) = {0}^{A}$ .

Proposition 6.2.3 (Properties of ×).

For all $A,B,C \in {\mathbb{T}}_{\Omega }$ , for all R ∈ 1 ^A ,S ∈ 1 ^B ,T ∈ 1 ^C :

• 1. R × ^A⊎B S = S × ^B⊎A R;

• 2. (R × ^A⊎B S) × ^(A⊎B)⊎C T = R × ^A⊎(B⊎C) (S × ^B⊎C T).

Proposition 6.2.4 (Properties of ⊳ ⊲ ).

For all $A,B,C \in {\mathbb{T}}_{\Omega }$ , for all R ∈ 1 ^A ,S ∈ 1 ^B ,T ∈ 1 ^C :

• 1. R ⊳ ⊲ ^A∪A R = R;

• 2. R ⊳ ⊲ ^A∪B S = S ⊳ ⊲ ^B∪A R;

• 3. (R ⊳ ⊲ ^A∪B S) ⊳ ⊲ ^(A∪B)∪C T = R ⊳ ⊲ ^A∪(B∪C) (S ⊳ ⊲ ^B∪C T).

Proposition 6.2.5 (Properties of ⊙ _{a, b} ).

For all $A \in {\mathbb{T}}_{\Omega }$ , for all a,b ∈ A such that a≠b, and for all R,S,P,Q ⊆ 1 ^A , if $Q\neq \varnothing$ , then:

• 1. ${1}^{A} {\odot }_{a,b}{-}^{A}{1}^{A} = {0}^{A}$

• 2. $({1}^{A} {\odot }_{a,b}{-}^{A}{1}^{A}) {\odot }_{a,b}{1}^{A} = {0}^{A}$;

• 3. ${1}^{A} {\odot }_{a,b}{1}^{A} = {1}^{A}$

• 4. $R {\odot }_{a,b}{0}^{A} = {0}^{A} = {0}^{A} {\odot }_{a,b}R$;

• 5. R ⊙ _a,b (S ⊙ _a,b P) = (R ⊙ _a,b S) ⊙ _a,b P.

Let R, S ⊆ 1^A and let a, b ∈ A, a≠b. Then:

$$R {\supset }_{a,b}^{A}S{ \mathrm{df} \atop =} (({1}^{A} {\odot }_{ a,b}{-}^{A}R) {\odot }_{ a,b}{1}^{A}) {\cup }^{A}S.$$

Proposition 6.2.6.

Let R,S ⊆ 1 ^A . Then for all a,b ∈ A such that a≠b the following hold:

• 1. ${1}^{A} {\supset }_{a,b}^{A}S = S$

• 2. If R≠1 ^A , then $R {\supset }_{a,b}^{A}S = {1}^{A}$.

The following theorem shows that entailment in the calculus of typed relations can be expressed in its language.

Theorem 6.2.1.

Let A,B ⊂ Ω, let R ⊆ 1 ^A ,S ⊆ 1 ^B , a,b ∈ A,a≠b, and let C = A ∪ B. Then the following are equivalent:

• 1. R = 1 ^A implies S = 1 ^B

• 2. $R \times {1}^{C-A} {\supset }_{a,b}^{C}S \times {1}^{C-B} = {1}^{C}$.

3 Logic of Typed Relations

In this section we present a language of typed relations introduced in [MO06] whose intended models are databases. Let Ω be a set of attributes as defined in Sect. 6.2. Let ${\mathbb{T}}_{\Omega }$ be a set of types based on Ω. Then the expressions of the language of the logic TRL of typed relations over Ω are built from the following pairwise disjoint sets of symbols:

• {e} – the empty tuple;

• ${\mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{a}$ – an infinite set of object variables of type a, for each a ∈ Ω; by ${\mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{A}$ we denote the set ${\bigcup \nolimits }_{a\in A}{\mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{a}$, where $A \in {\mathbb{T}}_{\Omega }$;

• ${\mathbb{O}\mathbb{C}}_{\mathsf{TRL}}^{a}$ – a set of object constants of type a, for each a ∈ Ω; by ${\mathbb{O}\mathbb{C}}_{\mathsf{TRL}}^{A}$ we denote the set ${\bigcup \nolimits }_{a\in A}{\mathbb{O}\mathbb{C}}_{\mathsf{TRL}}^{A}$, where $A \in {\mathbb{T}}_{\Omega }$;

• ${\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{a} ={ \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{a} \cup { \mathbb{O}\mathbb{C}}_{\mathsf{TRL}}^{a}$; by ${\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$ we denote the set ${\bigcup \nolimits }_{a\in A}{\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{a}$, where $A \in {\mathbb{T}}_{\Omega }$; we presume ${\mathbb{O}\mathbb{C}}_{\mathsf{TRL}}^{\varnothing } =\{ e\}$;

• ${\mathbb{R}\mathbb{V}}_{\mathsf{TRL}}^{A}$ – a set of relational variables of type A, for each $A \in {\mathbb{T}}_{\Omega }$;

• ${\mathbb{R}\mathbb{C}}_{\mathsf{TRL}}^{A}$ – a set of relational constants of type A, for each $A \in {\mathbb{T}}_{\Omega }$; ${0}^{A},{1}^{A} \in { \mathbb{R}\mathbb{C}}_{\mathsf{TRL}}^{A}$;

• ${\mathbb{O}\mathbb{P}}_{\mathsf{TRL}}$ – a set of operations of varying arities such that: for every k-ary operation $\# \in { \mathbb{O}\mathbb{P}}_{\mathsf{TRL}}$, k ≥ 1, there is associated a sequence τ(#) = (A ₁, …, A _k , A) of k + 1 elements of ${\mathbb{T}}_{\Omega }$, where A _i is the type of the ith argument of #, i = 1, …, k, A is the type of the expression obtained by performing the operation #.

We presume: ${\mathbb{O}\mathbb{P}}_{\mathsf{TRL}} \supseteq \{ {\Pi }_{B}^{A}$, ∪^A, ∩ ^A, − ^A, ×^{A ⊎ C} : $A,B,C \in {\mathbb{T}}_{\Omega },$ B ⊆ A}, where $\tau ({\Pi }_{B}^{A}) = (A,B)$, $\tau ({\cup }^{A}) = \tau ({\cap }^{A}) = (A,A,A)$, $\tau ({-}^{A}) = (A,A)$, and τ( ×^{A ⊎ C}) = (A, C, A ⊎ C). It follows that $\tau ({\div }_{B}^{A}) = (A,B,A-B)$, τ(σ _B ^A) = (B, A, A), and for any $D \in {\mathbb{T}}_{\Omega }$, τ( ⊳ ⊲ ^{A ∪D}) = (A, D, A ∪D).

Assumptions concerning the elements of ${\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A\uplus B}$ and ${\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{\varnothing }$, analogous to the corresponding assumptions on the set of tuples, are assumed to hold. It follows from the definitions that ${\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A\uplus B} ={ \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B\uplus A}$ and ${\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{(A\uplus B)\uplus C} ={ \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A\uplus (B\uplus C)}$. As with the notation defined for the tuples, if u denotes a variable from ${\mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{A\uplus B}$, it may be replaced by an expression vw, where $v \in { \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{A}$ and $w \in { \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{B}$. The set of atomic terms ${\mathbb{R}\mathbb{A}}_{\mathsf{TRL}}^{A}$ is defined as the set ${\mathbb{R}\mathbb{V}}_{\mathsf{TRL}}^{A} \cup { \mathbb{R}\mathbb{C}}_{\mathsf{TRL}}^{A}$. We assume that for all A, ${\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}\neq \varnothing$ and ${\mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{\varnothing } =\{ e\}$.

For each $A \in {\mathbb{T}}_{\Omega }$, the set of terms of type A, ${\mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$, is the smallest set such that:

• ${\mathbb{R}\mathbb{A}}_{\mathsf{TRL}}^{A} \subseteq { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$;

• If $\# \in { \mathbb{O}\mathbb{P}}_{\mathsf{TRL}}$ is such that τ(#) = (A ₁, …, A _m , A) and ${F}_{i} \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{{A}_{i}}$, i = 1, …, m, then $\#({F}_{1},\ldots,{F}_{m}) \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$.

A formula in the language of the logic TRL of typed relations over Ω is an expression of the form F(u), where $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$ and $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$, for some $A \in {\mathbb{T}}_{\Omega }$.

A TRL-model for the language of the logic TRL of typed relations over Ω is a system $\mathcal{M} =\{\{ \mathcal{A} : \mathcal{A}\in {\mathbb{T}}_{\otimes }\},\{{\mathcal{U}}^{\mathcal{A}} : \mathcal{A}\in {\mathbb{T}}_{\otimes }\},\rceil,\Updownarrow \}$, where U ^A is a non-empty set of tuples of type A, ${U}^{\varnothing } =\{ e\}$, and m is a meaning function subject to the following conditions:

• If $u \in { \mathbb{O}\mathbb{C}}_{\mathsf{TRL}}^{A}$, then m(u) ∈ U ^A and if u = vw, then m(u) = m(v)m(w); in addition, m(e) = e;

• If $R \in { \mathbb{R}\mathbb{A}}_{\mathsf{TRL}}^{A}$, then m(R) ⊆ U ^A; in particular, $m({0}^{A}) = \varnothing$ and m(1^A) = U ^A;

• If $\# \in { \mathbb{O}\mathbb{P}}_{\mathsf{TRL}}$ and τ(#) = (A ₁, …, A _k , A), then m(#) is a k-ary operation acting on relations of types A ₁, …, A _k and returning a relation of type A: $m(\#) : {2}^{{U}^{{A}_{1}} } \times \cdots \times {2}^{{U}^{{A}_{k}} } \rightarrow {2}^{{U}^{A} }$;

• m extends to all the compound relational terms as follows:

  if F = #(F ₁, …, F _k ), then m(F) = m(#)(m(F ₁), …, m(F _k )).

It is easy to see that each database over Ω determines a TRL-model.

A valuation in a TRL-model $\mathcal{M} =\{\{ \mathcal{A} : \mathcal{A}\in {\mathbb{T}}_{\otimes }\},\{{\mathcal{U}}^{\mathcal{A}} : \mathcal{A}\in {\mathbb{T}}_{\otimes }\},\rceil,\Updownarrow \}$ is a function $v: \bigcup \nolimits \{{ \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}: A \in {\mathbb{T}}_{\Omega }\} \rightarrow \bigcup \nolimits \{{U}^{A}: A \in {\mathbb{T}}_{\Omega }\}$ such that:

• If $u \in { \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{A}$, then v(u) ∈ U ^A;

• If $u \in { \mathbb{O}\mathbb{C}}_{\mathsf{TRL}}^{A}$, then v(u) = m(u);

• If $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$ and $w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B}$, then v(uw) = v(u)v(w).

It follows from the definition of tuple that v(ut) = v(tu), v((ut)w) = v(u(tw)), and $v(ue) = v(eu) = v(u)$.

Let $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$ and let $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$. The formula F(u) is said to be satisfied in a TRL-model $\mathcal{M}$ by a valuation v whenever v(u) ∈ m(F). We say that the formula F(u) is true in the model $\mathcal{M}$ if and only if it is satisfied by all valuations in $\mathcal{M}$. Therefore if $u \in { \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{A}$, then F(u) is true in the model $\mathcal{M}$ if and only if m(F) = U ^A. We say that F(u) is TRL-valid if it is true in all TRL-models.

4 Dual Tableau for the Logic of Typed Relations

We present a dual tableau for the language of typed relations whose semantics is determined by the class of TRL-models.

Decomposition rules have the following forms:

For all $F,G \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$, B ⊆ A, $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$, and $w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B},$

$$\begin{array}{ll} (\cup )\,\frac{(F {\cup }^{A}G)(u)} {F(u),G(u)} \qquad &\qquad (-\cup )\, \frac{{-}^{A}(F {\cup }^{A}G)(u)} {{-}^{A}F(u)\,\vert \,{-}^{A}G(u)} \\ (\cap )\,\frac{(F {\cap }^{A}G)(u)} {F(u)\,\vert \,G(u)} \qquad &\qquad (-\cap )\, \frac{{-}^{A}(F {\cap }^{A}G)(u)} {{-}^{A}F(u),{-}^{A}G(u)} \\ (-)\,\frac{{-}^{A}{-}^{A}F(u)} {F(u)} \\ (\Pi )\, \frac{({\Pi }_{B}^{A}F)(w)} {F(wt),({\Pi }_{B}^{A}F)(w)}\qquad t \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A-B}isanyobjectsymbol \\ (-\Pi )\,\frac{{-}^{B}({\Pi }_{B}^{A}F)(w)} {{-}^{A}F(wt)} \qquad t \in { \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{A-B}\mbox{ is a new object variable} \\ \end{array}$$

For all $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A},G \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{B},v \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A},w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B},$ and $z \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A-B},$

$$\begin{array}{ll} (\times )\,\frac{(F {\times }^{A\uplus B}G)(vw)} {F(v)\,\vert \,G(w)} \qquad &\qquad (-\times )\,\frac{{-}^{A\uplus B}(F {\times }^{A\uplus B}G)(vw)} {{-}^{A}F(v),{-}^{B}G(w)}\\ \end{array}$$

Specific rules have the following forms:

For all $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$, ${u}_{i} \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{{A}_{i}}$, A = A ₁ ⊎ … ⊎ A _n , 1 ≤ i ≤ n,

$$\begin{array}{l} (e)\, \frac{F({u}_{1}\ldots {u}_{i-1}(e{u}_{i})\ldots {u}_{n})} {F({u}_{1}\ldots {u}_{i-1}{u}_{i}\ldots {u}_{n}),F({u}_{1}\ldots {u}_{i-1}(e{u}_{i})\ldots {u}_{n})} \\ (e)\, \frac{F({u}_{1}\ldots {u}_{i-1}{u}_{i}\ldots {u}_{n})} {F({u}_{1}\ldots {u}_{i-1}(e{u}_{i})\ldots {u}_{n}),F({u}_{1}\ldots {u}_{i-1}{u}_{i}\ldots {u}_{n})} \\ (\pi )\, \frac{F({u}_{1}\ldots {u}_{n})} {F({u}_{\pi (1)}\ldots {u}_{\pi (n)})} \\ \qquad \mbox{ where }\pi \mbox{ is a permutation on}\{1,\ldots,n\} \\ (\uplus )\, \frac{F({u}_{1}\ldots {u}_{n})} {F({u}_{1}\ldots {u}_{i-1}{v}_{1}{v}_{2}{u}_{i+1}\ldots {u}_{n}),F({u}_{1}\ldots {u}_{n})} \\ \qquad {A}_{i} = {B}_{1} \uplus {B}_{2}, \\ \qquad {v}_{1} \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{{B}_{1}},{v}_{2} \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{{B}_{2}}\mbox{ are any object symbols} \end{array}$$

The rules (e) and (e′) reflect the interpretation of e as the empty tuple, the rule (π) reflects the fact that objects can be permuted without changing the meaning of a formula, and the rule ( ⊎ ) reflects the fact that any variable can be split into components in such a way that its type is preserved. The language includes variables of the empty type so that the rule ⊎ holds for all types.

A set of TRL-formulas is said to be TRL-axiomatic whenever it includes either of the sets of the following forms:

For any $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$, $R \in { \mathbb{R}\mathbb{A}}_{\mathsf{TRL}}^{A}$, and $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$, F≠0^A,

• (Ax1) {R(u), ( − ^A R)(u)};

• (Ax2) {1^A(u)};

• (Ax3) { − ^A0^A(u)};

• (Ax4) $\{({\Pi }_{\varnothing }^{A}F)(e)\}$.

Rules for the defined operations may be given explicitly using their set theoretic formulation. We present some examples below.

Let $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A},G \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{B}$, B ⊆ A, $w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B}$, $t \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A-B}$, then:

$$\begin{array}{ll} (\sigma )\,\frac{({\sigma }_{B}^{A}(G,F))(wt)} {G(w)\,\vert \,F(wt)} \qquad &\qquad (-\sigma )\,\frac{{-}^{A}({\sigma }_{B}^{A}(G,F))(wt)} {{-}^{B}G(w),{-}^{A}F(wt)} \end{array}$$

if, in addition, B≠∅, then:

$$\begin{array}{l} (\div )\, \frac{(F {\div }_{B}^{A}G)(t)} {{-}^{B}G(w),F(tw)}\quad w \in { \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{B}\mbox{ is a new object variable} \\ (-\div )\, \frac{{-}^{A-B}(F {\div }_{B}^{A}G)(t)} {G(w),{-}^{A-B}(F {\div }_{B}^{A}G)(t)\,\vert \,{-}^{A}F(tw),{-}^{A-B}(F {\div }_{B}^{A}G)(t)} \\ \qquad w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B}\mbox{ is any object symbol} \end{array}$$

Let $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A},G \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{B}$, $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A-(A\cap B)}$, $v \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A\cap B}$, $w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B-(A\cap B)}$, then:

$$\begin{array}{ll} (\vartriangleright \vartriangleleft )\,\frac{(F{\vartriangleright \vartriangleleft }^{A\cup B}G)(uvw)} {F(uv)\,\vert \,G(vw)} \qquad &\qquad (-\vartriangleright \vartriangleleft )\,\frac{{-}^{A\cup B}(F{\vartriangleright \vartriangleleft }^{A\cup B}G)(uvw)} {{-}^{A}F(uv),{-}^{B}G(vw)}\\ \end{array}$$

As usual, a TRL-set is a finite set of TRL-formulas such that the first-order disjunction of its members is true in all TRL-models. Correctness of a rule is defined in a similar way as in the relational logics of classical algebras of binary relations (see Sect. 2.4).

Proposition 6.4.1.

• 1. The TRL-rules are TRL-correct;

• 2. The TRL-axiomatic sets are TRL-sets.

Proof.

By way of example, we show correctness of the rules ( − Π) and (e).

• ( − Π) Let X be a finite set of TRL-formulas and let t be such that t≠ w and it does not occur in X. Assume X ∪{ − ^B(Π _B ^A F)(w)} is a TRL-set. Suppose X ∪{ − ^A F(wt)} is not a TRL-set. Then, there exist a TRL-model $\mathcal{M}$ and a valuation v in $\mathcal{M}$ such that for every φ ∈ X ∪{ − ^A F(wt)}, $\mathcal{M},\sqsubseteq \nvDash \varphi$, which means that v(w)v(t) ∈ m(F), where v(w) ∈ 1^B and v(t) ∈ 1^{A − B}. Since X ∪{ − ^B(Π _B ^A F)(w)} is a TRL-set, $\mathcal{M},\sqsubseteq \models {-}^{\mathcal{B}}({\prod}_{\mathcal{B}}^{\mathcal{A}}\mathcal{F})(\sqsupseteq )$. Thus, for every u ∈ 1^{A − B}, v(w)u ∉ m(F), a contradiction. Now, assume that X ∪{ − ^A F(wt)} is a TRL-set. Then for every TRL-model $\mathcal{M}$ and for every valuation v in $\mathcal{M}$, either there exists φ ∈ X such that $\mathcal{M},\sqsubseteq \models \varphi$ or $\mathcal{M},\sqsubseteq \models {-}^{\mathcal{A}}\mathcal{F}(\sqsupseteq \sqcup )$. By the assumption on variable t, it follows that either there exists φ ∈ X such that $\mathcal{M},\sqsubseteq \models \varphi$ or for every u ∈ 1^{A − B}, v(w)u ∉ m(F). Hence, $X \cup \{{-}^{B}({\Pi }_{B}^{A}F)(w)\}$ is a TRL-set.

• (e) Let X be a finite set of TRL-formulas. If X ∪{ F(u ₁ …u _{i − 1}(eu _i )…u _n )} is a TRL-set, then so is $X \cup \{ F({u}_{1}\ldots {u}_{i-1}(e{u}_{i})\ldots {u}_{n}),F({u}_{1}\ldots {u}_{i-1}{u}_{i}\ldots {u}_{n})\}$. Assume $X \cup \{ F({u}_{1}\ldots {u}_{i-1}(e{u}_{i})\ldots {u}_{n}),F({u}_{1}\ldots {u}_{i-1}{u}_{i}\ldots {u}_{n})\}$ is a TRL-set. Suppose X ∪{ F(u ₁ …u _{i − 1}(eu _i )…u _n )} is not a TRL-set. Then, there exist a TRL-model $\mathcal{M}$ and a valuation v in $\mathcal{M}$ such that for every φ ∈ X ∪{ F(u ₁ …u _{i − 1}(eu _i )…u _n )}, $\mathcal{M},\sqsubseteq \nvDash \varphi$, so v(u ₁)…v(u _{i − 1})v(eu _i )…v(u _n ) ∉ m(F). Since v(eu _i ) = v(u _i ), we obtain v(u ₁)…v(u _{i − 1})v(u _i )…v(u _n ) ∉ m(F). However, by the assumption $\mathcal{M},\sqsubseteq \models \mathcal{F}({\sqcap }_{\infty }\ldots {\sqcap }_{\rangle -\infty }{\sqcap }_{\rangle }\ldots {\sqcap }_{\setminus })$. Hence, v(u ₁)…v(u _{i − 1})v(u _i )…v(u _n ) ∈ m(F), a contradiction. □

The notions of a TRL-proof tree, a closed branch of such a tree, a closed TRL-proof tree, and TRL-provability are defined as in Sect. 2.4.

Due to Proposition 6.4.1, we obtain:

Proposition 6.4.2.

Let φ be a TRL-formula. If φ is TRL-provable, then it is TRL-valid.

Below we list the completion conditions that are specific for the logic TRL. The completion conditions for the rules ( ∩ ), ( − ∩ ), and ( − ) are as in Sect. 2.5.

For all $F,G \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$, B ⊆ A, $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$, and $w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B}$,

Cpl(Π) (resp. Cpl( − Π)) If (Π _B ^A F)(u) ∈ b (resp. ( − ^B Π _B ^A F)(u) ∈ b), then for every $t \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A-B}$, F(ut) ∈ b (resp. for some $t \in { \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{A-B}$, − ^A F(ut) ∈ b), obtained by an application of the rule (Π) (resp. ( − Π));For all $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$, $G \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{B}$, $v \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$, $w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B}$, and $z \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A-B}$,Cpl( ×) (resp. Cpl( − ×)) If (F ×^{A ⊎ B} G)(vw) ∈ b (resp. − ^{A ⊎ B}(F ×^{A ⊎ B} G)(vw) ∈ b), for some $v \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$ and $w \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{B}$, then either F(v) ∈ b or G(w) ∈ b (resp. both − ^A F(v) ∈ b and − ^B G(w) ∈ b), obtained by an application of the rule ( ×) (resp. ( − ×)); For all $F \in { \mathbb{R}\mathbb{T}}_{\mathsf{TRL}}^{A}$, ${u}_{i} \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{{A}_{i}}$, A = A ₁ ⊎ … ⊎ A _n , 1 ≤ i ≤ n,Cpl(e) If F(u ₁ …u _{i − 1}(eu _i )…u _n ) ∈ b, for n ≥ 1 and 1 ≤ i ≤ n, then F(u ₁ …u _{i − 1} u _i …u _n ) ∈ b, obtained by an application of the rule (e);Cpl(e′) If F(u ₁ …u _{i − 1}(u _i )…u _n ) ∈ b, for n ≥ 1 and 1 ≤ i ≤ n, then F(u ₁ …u _{i − 1}(eu _i )…u _n ) ∈ b, obtained by an application of the rule (e′);Cpl(π) If F(u ₁ …u _n ) ∈ b, then for any permutation π of the indices 1, …, n, F(u _π(1) …u _π(n)) ∈ b, obtained by an application of the rule (π);>Cpl( ⊎ ) If F(u ₁ …u _n ) ∈ b, for ${u}_{i} \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{{A}_{i}}$, 1 ≤ i ≤ n, and A _i = B ₁ ⊎ B ₂, then for all ${v}_{1} \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{{B}_{1}}$, ${v}_{2} \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{{B}_{2}}$, $F({u}_{1}\ldots {u}_{i-1}{v}_{1}{v}_{2}{u}_{i+1}\ldots {u}_{n}) \in b$, obtained by an application of the rule ( ⊎ ).

The notions of a complete TRL-proof tree and an open branch of a TRL-proof tree are defined as in RL-logic (see Sect. 2.5). Due to the forms of the rules of TRL-dual tableau, we can prove that whenever a branch of a TRL-proof tree contains both of the formulas R(u) and ( − ^A R)(u), for $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$ and for an atomic $R \in { \mathbb{R}\mathbb{A}}_{\mathsf{TRL}}^{A}$, then the branch can be closed. Thus, the closed branch property can be proved.

Let b be an open branch of a TRL-proof tree. A branch structure

$${\mathcal{M}}^{\lfloor } =\{\{ \mathcal{A} : \mathcal{A}\in {\mathbb{T}}_{ \otimes }\},\{{\mathcal{U}}^{\mathcal{A}} : \mathcal{A}\in {\mathbb{T}}_{ \otimes }\},{\rceil }^{\lfloor },{\Updownarrow }^{\lfloor }\}$$

is defined as follows:

• ${U}^{A} ={ \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A}$, for any $\varnothing \neq A \in {\mathbb{T}}_{\Omega }$;

• ${U}^{\varnothing } =\{ e\}$ and ${e}^{b} = {m}^{b}(e) = e$;

• m ^b(c) = c, for every $c \in { \mathbb{O}\mathbb{C}}_{\mathsf{TRL}}^{A}$;

• ${m}^{b}(R) =\{ u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A} : R(u)\not\in b\}$, for every $R \in \ { \mathbb{R}\mathbb{A}}_{\mathsf{TRL}}^{A}$;

• For every $\# \in { \mathbb{O}\mathbb{P}}_{\mathsf{TRL}}$, m ^b(#) is defined as in TRL-models;

• m ^b extends to all the compound relational terms as in TRL-models.

It is easy to see that the branch structure defined above is a TRL-model. Hence, the branch model property holds. Let v ^b be a valuation in ${\mathcal{M}}^{\lfloor }$ such that v ^b(u) = u, for every $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}$.

Proposition 6.4.3 (Satisfaction in Branch Model Property).

For every open branch b of a TRL-proof tree and for every TRL-formula φ, if ${\mathcal{M}}^{\lfloor },{\sqsubseteq }^{\lfloor }\models \varphi$ , then φ∉b.

Proof.

The proof is by induction on the complexity of formulas. The atomic case can be proved as in Sect. 2.5, it uses the closed branch property. By way of example, we show the proposition for some compound formulas that are specific for TRL-logic.

Let $\varphi = ({\Pi }_{B}^{A}F)(w)$. Assume ${\mathcal{M}}^{\lfloor },{\sqsubseteq }^{\lfloor }\models ({\prod}_{\mathcal{B}}^{\mathcal{A}}\mathcal{F})(\sqsupseteq )$. Then there exists $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A-B}$ such that wu ∈ m ^b(F), and by the induction hypothesis, F(wu) ∉ b. Suppose $({\Pi }_{B}^{A}F)(w) \in b$. Then by the completion condition Cpl(Π), for every $u \in { \mathbb{O}\mathbb{S}}_{\mathsf{TRL}}^{A-B}$, F(wu) ∈ b, a contradiction.

Let $\varphi ={ -}^{A\uplus B}(F {\times }^{A\uplus B}G)(uw)$. Assume ${\mathcal{M}}^{\lfloor },{\sqsubseteq }^{\lfloor }\models {-}^{\mathcal{A}\uplus \mathcal{B}}(\mathcal{F}{\times }^{\mathcal{A}\uplus \mathcal{B}}\mathcal{G})(\sqcap \sqsupseteq )$. Then u ∉ m ^b(F) or w ∉ m ^b(G). Suppose − ^{A ⊎ B}(F ×^{A ⊎ B} G)(uw) ∈ b. Then, by the completion condition Cpl( − ×), − ^A F(u) ∈ b and − ^B G(w) ∈ b. Thus, by the induction hypothesis, u ∈ m ^b(F) and w ∈ m ^b(G), a contradiction. □

As usual, Proposition 6.4.3 enables us to prove:

Proposition 6.4.4.

Let φ be a TRL-formula. If φ is TRL-valid, then it is TRL-provable.

Finally, by Propositions 6.4.2 and 6.4.4, we have:

Theorem 6.4.1 (Soundness and Completeness of TRL).

For every TRL-formula φ, the following conditions are equivalent:

• 1. φ is TRL-valid;

• 2. φ is TRL-provable.

Some other relational approaches to databases can be found in [DM01, Mac00, Mac01].

Theorem 6.4.2.

• 1. Each of the Boolean algebra identities is TRL-provable;

• 2. Each of the expressions in Propositions 6.2.1, …, 6.2.5 is TRL-provable.

Example.

Consider the following property: if R is a relation of type A and B ⊆ A, then $R \subseteq ({\Pi }_{B}^{A}R) {\times }^{B\uplus (A-B)}{1}^{A-B}$. To prove that this property holds in all TRL-models it suffices to demonstrate that the formula $(R {\rightarrow }^{A}({\Pi }_{B}^{A}R) {\times }^{B\uplus (A-B)}{1}^{A-B})(u)$ is TRL-provable, where F → ^A G is defined as − ^A F ∪^A G. If $u \in { \mathbb{O}\mathbb{V}}_{\mathsf{TRL}}^{A}$, then (F → ^A G)(u) is TRL-valid iff for all TRL-models, m(F) ⊆ m(G). Figure 6.1 presents a TRL-proof of the formula

$$({-}^{A}R {\cup }^{A}({\Pi }_{ B}^{A}R) {\times }^{B\uplus (A-B)}{1}^{A-B})(u).$$

Figure 6.2 shows TRL-provability of the formula:

$$(T {\times }^{{A}_{1}\uplus {A}_{2} }{\sigma }_{B}^{{A}_{2} }(S,R) {\rightarrow }^{{A}_{1}\uplus {A}_{2} }{\sigma }_{B}^{{A}_{1}\uplus {A}_{2} }(S,T \times R))(u).$$

Fig. 6.1

A TRL-proof of the formula $({-}^{A}R {\cup }^{A}({\Pi }_{B}^{A}R) {\times }^{B\uplus (A-B)}{1}^{A-B})(u)$

Fig. 6.2

A TRL-proof of $({-}^{{A}_{1}\uplus {A}_{2}}(T {\times }^{{A}_{1}\uplus {A}_{2}}{\sigma }_{B}^{{A}_{2}}(S,R)) {\cup }^{{A}_{1}\uplus {A}_{2}}{\sigma }_{B}^{{A}_{1}\uplus {A}_{2}}(S,T \times R))(u)$

Its equivalent form is:

$$({-}^{{A}_{1}\uplus {A}_{2} }(T {\times }^{{A}_{1}\uplus {A}_{2} }{\sigma }_{B}^{{A}_{2} }(S,R)) {\cup }^{{A}_{1}\uplus {A}_{2} }{\sigma }_{B}^{{A}_{1}\uplus {A}_{2} }(S,T \times R))(u).$$

5 Relational Representation of Database Dependencies

Let a universe Ω of attributes be given and let A be a finite subset of Ω. We recall that a database relation over A, R ^A, is a set of tuples of type A. We shall often omit the index A in the name of a database relation. Given a database relation R, by AT _R we mean the underlying set of attributes. Following the usual database notation, for a subset B of A and for a tuple t ∈ R ^A we write t[B] for a restriction of t (as a mapping) to set B.

Given a database relation R over A and a subset B of A, we define an indiscernibility relation in R as follows. For any t, u ∈ R, (t, u) ∈ ind(B) iff t[B] = u[B].

Example.

Consider relation R defined in Table 6.1. Indiscernibility relation ind(a) determined by attribute a consists of the following pairs of tuples:

$$\mathit{ind}(a) =\{ ({t}_{1},{t}_{1}),({t}_{2},{t}_{2}),({t}_{3},{t}_{3}),({t}_{4},{t}_{4}),({t}_{1},{t}_{4}),({t}_{2},{t}_{3}),({t}_{3},{t}_{2})\}.$$

Indiscernibility relation ind(bc) determined by attributes b and c consists of the following tuples:

$$\mathit{ind}(bc) =\{ ({t}_{1},{t}_{1}),({t}_{2},{t}_{2}),({t}_{3},{t}_{3}),({t}_{4},{t}_{4}),({t}_{1},{t}_{2}),({t}_{2},{t}_{1})\}.$$

In the following proposition we recall some basic properties of the indiscernibility relations.

Proposition 6.5.1.

For any database relation R and for all A,B ⊆ AT _R , the following conditions are satisfied:

• 1. ind(AT_R) ={ (t,t) : t ∈ R}, $\mathit{ind}(\varnothing ) = R \times R$;

• 2. ind(A ∪ B) = ind(A) ∩ ind(B);

• 3. ind(A) ∪ ind(B) ⊆ind(A) ; ind(B);

• 4. If A ⊆ B, then ind(B) ⊆ ind(A);

• 5. ind(A) = ⋂ { ind(a) : a ∈ A}.

Let a database relation R be given. Various attribute dependencies in R can be defined in terms of indiscernibility relations. We recall the standard definitions of those dependencies and their relational representation developed in [Orł87]. Let A, B, C ⊆ AT _R .

Table 6.1 A database relation

Functional Dependency

A → B holds in R iff for all tuples t,u ∈ R, if t[A] = u[A], then t[B] = u[B].

Proposition 6.5.2.

The following conditions are equivalent:

• 1. Functional dependency A → B holds in R;

• 2. ind(A) ⊆ ind(B).

Multivalued Dependency

A → → B holds in R iff for all tuples t, u ∈ R, if t[A] = u[A], then there exists t′ ∈ R such that the following conditions are satisfied:

• t′[A ∪B] = t[A ∪B];

• $t\prime[A{T}_{R}-(A \cup B)] = u[A{T}_{R}-(A \cup B)]$.

Proposition 6.5.3.

The following conditions are equivalent:

• 1. Multivalued dependency A →→ B holds in R;

• 2. ind(A) ⊆ ind(A ∪ B) ; ind(AT _R −(A ∪ B)).

Embedded Multivalued Dependency

A → → B | C holds in R iff A →→ B holds in the set {t[A ∪ B ∪ C] : t ∈ R}.

Proposition 6.5.4.

The following conditions are equivalent:

• 1. Embedded multivalued dependency A →→ B|C holds in R;

• 2. ind(A) ⊆ ind(A ∪ B) ; ind((C−(A ∪ B))).

Decomposition

(A, B) holds in R iff A ∪B = AT _R and for all t, u ∈ R, if t[A ∩ B] = u[A ∩ B], then there exists t′ ∈ R such that t′[A] = t[A] and t′[B] = u[B].

Proposition 6.5.5.

The following conditions are equivalent:

• 1. Decomposition (A,B) holds in R;

• 2. A ∪ B = AT _R and ind(A ∩ B) ⊆ ind(A) ; ind(B).

Join Dependency

^∗(A ₁, …, A _n ) holds in R iff A ₁, …, A _n = AT _R and R is the join of relations {t[A _i ] : t ∈ R}, for i = 1, …, n.

Proposition 6.5.6.

Join dependency ^∗ (A ₁ ,…,A _n ) holds in R implies ind(A₁ ∩… ∩ A_n) ⊆ ind(A ₁ ) ; … ; ind(A_n).

A dependency defined by the condition ind(A ₁ ∩ … ∩ A _n ) ⊆ ind(A ₁) ; … ; ind(A _n ), for A ₁, …, A _n such that A ₁ ∪…A _n = AT _R , is called a generalized join dependency.

We conclude that given a database relation R, any relation generated from relations ind(a), for a ∈ AT _R , with the operations of algebras of binary relations may be viewed as a kind of database dependency.

6 Dual Tableau for Database Dependencies

Due to the relational representation of database dependencies we can verify dependencies and implications of dependencies within a relational logic. The logic adequate for this purpose, RL _EQ , is obtained from RL(1, 1′) by restricting its class of models to the models where the meanings of relation variables are assumed to be equivalence relations. This assumption is in agreement with the fact that dependencies are represented with relations generated by indiscernibility relations which in turn are equivalence relations.

A relational logic obtained from RL _EQ by restricting its class of models to the models whose universes are sets of tuples of a database relation, is referred to as a relational logic with database models, RL _DEP .

Given a database relation R, an RL _DEP -model is a structure $\mathcal{M} = (\mathcal{R},\Updownarrow )$ such that:

• R is the set of tuples;

• m(P) ∈ {ind _R (a) : a ∈ AT _R }, for every relational variable P;

• m(1) = R ×R;

• m(1′) = Id _R .

Since AT _R is finite for any database relation R, the image under m of the set of relational variables is finite in any database model. Clearly, RL _DEP -model is an RL _EQ -model. On the other hand, for every RL _EQ -model we can construct an RL _DEP -model such that the models verify the same formulas, that is we have the following proposition.

Proposition 6.6.1.

• 1. For every RL _DEP -model there exists an RL _EQ -model $\mathcal{M} = (\mathcal{U},\Updownarrow )$ such that m({P : P is a relational variable}) is finite and the models verify the same formulas;

• 2. For every RL _EQ -model $\mathcal{M} = (\mathcal{U},\Updownarrow )$, if m({P : P is a relational variable}) is finite, then there is an RL _DEP -model such that the models verify the same formulas.

Proof.

The part 1. of the proposition is obvious in view of the corresponding definitions. To prove 2. we construct an RL _DEP -model determined by the given RL _EQ -model $\mathcal{M} = (\mathcal{U},\Updownarrow )$. We define a database relation R so that AT _R = m({P : P is a relational variable}), that is the attributes of R are the equivalence relations determined by the meanings of relational variables. It follows that for every relational variable P, {m(PDV is an attribute; it will be denoted by a _P . For every x ∈ U we define a tuple t _x as ${t}_{x}({a}_{P}) =\| {x\|}_{m(P)}$ which assigns an equivalence class of x with respect to the relation m(P) to the attribute a _P . Then we have (t _x , t _y ) ∈ ind _R (a _P ) iff (x, y) ∈ m(P). It is easy to check that the sets of formulas true in these models coincide. □

A dual tableau for the logic RL _EQ consists of the rules and axiomatic sets of RL(1, 1′)-dual tableau endowed with the rules which reflect interpretation of relational variables as equivalence relations:

For all object symbols x and y and for any relational variable P,

$$\begin{array}{ll} (\mbox{ ref }P)\, \frac{xPy} {x1y,xPy}\qquad &\qquad (\mbox{ sym }P)\,\frac{xPy} {yPx} \\ (\mbox{ tran }P)\, \frac{xPy} {xPz,xPy\,\vert \,zPy,xPy} &z\mbox{ is any object symbol} \end{array}$$

The notions of an RL _EQ -set and RL _EQ -correctness of a rule are defined as in Sect. 2.4.

Theorem 6.6.1 (Correspondence).

Let $\mathcal{K}$ be a class of RL(1,1′)-models. Then $\mathcal{K}$ is a class of RL _EQ -models iff the rules (ref P), (sym P), and (tran P) are $\mathcal{K}$-correct.

Proof.

Let $\mathcal{K}$ be a class of RL(1, 1′)-models.

• ( → ) Assume that $\mathcal{K}$ is the class of RL _EQ -models. By way of example, we show correctness of the rule (tran P). Let X be any finite set of formulas. Clearly, if X ∪{ xPy} is an RL _EQ -set, then so are X ∪{ xPz, xPy} and X ∪{ zPy, xPy}. Now, assume that X ∪{ xPz, xPy} and X ∪{ zPy, xPy} are RL _EQ -sets, and suppose X ∪{ xPy} is not an RL _EQ -set. Then, there exist an RL _EQ -model $\mathcal{M} = (\mathcal{U},\Updownarrow )$ and a valuation v in $\mathcal{M}$ such that for every φ ∈ X ∪{ xPy}, $\mathcal{M},\sqsubseteq \nvDash \varphi$. Thus, (v(x), v(y)) ∉ m(P). By the assumption, $\mathcal{M},\sqsubseteq \models \S \mathcal{P}\ddag$ and $\mathcal{M},\sqsubseteq \models \ddag \mathcal{P}\dag$. Hence, (v(x), v(z)) ∈ m(P) and (v(z), v(y)) ∈ m(P), and by transitivity of m(P), (v(x), v(y)) ∈ m(P), a contradiction. Therefore, the rule (tran P) is RL _EQ -correct.

• ( ← ) Assume that for all relational variables P the rules (ref P), (sym P), and (tran P) are $\mathcal{K}$-correct. We show that for every relational variable P, and for every $\mathcal{K}$-model $\mathcal{M} = (\mathcal{U},\Updownarrow )$, m(P) is an equivalence relation. By way of example, we show transitivity of the relation m(P). Observe that due to correctness of rule (tran P), for every finite set X of relational formulas the following holds: X ∪{ xPy} is a $\mathcal{K}$-set iff X ∪{ xPz, xPy} and X ∪{ zPy, xPy} are $\mathcal{K}$-sets. Let $X{ \mathrm{df} \atop =} \{x-Pz,z-Py\}$. Since {xPz, xPy, $x-Pz,z-Py\}$ and $\{zPy,xPy,x-Pz,z-Py\}$ are $\mathcal{K}$-sets, then so is the set {xPy, x − Pz, z − Py}. Thus, for every $\mathcal{K}$-model $\mathcal{M} = (\mathcal{U},\Updownarrow )$ and for every valuation v in $\mathcal{M}$, if (v(x), v(z)) ∈ m(P) and (v(z), v(y)) ∈ m(P), then (v(x), v(y)) ∈ m(P). Hence, m(P) is transitive in every $\mathcal{K}$-model. □

Proposition 6.6.2.

• 1. The RL _EQ -rules are RL _EQ -correct;

• 2. The RL _EQ -axiomatic sets are RL _EQ -sets.

Correctness of the rules (ref P), (sym P), and (tran P) follows from Theorem 6.6.1. Correctness of the remaining rules can be proved as in RL(1, 1′)-logic (see Sects. 2.5 and 2.7).

The notions of an RL _EQ -proof tree, a closed branch of such a tree, a closed RL _EQ -proof tree, and RL _EQ -provability are defined as in Sect. 2.4.

The completion conditions that are specific for RL _EQ -dual tableau are:

For all object symbols x and y and for any relational variable P,

Cpl(ref P) If xPy ∈ b, then x1′y ∈ b, obtained by an application of the rule (ref P);Cpl(sym P) If xPy ∈ b, then yPx ∈ b, obtained by an application of the rule (sym P);Cpl(tran P) If xPy ∈ b, then for every object symbol z, either xPz ∈ b or zPy ∈ b, obtained by an application of the rule (tran P).

The notions of a complete RL _EQ -proof tree and an open branch of an RL _EQ -proof tree are defined as in RL-logic (see Sect. 2.5).

Although, the rule (sym P) does not preserve the formulas of the form xPy, for a relational variable P, we can show that the closed branch property holds. The proof is similar to the proof of Proposition 2.8.1.

The branch structure ${\mathcal{M}}^{\lfloor } = ({\mathcal{U}}^{\lfloor },{\Updownarrow }^{\lfloor })$ determined by an open branch b of an RL _EQ -proof tree is defined as in the completeness proof of RL-dual tableau, in particular m ^b(P) = { (x, y) ∈ U ^b ×U ^b : xPy ∉ b}, for every relational variable P (see Sect. 2.6, p. 44).

Proposition 6.6.3 (Branch Model Property).

For every open branch b of an RL _EQ -proof tree, ${\mathcal{M}}^{\lfloor }$ is an RL _EQ -model.

Proof.

Following the method of proving the branch model property in the completeness proof of RL(1, 1′)-dual tableau (see Sects. 2.5 and 2.7), we show that ${\mathcal{M}}^{\lfloor }$ satisfies specific properties of RL _EQ -models, namely, we need to prove that every relation m ^b(P) is an equivalence relation. For reflexivity, assume that (x, y) ∈ m ^b(1′) and suppose that (x, y) ∉ m ^b(P). Then x1′y ∉ b and xPy ∈ b. By the completion condition Cpl(ref P), x1′y ∈ b, a contradiction. For symmetry, assume that (x, y) ∈ m ^b(P) and suppose that (y, x) ∉ m ^b(P). Then xPy ∉ b and yPx ∈ b. By the completion condition Cpl(sym R), xPy ∈ b, a contradiction. For transitivity, assume that (x, y) ∈ m ^b(P) and (y, z) ∈ m ^b(P), that is xPy ∉ b and yPz ∉ b. Suppose that (x, z) ∉ m ^b(P). Then xPz ∈ b, and by the completion condition Cpl(tran P), either xPy ∈ b or yPz ∈ b, a contradiction. □

Now, the completeness of the RL _EQ -dual tableau can be proved as in RL(1, 1′)-logic.

Theorem 6.6.2 (Soundness and Completeness of RL _EQ ).

For every RL _EQ -formula φ, the following conditions are equivalent:

• 1. φ is RL _EQ -valid;

• 2. φ is RL _EQ -provable.

Theorems on entailment, model checking, and verification of satisfaction presented in Sects. 2.11, 3.4, and 3.5, respectively, apply to RL _EQ -logic.

Example.

We show that the set {A → C, CD → AE} of functional dependencies implies dependency AD → E. By Propositions 6.5.1(2.) and 6.5.2, it suffices to show that ind(A) ⊆ ind(C) and ind(C) ∩ ind(D) ⊆ ind(A) ∩ ind(E) entail ind(A) ∩ ind(D) ⊆ ind(E). In what follows, for the sake of simplicity, we shall write Z instead of ind(Z) for Z = A, C, D, E. We apply the method of verification of entailment presented in Sect. 2.11, thus we verify RL _EQ -validity of the following relational formula:

$$x[1\,;\,-[(-A \cup C) \cap (-(C \cap D) \cup (A \cap E))]\,;\,1 \cup (-(A \cap D) \cup E)]y.$$

Figure 6.3 presents its RL _EQ -proof.

Fig. 6.3

An RL _EQ -proof showing that {A → C, CD → AE} implies AD → E