Canonical forms for relational algebra expressions 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.
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.