7 RC Simulates RA.We now show that DRC (and hence TRC) is at least as expressive as RA. Thatis, given an RA expression E that mentions at most C, there is an equivalentDRC expression E!that mentions at most C.Just as in the previous section, we must deal with the technical issue that DRCis defined by recursion on formulas rather than on expressions. We show thatfor every RA expression E there exists a DRC formula F that simulates E inthe sense that, when F is embedded in a simple DRC expression E!, then Eand E!are equivalent.To simplify the presentation, we assume the set of variables names usable inDRC expressions includes all the attribute names usable in RA expressions.Lemma: For every RA expression E(A1. . . Ak) there exists a DRC formulaF with F V (F ) = {A1, . . . , Ak} and(∀r) [[E]](r) = [[{"A1: A1, . . . , Ak: Ak# | F }]](r)Proof: We use induction on the structure of E.Case E = E1∪ E2: Inductively there exist E1and E2such that[[E1]](r) = [[{". . . Ai: Ai. . .# | F1]](r)[[E2]](r) = [[{". . . Ai: Ai. . .# | F2]](r)Note the attributes on which E1and E2are defined are the same. Let F beF1∨ F2; then[[E1∪ E2]](r) = [[{". . . Ai: Ai. . .# | F1∨ F2]](r)as desired.Case E = E1− E2: This case is similar to ∪, with F = F1∧ ¬F2.Case E = E1(A1. . . Aj) × E2(Aj+1. . . Ak): Note that the sets {A1. . . Aj}and {Aj+1. . . Ak} are disjoint (the × operator is Cartesian product, not join).As usual the formulas F1and F2exist by induction. Let F = F1∧ F2; then[[E1× E2]](r) = [[{"A1: A1. . . Ak: Ak# | F1∧ F2}]](r)as required.22Case E = ρA1"→BE1: We may assume without loss of generality that therenamed attribute appears first. Also, note that B does not occur among A2,. . . , Ak. Inductively there exists F1such that[[E]](r) = [[{"A1: A1. . . Ak: Ak# | F1]](r)We must construct a formula equivalent to F1but with the free variable A1replaced by B. This can be accomplished with an existential and an equalityconjunct. LetF = (∃A1)( (A1= B) ∧ F1)The free variables of F are {B, A2, . . . , Ak}, and[[E]](r) = [[{"B, A2: A2. . . Ak: Ak# | F }]](r)as required.Case E = πA1...AjE1(A1. . . Ak): This case is similar to renaming. Induc-tively, the usual formula F1exists, and we eliminate free variables Aj+1throughAkby existential quantification. LetF = (∃Aj+1. . . ∃Ak)(F1)Then[[E1× E2]](r) = [[{"A1: A1. . . Aj: Aj# | F }]](r)as required.Case E = σpE1: Inductively, the usual formula F1exists such that[[E1]](r) = [[{". . . Ai: Ai. . .# | F1]](r)The select condition p is a propositional formula with free variables among A1through Ak, and so can be interpreted as a DRC formula in the same freevariable environment used for F1. LetF = (F1∧ p)23Then[[σpE1]](r) = [[{"A1: A1. . . Aj: Aj# | (F1∧ p)}]](r)as required.!This demonstrates that DRC (or TRC) is at least as expressive as RA. Thepossibility remains that DRC/TRC is strictly more expressive. We deal withthis next.8 Domain Independence (Safety)Our ultimate goal is to show that RA and RC are in some sense equally expres-sive. There is an easy technical issue we must dispose of first.Let R be the database scheme {R1(A)}, a single relation with a single column.Consider the following simple example query in DRC.[[{"B : x# | x = c}]](r) = {"B : c#}This holds whether or not the value c occurs anywhere in the instance r, becausethe quantified variable x ranges over all values in D. Thus, the theoremD([[E]](r))⊆ Drwhich we proved earlier for RA expressions, fails for RC expressions.Next consider the two examples[[{"B : x# | x = x}]](r) = {"B : v# | v ∈ D}and[[{"B : x# | ¬("A : x# ∈ R1)}]](r) = {"B : v# | v ∈ (D − Dr)}The result in the first example is a complete copy of D; in the second caseit is the complement of relation r1in D. Thus, both finiteness and domain-independence, which we proved earlier for RA expressions, fail for RC expres-sions. A domain-dependent expression like the examples above is sometimescalled unsafe.24Relation Constants For the problem illustrated by the first example abovethere is a simple technical fix. We augment RA expressions with relation con-stants as follows:E ::= {"A1: c1, . . . , Ak: ck#}Attr(E) = A1. . . Ak[[E]](r) = {"A1: c1, . . . , Ak: ck#}Since RA includes a union operator, expressions for relations with only a singletuple are sufficient. We then augment the definition of “E mentions at mostC” in a straightforward way to include constants appearing in relation-valuedexpressions as well as those appearing in select conditions. It is easy to see thatthe revised theoremD[[E]](r)⊆ (Dr∪ C)holds, where E is a RA expression that mentions at most C.Domain Independence Having added relation constants to the RA lan-guage, we shall now argue that the only remaining issue is domain dependence,illustrated by the second and third examples above.We showed above that for every DRC expresison E(D)there is an equivalentTRC expression E(T ), and vice versa. Since domain-independence is a seman-tic notion, E(T )is domain-independent if and only if E(D)is. Let DRC-DIbe the language consisting of just the domain-independent DRC expressions;and let TRC-DI be the domain-independent TRC expressions. Ignore for themoment the question of how to decide whether a particular expression is domain-independent or not. Clearly DRC-DI and TRC-DI are equivalent. Moreover,both languages are at least as expressive as RA: we showed above that for everyRA expression E(A)there is an equivalent TRC expression E(T )and an equiv-alent DRC expression E(D); since E(A)is domain-independent, E(T )and E(D)must be domain-independent also.We shall complete the argument to show that DRC-DI (TRC-DI) and RA haveexactly the same expressive power, by showing that for every DRC-DI expressionthere is an equivalent RA expression. Formally, we show:Theorem: For any DRC formula F on free variables {X1, . . . , Xk} mentioningat most C, there exists an RA expression E with attributes {X1, . . . , Xk} andmentioning at most C such that[[E]](r) = [[{"X1: X1. . . Xk: Xk#} | F ]]Dr∪C(r)25for all instances r. Note that F and E mention at most C; the case that Cincludes some constants not mentioned in E or F is explicitly allowed. In fact,it is necessary to make the inductive hypothesis apply to subformulas in theproof below.Proof: As usual, we assume all DRC variable names can be used as attributenames, and proceed by induction on F .First we make an observation. Given the set of constants C and a any attributename A, we can construct an