Proofs by structural induction using partial evaluation

ABSTRACT

In this paper we show how partial evaluation can be used in developing proofs about program transformations. Partial evaluation is particularly appropriate for this task because it distinguishes between static and dynamic data. As a realistic example of this technique we prove a theorem arising in our earlier study of the CPS transformation. Our approach requires a partial evaluator that supports the following features: resugaring, partially-static structures, higher-order functions, polyvariance, and filters. In particular, we use Consel's partial evaluator Schism.

REFERENCES

• 1: R. S. Bird, Algebraic identities for program calculation, The Computer Journal, v.32 n.2, p.122-126, April 1989 [doi>10.1093/comjnl/32.2.122]
• 2: Anders Bondorf, Improving binding times without explicit CPS-conversion, Proceedings of the 1992 ACM conference on LISP and functional programming, p.1-10, June 22-24, 1992, San Francisco, California, United States
• 3: Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
• 4: Alan Bundy , Andrew Stevens , Frank van Harmelen , Andrew Ireland , Alan Smaill, Rippling: a heuristic for guiding inductive proofs, Artificial Intelligence, v.62 n.2, p.185-253, Aug. 1993 [doi>10.1016/0004-3702(93)90079-Q]
• 5: Charles Consel. Report on Schism'92. Research report, Pacific Software Research Center, Oregon Graduate Institute of Science and Technology, Beaverton, Oregon, USA, 1992.
• 6: Charles Consel, A tour of Schism: a partial evaluation system for higher-order applicative languages, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.145-154, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154645]
• 7: Charles Consel , Olivier Danvy, For a better support of static data flow, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.496-519, June 1991, Cambridge, Massachusetts, United States
• 8: Olivier Danvy, Back to direct style, Symposium proceedings on 4th European symposium on programming, p.130-150, January 1992, Rennes, France
• 9: Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361-391, 1992.
• 10: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 11: Christian Horn. The Oyster proof development system. Working paper 214, University of Edinburgh, Dept. of Artificial Intelligence, December 8, 1989.
• 12: Julia L. Lawall , Olivier Danvy, Separating stages in the continuation-passing style transformation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.124-136, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158613]
• 13: Karoline Malmkjmr. On static properties of specialized programs. In Michel Billaud et al., editor, Analyse Statique en Programmation E, quationnelle, Fonctionnelle et Logique, volume 74 of Bigre Journal, pages 234- 241, Bordeaux, France, October 1991. IttISA, Rennes, FrllJlCe.
• 14: Karo}ine Malmkjver. Predicting properties of residual programs. In Charles Consel, editor, A CM SIGPLAN Workshop on Partial Evaluation and Semantics.Based Program Manipulation, Research Report 909, Department of Computer Science, Yale University, pages 8-13, San Francisco, California, June 1992.
• 15: Torben Æ Mogensen, Separating binding times in language specifications, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.12-25, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99372]
• 16: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 17: Tim Sheard, Automatic generation and use of abstract structure operators, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.531-557, Oct. 1991 [doi>10.1145/115372.115369]
• 18: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 19: Valentin F. Turchin, The Use of Metasystem Transition in Theorem Proving and Program Optimization, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.645-657, July 14-18, 1980
• 20: 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]
• 21: Frank van Harmelen. The C/~Mproof planner, user manual, and programmer manual: version 1.4. Technical paper TP-4, University of Edinburgh, Dept. of Artificial Intelligence, December 12 1989.
• 22: Philip Wadler, Deforestation: transforming programs to eliminate trees, Theoretical Computer Science, v.73 n.2, p.231-248, June 22, 1990

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

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

          Nouns: SCHEME
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Languages, Theory, Verification