## Non Associative Operations in Relational Lattice

Recently, the name “Relational Lattice” has become a misnomer. There is a wealth of other operations, so the situation resembles famous: “Who ordered all these?”. First, there is intriguing parallel to Relation algebras first mentioned in Litak et.al.. The additional operations introduced in my last year paper make even more convincing case.

In Relation algebras there are two sets of operations: Logical and Relative. Logical operations are familiar Boolean conjunction, disjunction and negation. Each logical operation has its relative counterpart: relative product (aka composition), relative sum, and converse. Relational Lattice operation structure is similar: loosely speaking each Boolean operation splits into the two: there are two versions of conjunction — natural join and inner join –, two version of disjunction — generalized union and outer union (aka Date&Darwen <OR>) — and, finally, two versions of negation: complement (aka Date&Darwen <NOT>) and inversion. The two distinguished constants — true and false — bifurcate into four elements in each system: Relation Algebra and Relational Lattice.

Since the logical part of Relation Algebra honors all Boolean algebra axioms, it is stronger than Boolean algebra. In contrast, Relational lattice is weaker than Boolean algebra, notably, the distributive law for natural join and generalized union is broken. If one tries to combine natural join with outer union, then this pair satisfies distributive law, however, don’t honor absorption. The inner join is the most enigmatic operation of all, because it is not even associative.

One may question utility of such operation, amplified by the fact that inner join can be represented in terms of “fundamental” operations: natural join and inner union. There are reasons, both practical and theoretical. On pragmatic side QBQL for SQL people lists two queries that are naturally expressed with such an operation. On theoretical side, this operation contribution is introduction of partial order.

Remember that each idempotent, commutative and associative binary operation gives rise to a partial order. We have three associative operations: natural join, inner union, and outer union generating potentially three different orders. It is well known that the orders produced by natural join and inner union coincide. It is the absorption law that makes it happen. Outer union doesn’t honor absorption law (in combination with none of the other operation), therefore, it generates a distinct [partial] order. Both orders pretends to be generalizations of subset relationship, however we’d argue that the one induced by the outer union is the least interesting one. The Relational Lattice identity

y + x = x <-> x' < y'.

is a consequence of relational lattice version of De Morgan’s law:

x' < y' <-> -- equational "<" definition
x' ^ y' = x' <-> -- De Morgan's law
(x + y)' = x' <-> -- Double Complement law
y + x = x

What about inner join — “*” –, can it give rise to some order? Non-associativity appears to be a snag, yet, it is easy to prove that the constraint

x * y = x.

is reflexive, antisymmetric, and transitive. Therefore, it is a partial order. Like outer union induced order, the inner join order can be expressed in terms of lattice one:

y * x = x <-> (x' v y)' < x'.

Inner join order can be expressed via alternative identity

y * x = x <-> (R11 ^ x) v (R00 ^ y) = x v y.

which left hand side expression mysteriously resembles Fundamental Decomposition Identity

x = (R11 ^ x) v (R00 ^ x).

Among various algebraic systems lack of associativity is rare. Jordan Algebras require commutativity and Jordan identity. For inner join, which is idempotent operation, Jordan identity

(x * y) * (x * x) = x * (y * (x * x).

collapses to

(x * y) * x = x * (y * x).

which further reduces to tautology due commutativity of inner join.

The other prominent non-associative commutative operation — composition — is another candidate to be organized into Jordan Algebra. Jordan identity in this case is not obvious, yet, it surrenders to brute force of Prover9. Here is Prover9 code:

% Language Options

op(300, postfix,      "`" ).
op(450, infix,      "/^" ).

formulas(assumptions).

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.

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).

x = (x ^ R00) v (x ^ R11).
R00 ^ (x v R11) = x ^ R00.

x` ^ x = R11 ^ x.
x` v x = R00 v x.

x /^ y = (R00 ^ (x` ^ y`)) v (y ^ x).

end_of_list.

formulas(goals).

(x /^ y) /^ (x /^ x) = x /^ (y /^ (x /^ x)).