4
$\begingroup$

I'm looking for whatever work may exist, or thoughts people have, on the question of whether/to what extent there exist(s) one or more canonical form(s) to which relational algebra expressions may be reduced.

I'm investigating the feasability of building a relational query optimizer which allows hand-writing of query plans but proves (or assists the user in proving) that the plan satisfies the query.

If there isn't a (usefully non-enormous) canonical form, then I wouldn't know the first thing about how to attack the problem. I suppose read up on Coq or Isabelle, work on translating my equivalence question into theorem prover's language, and work on providing a less-grad-school-required interface that exposes (relevant parts of) the theorem prover's output.

If there is a canonical form that doesn't tend to blow up to enormous sizes, then of course its a much easier problem.

$\endgroup$
  • $\begingroup$ While I don't have a specific answer, the PODS community (PODS is the main database theory conference) has done a ton of work on these sorts of questions, and and it might be worth looking into. A good start might be the Database theory book by Abiteboul et al $\endgroup$ – Suresh Venkat Oct 6 '11 at 15:24
  • $\begingroup$ @Suresh: The Alice book doesn't really go in depth. Query rewrites there are just ad-hoc rules. $\endgroup$ – Tegiri Nenashi Oct 6 '11 at 18:04
4
$\begingroup$

There are canonical forms, but there are not unique canonical forms. Roughly, the idea is to use observe that sets form a monad and use the equational theory of Moggi's monadic metalanguage as a well-behaved IR for optimizing queries. See Torsten Grust's PhD thesis, Comprehending Queries.

More recently, the Ferry Project has been investigating integrating programming languages with query languages.

$\endgroup$
  • $\begingroup$ Great stuff. This Comprehending Queries paper is excellent. Thanks. $\endgroup$ – Doug McClean Oct 7 '11 at 13:26
  • $\begingroup$ Ferry Project link appears broken. $\endgroup$ – I. J. Kennedy Jun 27 '12 at 1:27
3
$\begingroup$

Relational Lattice is axiomatic foundation for Relational Algebra. Predictably, query transformations reduce to equational reasoning in that axiom system. Here are examples:

Many others like commutativity and associativity of [relational] join operation, or permutting selection via join are trivial in the sense that they are fundamental lattice laws.

You mentioned theorem provers; not surprisingly, some research has been facilitated with Prover9.

$\endgroup$
  • $\begingroup$ Wow, this is really interesting stuff, thanks Tegiri! $\endgroup$ – Doug McClean Oct 7 '11 at 13:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.