Equational theories and database constraints

ABSTRACT

We present a novel way to formulate database dependencies as sentences of first-order logic, using equational statements instead of Horn clauses. Dependency implication is directly reduced to equational implication. Our approach is powerful enough to express functional and inclusion dependencies, which are the most common database constraints. We present a new proof procedure for these dependencies. We use our equational formulation to derive new upper and lower bounds for the complexity of their implication problems.

REFERENCES

• 1: Catriel Beeri , Philip A. Bernstein, Computational problems related to the design of normal form relational schemas, ACM Transactions on Database Systems (TODS), v.4 n.1, p.30-59, March 1979 [doi>10.1145/320064.320066]
• 2: Beeri, C. and Vardi, M.Y. "Formal Systems for Tuple and Equality Generating l)cpendencies". S/aIM Journal of Cornputing 13, I (February 1984), 76-98.,
• 3: Catriel Beeri , Moshe Y. Vardi, A Proof Procedure for Data Dependencies, Journal of the ACM (JACM), v.31 n.4, p.718-741, Oct. 1984 [doi>10.1145/1634.1636]
• 4: Birkhoff, G. "On the Structure of Abstract Algebras". Proceedings of. the Cambridge Philosophical Society 31, (1935).
• 5: Casanova, M.A., Fagin. R. and Papadimitfiou, C.H. "Inclusion Dependencies and'!'heir Interaction with Functional Dependencies". jountal o/Computer and System Sciences 28, 1 (February 1984), 29-59,.
• 6: M. A. Casanova , V. M. P. Vidal, Towards a sound view integration methodology, Proceedings of the 2nd ACM SIGACT-SIGMOD symposium on Principles of database systems, March 21-23, 1983, Atlanta, Georgia [doi>10.1145/588058.588065]
• 7: Chandra, A.K. and Vardi, M.Y. The Implication Problem for Functional and Inclusion Dependencies is Undecidable. iBM Tech. Rep, RC 9980, , , 1983,
• 8: Cosmadakis, $.S. Equational Theories ctnd Dalabase Constraints, Ph.D. 'I~., Massachusetts Institute of Technology, 1985,
• 9: Stavros S. Cosmadakis , Paris C. Kanellakis, Functional and inclusion dependencies a graph theoretic approach, Proceedings of the 3rd ACM SIGACT-SIGMOD symposium on Principles of database systems, April 02-04, 1984, Waterloo, Ontario, Canada [doi>10.1145/588011.588016]
• 10: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 11: Ronald Fagin, Horn clauses and database dependencies, Journal of the ACM (JACM), v.29 n.4, p.952-985, Oct. 1982 [doi>10.1145/322344.322347]
• 12: Forgaard, R. and Guttag, J.V. "REVE: A l'erm Rewriting System Generator with Failure Resistant Knuth-Bendiix". Proctedings of an NSF ff/3rkshop on the Rewrite Rule Laboratory (A{:ri11984), $-31.
• 13: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 14: Huet. G. and Oppen, D. Equations and Rewrite Rules: a Survey. In Fomtal Languages: Perspectives a~td Open Problems,, Eds., Academic Press. ,1980.
• 15: Johnson, D.S. and Klug, A. "Testing Containment of Conjunctive Queries Under Functional and Inclusion Dependencies". Journal of Computer and $),stem Sciences 28, 1 (February 1984). 167-189..
• 16: Paris C. Kanellakis , Stavros S. Cosmadakis , Moshe Y. Vardi, Unary inclusion dependencies have polynomial time inference problems, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.264-277, December 1983 [doi>10.1145/800061.808756]
• 17: Knuth, D.E. and Bendix, P.B.. Volume: Simple Word Problems in Universal Algebras. In Cotnptttational Problems bt dbstracl Algebra,, Eds., Pergamon, Oxford, 1970, ch..
• 18: Dexter Kozen, Complexity of finitely presented algebras, Proceedings of the ninth annual ACM symposium on Theory of computing, p.164-177, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803406]
• 19: Kent Laver , Alberto O. Mendelzon , Marc H. Graham, Functional dependencies on cyclic database schemes, Proceedings of the 1983 ACM SIGMOD international conference on Management of data, May 23-26, 1983, San Jose, California
• 20: Lewis. H.R. and Papadimitriou, C.H.. Elements of the Theory of Computation. Prentice-Hall, Inc,, Eaglewood Cliffs, New Jersey, 1981,,
• 21: Minsky, M.L. "Recursive Unsolvability of Posfs Problem of"Tag" and Other Topics in the Theory of Turing Machines". Annals of Mathematics 74, 3 ( 1961)..
• 22: John C. Mitchell, The implication problem for functional and inclusion dependencies, Information and Control, v.56 n.3, p.154-173, March 1983 [doi>10.1016/S0019-9958(83)80002-3]
• 23: E.L. Post. "Recursive Unsolvability of a Problem of Thue". Journal of Symbolic Logic 13, (1947).
• 24: Edward Sciore, Inclusion dependencies and the universal instance, Proceedings of the 2nd ACM SIGACT-SIGMOD symposium on Principles of database systems, March 21-23, 1983, Atlanta, Georgia [doi>10.1145/588058.588066]
• 25: Jeffrey D. Ullman, Principles of Database Systems, W. H. Freeman & Co., New York, NY, 1983
• 26: Yannakakis, M. and Papadimitriou C.H. "Algebraic Dependencies". J. Comput. Systems Sci. 21,1 (August 1982), 2-41.

INDEX TERMS

Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES

General Terms:
Theory, Verification