Rewriting systems on FP expressions that reduce the number of sequences they yield

ABSTRACT

In this paper, we are interested in the application of program transformation for minimizing the number of intermediary sequences used in iterative programs. We shall use the FP language for presenting programs. The transformation rules are based on the algebra of functional programs. In contrast to the other systems of rules for program transformation, sets of rules presented here are convergent (i.e. finitely terminating and confluent) rewriting systems. These rewriting systems are the result of the Knuth-Bendix procedure applied to a set of equations. The equations are valided by the algebra of functional programs. We use the implementation of the Knuth-Bendix procedure in the system REVE. If REVE is applied to a set of equations and if it does not fail, then it returns a convergent rewriting set of rules. With such a rewriting system, the task of transforming a program is reduced to rewrite it until we get its normal form. Thus we propose a set of valid equations and we discuss how convergent rewriting systems can be generated using REVE.

REFERENCES

• 1: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 2: John Backus, The Algebra of Functional Programs: Function Level Reasoning, Linear Equations, and Extended Definitions, Proceedings of the International Colloquium on Formalization of Programming Concepts, p.1-43, April 19-25, 1981
• 3: John Backus, Function level programs as mathematical objects, Proceedings of the 1981 conference on Functional programming languages and computer architecture, p.1-10, October 18-22, 1981, Portsmouth, New Hampshire, United States [doi>10.1145/800223.806757]
• 4: DERSHOWITZ N., "Orderings for term-rewriting systems" Theorical Computer Science, 17-3, (1982), pp. 279-301.
• 5: M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512773]
• 6: Leo J. Guibas , Douglas K. Wyatt, Compilation and delayed evaluation in APL, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.1-8, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512761]
• 7: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• 8: Jean-Pierre Jouannaud , Claude Kirchner , Hélène Kirchner, Incremental Construction of Unification Algorithms in Equational Theories, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.361-373, July 18-22, 1983
• 9: JOUANNAUD J.P., KIRCHNER C., KIRCHNER H., "Using meta-rules in the Knuth-Bendix completion algorithm" To appear.
• 10: JOUANNAUD J.P., LESCANNE P., REINIG F., "Recursive decomposition ordering" In Formal Description of programming, concept II, IFIP TC-2 Conference, D. Bjorner Ed., North Holland, (1982), pp.331-348.
• 11: KNUTH D., BENDIX P., "Simple word problems in universal algebras" In Computational problem in universal algebra. Leech J. Ed. Pergamon Press., (1970), pp. 263-297.
• 12: KIRCHNER C., KIRCHNER H., "Unification dans les theories equationnelles" Internal Report. CRIN 83R011, (1983)
• 13: LANKFORD D., "On proving Term-Rewriting Systems are Noetherian" Report MTP-2, Math. Dept., Louisiana Tech. University, (1979)
• 14: Pierre Lescanne, Computer experiments with the REVE term rewriting system generator, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.99-108, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567078]
• 15: LESCANNE P., "Uniform Termination of Term-Rewriting systems, a new Recursive Decomposition Ordering with status" CAAP, Bordeaux(1984)
• 16: MANNA Z., NESS S., "On the termination of Markov algorithms" Proc. 3rd Int. Conf. on System Sciences, Honolulu, (1970), pp. 789-792.
• 17: REDDY U.S., JAYARAMAN B., "Theory of linear equations applied to program transformation" Proc. of 9th. IJCAI, (1983), pp. 10-16.
• 18: TURNER D. A., "SASL Language Manuel" St. Andrews University Technical Report, (1976)
• 19: WILLIAMS J.H., "On the development of the algebra of functional programs" Report RJ2983, IBM Research Laboratory, San Jose, California, (1980)

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: FP

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program transformation

General Terms:
Languages