Finiteness Analysis in Polynomial Time
To achieve the termination of offline partial evaluation, it is necessary to ensure that static variables assume boundedly many values during specialization. Various works have addressed the analysis of variable boundedness, also called finiteness analysis, in the context of specializing first-order functional programs. The underlying reasoning is always: Unbounded sequences of increases in a static variable must be impossible, if they would give rise to unbounded sequences of size-decreases for some bounded-variable values.
Static analysis is used to collect a set of bipartite graphs that describe the parameter dependencies and data size changes in possible state transitions of the specializer (operating on the program). We capture the reasoning above as a condition on the graphs. This condition is decid-able, but complete for pspace. We therefore derive a polynomial-time approximation, by considering realistic parameter size-change behaviour.
KeywordsPolynomial Time Bipartite Graph Bounded Variable Dependency Graph Partial Evaluation
Unable to display preview. Download preview PDF.
- 1.Peter Holst Andersen and Carsten Kehler Holst. Termination analysis for offline partial evaluation of a higher-order functional language. In Static Analysis, Proceedings of the Third International Symposium, SAS’ 96, Aachen, Germany, Sep 24–26, 1996, volume 1145 of Lecture Notes in Computer Science, pages 67–82. Springer, 1996.Google Scholar
- 2.Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms. MIT Press, 1990.Google Scholar
- 3.Arne J. Glenstrup. Terminator II: Stopping partial evaluation of fully recursive programs. Master’s thesis, DIKU, University of Copenhagen, Denmark, 1999.Google Scholar
- 4.Arne J. Glenstrup and Neil D. Jones. BTA algorithms to ensure termination of off-line partial evaluation. In Perspectives of System Informatics, Proceedings of the Second International Andrei Ershov Memorial Conference, Russia, Jun 25–28, 1996, volume 1181 of Lecture Notes in Computer Science, pages 273–284. Springer, 1996.Google Scholar
- 5.Robert Glück. Towards multiple self-application. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 309–320. ACM, 1991.Google Scholar
- 6.Matthew Hennessy. The Semantics of Programming Languages. Wiley, 1990.Google Scholar
- 7.Carsten Kehler Holst. Finiteness analysis. In John Hughes, editor, Functional Programming Languages and Computer Architecture, Cambridge, Massachusetts, Aug 1991, volume 523 of Lecture Notes in Computer Science, pages 473–495. Springer, 1991.Google Scholar
- 8.Neil Jones and Arne Glenstrup. Program generation, termination, and binding-time analysis. In Principles, Logics, and Implementations of High-Level Programming Languages, PLI 2002 (invited paper). Springer, 2002.Google Scholar
- 9.Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.Google Scholar
- 10.Chin Soon Lee. Partial evaluation of the euclidean algorithm, revisited. Higher-Order and Symbolic Computation, 12(2):203–212, Sep 1999.Google Scholar
- 11.Chin Soon Lee. Program Termination Analysis, and Termination of Offline Partial Evaluation. PhD thesis, UWA, University of Western Australia, Australia, 2001.Google Scholar
- 12.Chin Soon Lee. Finiteness analysis in polynomial time (with proofs). To be available as a technical report at DIKU, Copenhagen University, Denmark., 2002.Google Scholar
- 13.Chin Soon Lee. Program termination analysis in polynomial time. In Proceedings of Generative Programming and Component Engineering, GPCE’ 02. Springer, 2002.Google Scholar
- 14.Chin Soon Lee, Neil D. Jones, and Amir Ben-Amram. The size-change principle for program termination. In Proceedings of the ACM Symposium on Principles of Programming Languages, Jan 2001. ACM, 2001.Google Scholar
- 15.Wim Vanhoof and Maurice Bruynooghe. Binding-time annotations without binding-time analysis. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 8th International Conference, Havana, Cuba, Dec 3–7, 2001, volume 2250 of Lecture Notes in Computer Science, pages 707–722, 2001.CrossRefGoogle Scholar