About Codd's reduction algorithm

Question

Codd's Algorithm converts an expression in tuple relational calculus to Relational Algebra.

1. Is there a standard implementation of the algorithm?
2. Is this algorithm used anywhere? (It seems that the industry only needs SQL and variants, I'm not sure about database theorists in academia.)
3. What's the complexity of the reduction?

_{This was posted on SO over a year ago, but it didn't receive a good answer.}

Answer 1

This reduction is the constructive proof technique to show that a subset (named safe) Tuple Relational Calculus (TRC) is less expressive than Relational Algebra (RA). The other way being true too, Safe-TRC and RA have equivalent expressive power. See Theorem 5.3.10 for instance. The syntactic "safety" restriction ensures the domain independent property of the calculus and is needed.

In R-DBMS, SQL can be seen as the concrete (declarative) language for TRC. The RA counterpart is the procedural plan (a sequence of operations) in which an SQL expression is compiled to. So, the conversion is actually the formal description of the compilation process. Note that SQL introduces extensions like DISTINCT, ORDER BY, GROUP BY which are clearly outside the scope of TRC and RA theory.

I don't know the precise theoretical complexity of the conversion, but clearly it has to be "cheap". Photon Kolaitis states that it is linear.

I'm not aware of a proof-of-concept implementation of this algorithm.