Total correctness by local improvement in program transformation

ABSTRACT

The goal of program transformation is to improve efficiency while preserving meaning. One of the best known transformation techniques is Burstall and Darlington's unfold-fold method. Unfortunately the unfold-fold method itself guarantees neither improvement in efficiency nor total-correctness. The correctness problem for unfold-fold is an instance of a strictly more general problem: transformation by locally equivalence-preserving steps does not necessarily preserve (global) equivalence.This paper presents a condition for the total correctness of transformations on recursive programs, which, for the first time, deals with higher-order functional languages (both strict and non-strict) including lazy data structures. The main technical result is an improvement theorem which says that if the local transformation steps are guided by certain optimisation concerns (a fairly natural condition for a transformation, then correctness of the transformation follows.The improvement theorem makes essential use of a formalised improvement-theory; as a rather pleasing corollary it also guarantees that the transformed program is a formal improvement over the original. The theorem has immediate practical consequences:• It is a powerful tool for proving the correctness of existing transformation methods for higher-order functional programs, without having to ignore crucial factors such as memoization or folding. We have applied the theorem to obtain a particularly simple proof of correctness for a higher-order variant of deforestation.• It yields a simple syntactic method for guiding and constraining the unfold/fold method in the general case so that total correctness (and improvement) is always guaranteed.

REFERENCES

• Abr90: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• Amt92: Torben Amtoft, Unfold/fold Transformations Preserving Termination Properties, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.187-201, August 26-28, 1992
• BCE92a: Annalisa Bossi , Nicoletta Cocco , Sandro Etalle, On Safe Folding, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.172-186, August 26-28, 1992
• BCE92b: Annalisa Bossi , Nicoletta Cocco , Sandro Etalle, Transforming Normal Programs by Replacement, Proceedings of the 3rd International Workshop on Meta-Programming in Logic, p.265-279, June 10-12, 1992
• BD77: R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
• Bir84: R. Bird. Using circular programs to eliminate multiple traversals of data. A cta Informat#ca, 21:239-250, 1984.
• BK83: G. Boudol and L. Kott. Recursion induction principle revisited. Theoretical Computer Science, 22:135-173, 1983.
• CK93: C. Consel and S. Khoo. On-line and off-line partial evaluation: Semantic specification and correctness proofs. Technical report, Yale University, April 1993.
• Cou79: B. Courcell. Infinite trees in normal form and recursive equations having a unique solution. Mathematical Systems Theory, 13:131-180, 1979.
• Cou86: B. Courcelle. Equivalences and transformations of regular systems--applications to recursive program schemes and grammars. Theoretical Computer Science, 42:1-122, 1986.
• FFK87: M. Felleisen , D. P. Friedman , E. Kohlbecker , B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, v.52 n.3, p.205-237, June 1987 [doi>10.1016/0304-3975(87)90109-5]
• Gom92: Carsten K. Gomard, A self-applicable partial evaluator for the lambda calculus: correctness and pragmatics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.2, p.147-172, April 1992 [doi>10.1145/128861.128864]
• GS91: P. Gardner and j. Shepherdson. Unfold/fold transformations of logic programs. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. 1991.
• How89: D. Howe, Equality in lazy computation systems, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.198-203, June 1989, Pacific Grove, California, United States
• JGS93: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• KF86: T. Kanamori and H. Fujita. Unfold/fold transformation of logic programs with counters. Technical Report ICOT Tech Report TR-179, Mitsubishi Electric Corp., 1986.
• Kot78: L. Kott. About transformation system: A theoretical study. In B. Robinet, editor, Program Transformations, pages 232-247. Dunod, 1978.
• Kot80: Laurent Kott, A System for Proving Equivalences of Recursive Programs, Proceedings of the 5th Conference on Automated Deduction, p.63-69, July 08-11, 1980
• Kot85: L Kott, Unfold/fold program transformations, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• Mah89: M. Maher. Correctness of a logic program transformation system. Technical report, IBM - Watson Research Center, 1987 (revised 1989).
• Mil77: R. Milner. Fully abstract models of the typed A- calculus. Theoretical Computer Science, 4, 1977.
• Mil89: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• MW79: Z. Manna and R. Waldinger. Synthesis: Dreams -+ programs. Transactions on Programming Languages and Systems, 5(4), 1979.
• Pal93: J. Palsberg. Correctness of binding time analysis. Journal of Functional Programming, 3(3), 1993.
• Plo75: G.D. Plotkin. Call-by-name, Call-by-value and the A-calculus. Theoretical Computer Science, 1(1):125-159, 1975.
• PP91: Maurizio Proietti , Alberto Pettorossi, Semantics preserving transformation rules for Prolog, ACM SIGPLAN Notices, v.26 n.9, p.274-284, Sept. 1991
• PP93: A. Pettorossi and M Proietti. Transformation of logic programs: Foundations and techniques. Technical Report R 369, CNR Istituto di Analisi dei Sistemi ed Informatica, Rome, November 1993.
• Red89: U. S. Reddy, Rewriting techniques for program synthesis, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.388-403, January 1989
• RFJ89: Colin Runciman , Mike Firth , Nigel Jagger, Transformation in a Non-Strict Language: An Approach to Instantiation, Proceedings of the 1989 Glasgow Workshop on Functional Programming, p.133-141, August 21-23, 1989
• San91: David Sands, Operational Theories of Improvement in Functional Languages (Extended Abstract), Proceedings of the 1991 Glasgow Workshop on Functional Programming, p.298-311, August 12-14, 1991
• San93: D. Sands. A naive time analysis and its theory of cost equivalence. TOPPS report D-173, DIKU, 1993. To appear: Journal of Logic and Computation.
• San94: D. Sands. Total correctness and improvement in the transformation of functional programs. DIKU, University of Copenhagen, Unpublished (53 pages), May 1994.
• Sat90: Taisuke Sato, An Equivalence Preserving First Order Unfold/fold Transformation System, Proceedings of the Second International Conference on Algebraic and Logic Programming, p.173-188, October 01-03, 1990
• Sch80: William Louis Scherlis, Expression procedures and program derivation, 1980
• Sch81: William L. Scherlis, Program improvement by internal specialization, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.41-49, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567536]
• Sek93: H. Seki. Unfold/fold transformation of general logic programs for the well-founded semantics, jr. Logic Programming, 16:5-23, 1993.
• TS84: H. Tamaki and T. Sato. Unfold/fold transformation of logic programs. In S. Tarnlund, editor, 2nd International Logic Programming Conference, pages 127-138, 1984.
• Tur86: Valentin F. Turchin, The concept of a supercompiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.3, p.292-325, July 1986 [doi>10.1145/5956.5957]
• Wad90: Philip Wadler, Deforestation: transforming programs to eliminate trees, Theoretical Computer Science, v.73 n.2, p.231-248, June 22, 1990
• Wan93: M. Wand. Specifying the correctness of binding time analysis. Journal of Functional Programming, 3(3), 1993.
• Zhu94: Hong Zhu. How powerful are folding/unfolding transformations? J. Functwnal Programing, 4(1):89-112, January 1994.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

General Terms:
Languages, Theory, Verification