Off-line and on-line algorithms for deducing equalities

ABSTRACT

The classical common subexpression problem in program optimization is the detection of identical subexpressions. Suppose we have some extra information and are given pairs of expressions ei1=ei2 which must have the same value, and expressions fj1≠fj2 which must have different values. We ask if as a result, h1=h2, or h1≠h2. This has been called the uniform word problem for finitely presented algebras, and has application in theorem-proving and code optimization. We show that such questions can be answered in O(nlogn) time, where n is the number of nodes in a graph representation of all relevant expressions. A linear time algorithm for detecting common subexpressions is derived. Algorithms which process equalities, inequalities and deductions on-line are discussed.

REFERENCES

• 1: {A} W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam (1954).
• 2: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 3: {AU} A. V. Aho and J. D. Ullman, Optimization of straight line programs, SIAM J. Computing 1, 1 (March 1972) 1-19.
• 4: Melvin A. Breuer, Generation of optimal code for expressions via factorization, Communications of the ACM, v.12 n.6, p.333-340, June 1969 [doi>10.1145/363011.363153]
• 5: E. Cardoza , R. Lipton , A. R. Meyer, Exponential space complete problems for Petri nets and commutative semigroups (Preliminary Report), Proceedings of the eighth annual ACM symposium on Theory of computing, p.50-54, May 03-05, 1976, Hershey, Pennsylvania, United States [doi>10.1145/800113.803630]
• 6: {CS} John Cocke and J. T. Schwartz, Programming Languages and Their Compilers Preliminary Notes, Second Revised Version, Courant Institute of Mathematical Sciences, New York, NY (April 1970).
• 7: {Cu} Karel Culik, Combinatorial problems in the theory of complexity of algorithmic nets without cycles for simple computers, Aplikace Matematiky 16 (1971) 188-202.
• 8: {DS} P. J. Downey and Ravi Sethi, Assignment commands and array structures, Proc. 17th Ann. Symposium on Foundations of Computer Science, (October 1976) 57-66.
• 9: {Go} D. I. Good, R. L. London and W. W. Bledsoe, An interactive program verification system, IEEE Trans. on Software Engineering SE-1 (March 1975) 59-67.
• 10: {H} J. E. Hopcroft, An n log n algorithm for minimizing states in a finite automaton, in Z. Kohavi and A. Paz (ed.) Theory of Machines and Computations, Academic Press, New York, NY (1971) 189-196.
• 11: {HK} J. E. Hopcroft and R. M. Karp, An algorithm for testing equivalence of finite automata, TR-71-114, Dept. of Computer Science, Cornell Univ. (1971); see description in Aho et. al. (1974) 143-145.
• 12: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 13: Donald E. Knuth, The art of computer programming, volume 3: (2nd ed.) sorting and searching, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1998
• 14: {KB} D. E. Knuth and P. B. Bendix, Simple word problems in universal algebras. In J. Leech, Ed., Computational Problems in Abstract Algebra, Pergamon Press, (1970).
• 15: 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]
• 16: {Ko2} D. Kozen, Lower bounds for natural proof systems, Proc. 18th Ann. Symp. on Foundations of Computer Science, (Oct. 1977), 254-266.
• 17: {L} D. S. Lankford, Canonical algebraic simplification in computational logic, Department of Mathematics report, Southwestern University, Georgetown, TX (1975).
• 18: {NO1} G. Nelson and D. Oppen, Fast decision algorithms based on union and find, Proc. 18th Ann. Symp. on Foundations of Computer Science, (Oct. 1977), 114-119.
• 19: {NO2} G. Nelson and D. Oppen, A simplifier for program manipulation, this proceedings.
• 20: M. S. Paterson , M. N. Wegman, Linear unification, Proceedings of the eighth annual ACM symposium on Theory of computing, p.181-186, May 03-05, 1976, Hershey, Pennsylvania, United States [doi>10.1145/800113.803646]
• 21: Hanan Samet, A normal form for compiler testing, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.155-162, August 15-17, 1977
• 22: Hanan Samet, Proving the correctness of heuristically optimized code, Communications of the ACM, v.21 n.7, p.570-582, July 1978 [doi>10.1145/359545.359569]
• 23: Ravi Sethi, Testing for the Church-Rosser Property, Journal of the ACM (JACM), v.21 n.4, p.671-679, Oct. 1974 [doi>10.1145/321850.321862]
• 24: {Se2} Ravi Sethi, Scheduling graphs on two processors, SIAM J. Computing 5, 1 (March 1976) 73-82.
• 25: {Sh} R. E. Shostak, An algorithm for reasoning about equality, Proc. of the Symp. on AI and Programming Languages, SIGPLAN Notices 12 (Aug. 1977), 155-162.
• 26: {Tarj1} R. E. Tarjan, Depth first search and linear graph algorithms, SIAM J. Computing 1, 2 (June 1972) 146-160.
• 27: Robert Endre Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM (JACM), v.22 n.2, p.215-225, April 1975 [doi>10.1145/321879.321884]
• 28: {Tarj3} R. E. Tarjan, private communication.
• 29: {Tars} A. Tarski, A. Mostowski and R. M. Robinson, Undecidable theories, North-Holland Publishing Co., Amsterdam (1953).