A self-applicable partial evaluator for the lambda calculus: correctness and pragmatics

ABSTRACT

We describe theoretical and a few practical aspects of an implemented self-applicable partial evaluator for the untyped lambda calculus with constants, conditionals, and a fixed point operator. The purpose of this paper is first to announce the existence of (and to describe) a partial evaluator that is both higher-order and self-applicable; second to describe a surprisingly simple solution to the central problem of binding time analysis, and third to prove that the partial evaluator yields correct answers. While &lgr;-mix (the name of our system) seems to have been the first higher-order self-applicable partial evaluator to run on a computer, it was developed mainly for research purposes. Two recently developed systems are much more powerful for practical use, but also much more complex: Similix[3,5] and Schism[7]. Our partial evaluator is surprisingly simple, completely automatic, and has been implemented in a side effect-free subset of Scheme. It has been used to compile, generate compilers and generate a compiler generator.

REFERENCES

• 1: Andrew W. Appel, Semantics-directed code generation, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.315-324, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318661]
• 2: BECKMAN, L., et al. A partial evaluator, and its use as a programming tool. Artif. Intell. 7, 4 (1976), 319-357.
• 3: A. Bondorf, Automatic autoprojection of higher order recursive equations, Proceedings of the third European symposium on programming on ESOP '90, p.70-87, May 1990, Copenhagen, Denmark
• 4: Anders Bondorf, A Self-Applicable Partial Evaluator for Term Rewriting Systems, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.81-95, March 13-17, 1989
• 5: BONDORP, A., AND DANVY, O. Automatic autoprojection of recursive equations with global variables and abstract data types. Tech. Rep. 90/4, DIKU, Univ. of Copenhagen, 1990. Te appear in Science of Computer Programming.
• 6: BONDORF, A., JONES, N. D., MOGENSEN, T., AND SESTOFT, P. Binding time analysis and the taming of self-application. Draft, DIKU, Univ. of Copenhagen, Aug. 1988.
• 7: ONSEL, C. Analyse de programmes, evaluation partielle et g~n~ration de compilateurs. Ph.D. dissertation, Univ. de Paris 6, Paris, June 1989, 109 pp. (in French).
• 8: Charles Consel, New Insights into Partial Evaluation: the SCHISM Experiment, Proceedings of the 2nd European Symposium on Programming, p.236-246, March 21-24, 1988
• 9: Charles Consel , Olivier Danvy, Partial evaluation of pattern matching in strings, Information Processing Letters, v.30 n.2, p.79-86, January 1989 [doi>10.1016/0020-0190(89)90113-0]
• 10: ERs~ov, A. P. On the essence of compilation. In Formal Description of Programming Concepts, E. J. Neuhold, Ed., North-Holland, Amsterdam, 1978, 391-420.
• 11: ERSHOV, A. P., AND ITKIN, V.E. Correctness of mixed computation in Algol-like programs. In Mathematical Foundations of Computer Science (Tatransk~ Lomnica, Czechoslovakia), J. Gruska, Ed., Lecture Notes in Computer Science, 53, Springer-Verlag, New York, pp. 59-77.
• 12: D. A. Fuller , S. Abramsky, Mixed computation of Prolog programs, New Generation Computing, v.6 n.2-3, p.119-141, March-April 1988 [doi>10.1007/BF03037134]
• 13: FUTAMURA, Y. Partial evaluation of computation process--An approach te a compiler- ~compiler. Syst. Comput. Controls 2, 5 (1971), 45-50.
• 14: GOMARD, C. K., AND JONES, N.D. Compiler generation by partial evaluation: A case study. J. Struct. Program. 12, 3 (July 1991), te appear. Also DIKU Rep. 88/24 and 90/16.
• 15: Carsten K. Gomard, Partial type inference for untyped functional programs, Proceedings of the 1990 ACM conference on LISP and functional programming, p.282-287, June 27-29, 1990, Nice, France [doi>10.1145/91556.91672]
• 16: GOMARD, C. K., AND JONES, N. D. A partial evaluator for the untyped lambda-calculus. J. Func. Program. 1, I (Jan. 1991), 21-69.
• 17: GuzowsKI, M.A. Towards developing a refiexive partial evaluator for an interesting subset of Lisp. Master's Thesis, Dept. of Computer Eng. and Science, Case Western Reserve Univ., Cleveland, Ohio, Jan. 1988.
• 18: John Hannan , Dale Miller, Deriving Mixed Evaluation from Standard Evaluation for a Simple Functional Language, Proceedings of the International Conference on Mathematics of Program Construction, 375th Anniversary of the Groningen University, p.239-255, June 26-30, 1989
• 19: JONES, N.D. Automatic program specialization: a re-examination from basic principles. In Partial Evuluation and Mixed Computation, D. Bj~/rner, A P Ershov, and N D. Jones, Eds., North-Holland, Amsterdam, 1988, pp. 225-282.
• 20: JO~~ES, N. D, GOMARD, C. K., BONDORF, A., DANVY, O., AND MOGENSEN, T. E. A selfapplicable partial evaluator for the lambda calculus. In 1990 International Conference on Computer Languages (New Orteans, LA, March 1990), IEEE Computer Society, New York, 1990, pp. 49-58.
• 21: Neil D. Jones , Peter Sestoft , Harald Sondergaard, An experiment in partial evaluation: the generation of a compiler generator, Proc. of the first international conference on Rewriting techniques and applications, p.124-140, December 1985, Dijon, France
• 22: JON~S, N. D., SESTOFT, P., AND SfINDERCAARD, H. Mix: a sel~applicable partial evaluator for experiments in compiler generation. Lisp Symbol~c Comput. 2, i (1989), 9-50.
• 23: Ulrik Jørring , William L. Scherlis, Compilers and staging transformations, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.86-96, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512652]
• 24: LOMSARDI, L. A. Incremental computation. In Advances Comput. 8, F. L. Alt and M Rubinoff, Eds., 1967, 247-333.
• 25: MessEs, P. SIS--Semant~cs Implem?tation System, Reference Manual and User Guide. DAIMI Rep. MD-30, DAIMI, Univ. of Arhus, Denmark, 1979.
• 26: NmLSON, F. A formal type system for comparing partial evaluators. In Partial Evaluatwn and Mixed Computatwn, D. Bj9/rner, A. P. Ershov, and N. D. Jones, Eds , North-Holland, Amsterdam, 1988, 349-384.
• 27: NmLSON, F., AEND NmLSO~, H. R. The TML-approach te compiler-compilers. Tech. Rep. 1988-47, Dept. of Computer Science, Technical Univ. of Denmark, 1988.
• 28: F. Nielson , R. H. Nielson, Automatic binding time analysis for a typed &lgr;-calculus, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-106, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73569]
• 29: Lawrence Paulson, A semantics-directed compiler generator, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-233, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582178]
• 30: JONES, S. L.P. The Implementation of Functwnal Programming Languages. Prentice-Hall, Englewood Cliffs, N.J., 1987.
• 31: Uwe F. Pleban, Compiler prototyping using formal semantics, ACM SIGPLAN Notices, v.19 n.6, p.94-105, June 1984
• 32: ROMANENKO, S.A. A compiler generator produced by a self-applicable specializer can bave a surprisingly natural and understandable structure. In Partial Evaluatwn and Mixed Computation, D. Bj~/rner, A. P. Ershov, and N. D. Jones, Eds., North-Holland, Amsterdam, 1988, 445-463.
• 33: David A. Schmidt, Detecting global variables in denotational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.2, p.299-310, April 1985 [doi>10.1145/3318.3323]
• 34: R. Schooler, PARTIAL EVALUATION AS A MEANS OF LANGUAGE EXTENSIBILITY, Massachusetts Institute of Technology, Cambridge, MA, 1984
• 35: Peter Sestoft, Replacing function parameters by global variables, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.39-53, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99374]
• 36: 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
• 37: Mitchell Wand, A semantic prototyping system, Proceedings of the 1984 SIGPLAN symposium on Compiler construction, p.213-221, June 17-22, 1984, Montreal, Canada
• 38: Mitchell Wand, Semantics-directed machine architecture, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-241, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582179]
• 39: WEIS, P. Le Systeme SAM: Metacompilation tres efficace a l'aide d'operateur semantiques. Ph.D. dissertation, l'Univ. Paris VII, 1987 (in French).

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
          Subjects: Evaluation strategies

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Translator writing systems and compiler generators; Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
compiler generation, lambda calculus, partial evaluation, self-application