Renaming is an intuitive operation, although somewhat obscure from mathematical perspective. Indeed, mathematics don’t make much ado about renaming variables: it is generally assumed that variable names are not important, and that variables themselves can be renamed at will (subject to common-sense restrictions). It is Relational Algebra that elevated renaming into first-rank operation. There renaming is both explicit and honors several query transformation laws. This article casts Relational Lattice perspective into renaming.
Basic Renaming properties
Relational algebra wikipedia web page lists the following renaming properties
Let’s rewrite these equalities in Relational Lattice / QBQL terms:
(R /^ "a=b") /^ "b=c" = R /^ "a=c".
(R /^ "a=b") /^ "c=d" = (R /^ "c=d") /^ "a=b".
/^ is set intersection join operation, and
"a=b" is an identity relation with attributes
b. Set intersection join is a natural join projected into the set of distinct relation attributes. QBQL queries in the other articles at this site should convince the reader that set intersection join is at least as common and important as natural join. Set intersection join resembles composition operation from the Algebra of Dyadic Relations, hence we’ll carry it over to our field (i.e. Algebra of Relations with Named Attributes).
Let’s leverage commutativity of composition, and rewrite the second equality into the form that would make the issue more transparent:
("a=b" /^ R) /^ "c=d" = "a=b" /^ (R /^ "c=d").
A similar trick with the first equality and leveraging the identity
"a=b" /^ "b=c" = "a=c".
demonstrates that both properties of renaming operation are essentially associativity laws of composition in disguise. Unfortunately, composition doesn’t honor associativity in general.
If the three relations
z have no attributes in common, then composition is associative. Formally:
R00 ^ ((x v y) v z) = R00 -> x /^ (y /^ z) = (x /^ y) /^ z.
R00 is the empty relation with empty set of attributes. This is exactly what is needed to prove renaming properties. In the first case, the identity relations
"b=c" have common attribute
b, but relation
R is not supposed to have it. In the second case, the identity relations
"c=d" don’t have any common attributes to begin with.
Let’s try establishing conditional associativity formally: could it be proved from relational lattice axioms? We have general lattice axioms
x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.
x v y = y v x.
(x v y) v z = x v (y v z).
x v (x ^ y) = x.
amended with three axioms borrowed from the Litak et.al. paper
x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))).
(x ^ y) v (x ^ z) = x ^ ( ((x v z) ^ y) v ((x v y) ^ z) ).
(R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y).
Next, we need to introduce universal relation
R11 captured with laws of Fundamental Decomposition Identity and its “dual”
x = (x ^ R00) v (x ^ R11).
R00 ^ (x v R11) = x ^ R00.
and inversion defined via
x` ^ x = R11 ^ x.
x` v x = R00 v x.
Now we have everything for defining composition:
x /^ y = (R00 ^ (x` ^ y`)) v (y ^ x).
Unfortunately, proving conditional associativity doesn’t turn to be a simple matter of copying and pasting these axioms and the goal into Prover9. The problem, at least in this form, seems to be too challenging for automated prover abilities. Mace4 established that the conditional associativity is valid for the domains up to size 20, at least.
The reader might wonder what was the purpose of this exercise; aren’t renaming rules obvious to begin with? Yes, they are. However, we learned several lessons here. From relational algebra perspective renaming rules (and others) are essentially ad-hoc. In one of the earlier papers we have already established that rewrite rules such as push-select-through-project can be firmly rooted into relational lattice foundation. We see that there is nothing special about renaming rules as well: the crux of the matter is associativity of some other operation. Knowing that renaming is essentially join with an identity relation and projecting away unwanted attribute, one may have suggest that properties of identity relation might be important too. This may have an implication for relational lattice theory, as perhaps we should add identity relation axioms as well. However, we have witnessed what really matters is the condition for the three relation not to have common attribute(s).
The rest of renaming properties
handles just as easily. Rewritten into relational lattice notation the above assertions become
"a=b" /^ (R ^ P') = ("a=b" /^ R) ^ ("a=b" /^ P').
"a=b" /^ (R v P) = ("a=b" /^ R) v ("a=b" /^ P).
"a=b" /^ (R ^ P) = ("a=b" /^ R) ^ ("a=b" /^ P).
In relational lattice we have the following analog of Spight Distributivity Criteria (SDC):
R00 ^ (x v y) = R00 ^ (x v z) -> x /^ (y v z) = (x /^ y) v (x /^ z).
P have the same set of attributes, hence they satisfy the premise of SDC, and distributivity of composition/renaming over union follows. Again, we see that the nature of the identity relation
"a=b" is irrelevant.
The other two identities reduce to distributivity of composition/renaming over join. Again, this is conditional property. It is easy to see that general distributivity of composition over join is invalid with relations on both sides of equality failing to have the same set of attributes! Run QBQL with formal assertion that distributivity has relations with the same set of attributes on each side of the equality, that is
(x /^ (y ^ z)) ^ R00 = ((x /^ y) ^ (x /^ z)) ^ R00.
and witness QBQL producing the following counterexample
z = [q] a ; y = [p] 1 ; x = [p] 1 ;
Previously cited wikipedia article claims modest distributivity of renaming over intersection, rather than more general distributivity of renaming over join. Both arguments of intersection operation having the same set of attributes in relational lattice terms is formal equality
y ^ R00 = z ^ R00.
which is stronger than the previous assertion that we refuted with QBQL. Neither of those premises fixes the distributivity law that we are after; we have to add the familiar condition that the three relations in questions have no attributes in common. Formally:
R00 ^ (x v y v z) = R00 &
(x /^ (y ^ z)) ^ R00 = ((x /^ y) ^ (x /^ z)) ^ R00 ->
x /^ (y ^ z) = (x /^ y) ^ (x /^ z).