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.

Improve this question
$\endgroup$
2
  • $\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, 2011 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, 2011 at 18:04

2 Answers 2

Reset to default
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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Great stuff. This Comprehending Queries paper is excellent. Thanks. $\endgroup$
    – Doug McClean
    Oct 7, 2011 at 13:26
  • $\begingroup$ Ferry Project link appears broken. $\endgroup$
    – I. J. Kennedy
    Jun 27, 2012 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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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