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.