<p>There are canonical forms, but there are not <em>unique</em> 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, <a href="http://www.inf.uni-konstanz.de/dbis/publications/download/TG-GI00.pdf" rel="nofollow"><em>Comprehending Queries</em></a>. </p>

<p>More recently, <a href="http://www.pathfinder-xquery.org/research/ferry" rel="nofollow">the Ferry Project</a> has been investigating integrating programming languages with query languages. </p>

CC BY-SA 3.0
2011-10-07T13:26:31.880Z
Great stuff. This Comprehending Queries paper is excellent. Thanks.
Doug McClean
CC BY-SA 3.0
2012-06-27T01:27:54.417Z
Ferry Project link appears broken.
I. J. Kennedy
CC BY-SA 3.0
2011-10-07T06:12:18.053Z
2011-10-07T06:12:18.053Z
Neel Krishnaswami
<p><em>Relational Lattice</em> is axiomatic foundation for <em>Relational Algebra</em>. Predictably, query transformations reduce to equational reasoning in that axiom system. Here are examples:</p>

<ul>
<li><a href="http://arxiv.org/ftp/cs/papers/0603/0603044.pdf" rel="nofollow">Push-select-via-project</a> </li>
<li><a href="http://vadimtropashko.wordpress.com/relational-lattice/the-laws-of-renaming/" rel="nofollow">Renaming</a></li>
</ul>

<p>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.</p>

<p>You mentioned theorem provers; not surprisingly, some research has been facilitated with <em>Prover9</em>.</p>

CC BY-SA 3.0
2011-10-07T13:21:47.500Z
Wow, this is really interesting stuff, thanks Tegiri!
Doug McClean
CC BY-SA 3.0
2011-10-06T17:41:59.367Z
2011-10-06T18:00:21.013Z
2011-10-06T18:00:21.013Z
Tegiri Nenashi
<p>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.</p>

<p>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.</p>

<p>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.</p>

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

CC BY-SA 3.0
2011-10-06T15:24:13.350Z
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
Suresh Venkat
CC BY-SA 3.0
2011-10-06T18:04:03.800Z
@Suresh: The Alice book doesn't really go in depth. Query rewrites there are just ad-hoc rules.
Tegiri Nenashi
<db.databases><relational-structures><normalization>
Canonical forms for relational algebra expressions
Doug McClean
# Canonical forms for relational algebra expressions

(Asked by: username_0 on 2011-10-06)

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.

**Tags:** db.databases, relational-structures, normalization
> **Comments:**
> **username_1**: 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  
> **username_2**: @Suresh: The Alice book doesn't really go in depth. Query rewrites there are just ad-hoc rules.  

---

## 2 answers

### Answer by username_3 on 2011-10-07. Score: 4

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*](http://www.inf.uni-konstanz.de/dbis/publications/download/TG-GI00.pdf).

More recently, [the Ferry Project](http://www.pathfinder-xquery.org/research/ferry) has been investigating integrating programming languages with query languages.

> **Comments:**
> **username_0**: Great stuff. This Comprehending Queries paper is excellent. Thanks.  
> **username_4**: Ferry Project link appears broken.  

---

### Answer by username_2 on 2011-10-06. Score: 3

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

* [Push-select-via-project](http://arxiv.org/ftp/cs/papers/0603/0603044.pdf)
* [Renaming](http://vadimtropashko.wordpress.com/relational-lattice/the-laws-of-renaming/)

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

> **Comments:**
> **username_0**: Wow, this is really interesting stuff, thanks Tegiri!  

---

