Abstract:
The natural join and the inner union operations combine relations
(tables) of a database.
Tropashko and Spight realized that these two operations are the meet
and join operations in a class of lattices, known by now as the
relational lattices. They proposed then lattice theory as an algebraic
approach to the theory of databases, alternative to the relational
algebra. Previous works proved that the quasiequational theory of
these lattices - that is, the set of definite Horn sentences valid in
all the relational lattices - is undecidable, even when the signature is
restricted to the pure lattice signature.
In this talk I'll argue that injective generalized ultrametric spaces
on a powerset algebra yield duals for these lattices. In particular,
I'll argue that ideas stemming from the theory of generalized
ultrametric spaces are the keys to prove that the equational theory of
relational lattices is decidable - by finding a finite countermodel of
bounded size.
Namely, we provide an algorithm to decide if two lattice theoretic
terms t, s are made equal under all intepretations in some relational
lattice. We achieve this goal by showing that if an inclusion t ≤ s
fails in any of these lattices, then it fails in a relational lattice
whose size is bound by a triple exponential function of the sizes of t
and s.