A Completeness Theorem for Straight-Line Programs with Structured Variables

ABSTRACT

A program scheme which models straight-line code admitting structured variables such as arrays, lists, and queues is considered. A set of expressions is associated with a program reflecting the input-output transformations. A basic set of axioms is given and program equivalence is defined in terms of expression equivalence. Program transformations are then defined such that two programs are equivalent if and only if one program can be transformed to the other via the transformations. An application of these results to code optimization is then discussed.

REFERENCES

• 1: AHO, A V., AND ULLMAN, J D. Equivalence of programs with structured variables llth Ann. Syrup. on Switching and Automata Theory, 1970, pp. 25-31.
• 2: AHo, A.V., AND ULLMAN, J.D. Optimization of straight line programs. SIAM J. Comput. 1, I (March 1972), 1-19.
• 3: AHO, A.V., AND ULLMAN, J.D. Equivalence of programs with structured variables. J. Comput. Syst. Sc~s. 6, 2 (April 1972), 125-137.
• 4: Alfred V. Aho , Jeffrey D. Ullman, Theory of Parsing, Translation and Compiling, Prentice Hall Professional Technical Reference, 1973
• 5: ALLEN, F.E. Program optimization. In Annual Review of Automatic Programming, Vol. 5, M.I. Halpern and C.J. Shaw, Eds., Pergamon, New York, 1969, pp. 239-308.
• 6: James C. Beatty, An axiomatic approach to code optimization for expressions, Journal of the ACM (JACM), v.19 n.4, p.613-640, Oct. 1972 [doi>10.1145/321724.321728]
• 7: CHROUST, G. Expression evaluation with minimal average working storage. Inform Processing Letters i, 3 (Feb. 1972), 111-114.
• 8: COCKE, J., AND SCHWARTZ, J.T. Programming Languages and Their Corapders. Courant institute of Math. Sciences, New York U., New York, 1970, 767 pp.
• 9: Christoph Martin Hoffmann, Axiomatic code optimization in the presence of structured variables., 1974
• 10: HOFFMANN, C.M , AND LANDWEBER, L H Axiomatic equivalence of programs with structured variables 15th Ann. Symp on Switching and Automata Theory, 1974, pp. 78-83
• 11: Barry K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, Journal of the ACM (JACM), v.20 n.1, p.160-187, Jan. 1973 [doi>10.1145/321738.321750]
• 12: Ravi Sethi, Complete register allocation problems, Proceedings of the fifth annual ACM symposium on Theory of computing, p.182-195, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804049]
• 13: 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]
• 14: Ravi Sethi , J. D. Ullman, The Generation of Optimal Code for Arithmetic Expressions, Journal of the ACM (JACM), v.17 n.4, p.715-728, Oct. 1970 [doi>10.1145/321607.321620]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Program and recursion schemes

General Terms:
Design, Performance, Theory, Verification