More Web Proxy on the site http://driver.im/

Article

Free access

Off-line and on-line algorithms for deducing equalities

Authors:

Ravi SethiAuthors Info & Claims

POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Pages 158 - 170

https://doi.org/10.1145/512760.512777

Published: 01 January 1978 Publication History

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 e_i1=e_i2 which must have the same value, and expressions f_j1≠f_j2 which must have different values. We ask if as a result, h₁=h₂, or h₁≠h₂. 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]

{AHU} A. V. Aho, J. E. Hopcroft, J. D. Ullman, The Design and Analysis of Computer Algorithms, Addison Wesley, Reading, Mass., (1974).

Digital Library

[3]

{AU} A. V. Aho and J. D. Ullman, Optimization of straight line programs, SIAM J. Computing 1, 1 (March 1972) 1-19.

[4]

{B} M. S. Breuer, Generation of optimal code for expressions via factorization, CACM 12, 6 (June 1969) 333-340.

Digital Library

[5]

{CLM} E. Cardoza, R. Lipton and A. R. Meyer, Exponential space complete problems for Petri nets and commutative semigroups, Proc. 8th Ann. ACM Symp. on Theory of Computing, Hershey, PA (May 1976) 50-54.

Digital Library

[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]

{Ki} J. C. King, Symbolic execution and program testing, C. ACM 19 (July 1976) 385-394.

Digital Library

[13]

{Kn} D. E. Knuth, The Art of Computer Programming: Volume 3, Sorting and Searching, Addison Wesley, Reading, MA (1973).

Digital Library

[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]

{Ko1} D. Kozen, Complexity of finitely presented algebras, Proc. 9th Ann. ACM Symp. on Theory of Computing, Boulder, Co. (May 1977) 164-177.

Digital Library

[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.

Digital Library

[19]

{NO2} G. Nelson and D. Oppen, A simplifier for program manipulation, this proceedings.

[20]

{PW} M. S. Paterson and M. N. Wegman, Linear unification, Proc. 8th Ann. ACM Symp. on Theory of Computing, Hershey, PA (May 1976) 181-186.

Digital Library

[21]

{Sa1} H. Samet, A normal form for compiler testing Proc. Symp. on Artificial Intelligence and Programming Languages, Rochester, NY (August 1977).

Digital Library

[22]

{Sa2} H. Samet, Proving the correctness of heuristically optimized code, Communications of the ACM, to appear.

Digital Library

[23]

{Se1} Ravi Sethi, Testing for the Church Rosser property, JACM 21, 4 (October 1974) 671-679; errata JACM 22, 3(July 1975) 424.

Digital Library

[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]

{Tarj2} R. E. Tarjan, On the efficiency of a good but not linear set merging algorithm, JACM 22, 2 (April 1975) 215-225.

Digital Library

[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).

Cited By

Armando ABonacina MRanise SSchulz S(2009)New results on rewrite-based satisfiability proceduresACM Transactions on Computational Logic10.1145/1459010.145901410:1(1-51)Online publication date: 23-Jan-2009
https://dl.acm.org/doi/10.1145/1459010.1459014
Snyder W(2005)Efficient ground completionRewriting Techniques and Applications10.1007/3-540-51081-8_123(419-433)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-51081-8_123
Pratt V(2005)Axioms or algorithmsMathematical Foundations of Computer Science 197910.1007/3-540-09526-8_12(160-169)Online publication date: 26-May-2005
https://doi.org/10.1007/3-540-09526-8_12
Show More Cited By

Off-line and on-line algorithms for deducing equalities
1. Mathematics of computing

Recommendations

Gene function classification using NCI-60 cell line gene expression profiles

Gene expression patterns from NCI's panel of 60 cell lines were used to train a Neural Network model for classifying genes to pathways. The model assigns probabilities to each gene for each of the 21 modeled pathways assigned by the Kyoto Encyclopedia ...
Line greatest common subgraphs
Logicality, Double-Line Rules, and Modalities

This paper deals with the question of the logicality of modal logics from a proof-theoretic perspective. It is argued that if Dos?en's analysis of logical constants as punctuation marks is embraced, it is possible to show that all the modalities in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

January 1978

264 pages

ISBN:9781450373487

DOI:10.1145/512760

Conference Chairs:
Alfred V. Aho
Bell Laboratories, Murray Hill, New Jersey
,
Stephen N. Zilles
IBM, San Jose, California
,
Program Chair:
Thomas G. Szymanski
Princeton University, Princeton, New Jersey

Copyright © 1978 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1978

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

POPL '78 Paper Acceptance Rate 27 of 135 submissions, 20%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
306
Total Downloads

Downloads (Last 12 months)54
Downloads (Last 6 weeks)11

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Armando ABonacina MRanise SSchulz S(2009)New results on rewrite-based satisfiability proceduresACM Transactions on Computational Logic10.1145/1459010.145901410:1(1-51)Online publication date: 23-Jan-2009
https://dl.acm.org/doi/10.1145/1459010.1459014
Snyder W(2005)Efficient ground completionRewriting Techniques and Applications10.1007/3-540-51081-8_123(419-433)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-51081-8_123
Pratt V(2005)Axioms or algorithmsMathematical Foundations of Computer Science 197910.1007/3-540-09526-8_12(160-169)Online publication date: 26-May-2005
https://doi.org/10.1007/3-540-09526-8_12
Hoffmann CO'Donnell M(1982)Pattern Matching in TreesJournal of the ACM10.1145/322290.32229529:1(68-95)Online publication date: 1-Jan-1982
https://dl.acm.org/doi/10.1145/322290.322295
Pratt VWhite JLipton RGoldberg P(1981)Program logic without binding is decidableProceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/567532.567550(159-163)Online publication date: 26-Jan-1981
https://dl.acm.org/doi/10.1145/567532.567550
Samet HMarcus L(1980)Purging in an equality data baseInformation Processing Letters10.1016/S0020-0190(80)90081-210:2(89-95)Online publication date: Mar-1980
https://doi.org/10.1016/S0020-0190(80)90081-2

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents