Skip to main content
SpringerLink
Log in

Improving Offline Narrowing-Driven Partial Evaluation Using Size-Change Graphs

  • Conference paper
Logic-Based Program Synthesis and Transformation (LOPSTR 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4407))

Abstract

An offline approach to narrowing-driven partial evaluation (a partial evaluation scheme for first-order functional and functional logic programs) has recently been introduced. In this approach, program annotations (i.e., the expressions that should be generalised at partial evaluation time to ensure termination) are based on a simple syntactic characterisation of quasi-terminating programs. This work extends the previous offline scheme by introducing a new annotation strategy which is based on a combination of size-change graphs and binding-time analysis. Preliminary experiments point out that the number of program annotations is significantly reduced compared to the previous approach, which means that faster residual programs are often produced.

This work has been partially supported by the EU (FEDER) and the Spanish MEC under grant TIN2005-09207-C03-02, by the Mexican SEIT-ANUIES and DGEST beca-comisión and by the ICT for EU-India Cross-Cultural Dissemination Project ALA/95/23/2003/077-054.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Albert, E., Vidal, G.: The Narrowing-Driven Approach to Functional Logic Program Specialization. New Generation Computing 20(1), 3–26 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  2. Alpuente, M., Falaschi, M., Vidal, G.: Partial Evaluation of Functional Logic Programs. ACM TOPLAS 20(4), 768–844 (1998)

    Article  Google Scholar 

  3. Antoy, S.: Definitional trees. In: Kirchner, H., Levi, G. (eds.) Algebraic and Logic Programming. LNCS, vol. 632, pp. 143–157. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  4. Antoy, S., Echahed, R., Hanus, M.: A Needed Narrowing Strategy. Journal of the ACM 47(4), 776–822 (2000)

    Article  MathSciNet  Google Scholar 

  5. Arroyo, G., Ramos, J.G., Silva, J., Vidal, G.: Improving Offline Narrowing-Driven Partial Evaluation Using Size-Change Graphs. Technical report, Technical University of Valencia (2006), Available from the following URL, http://www.dsic.upv.es/users/elp/german/papers.html

  6. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  7. Bossi, A., Cocco, N., Fabris, M.: Proving Termination of Logic Programs by Exploiting Term Properties. In: Abramsky, S. (ed.) TAPSOFT 1991, CCPSD 1991, and ADC-Talks 1991. LNCS, vol. 494, pp. 153–180. Springer, Heidelberg (1991)

    Google Scholar 

  8. Chin, W.N., Khoo, S.C.: Better Consumers for Program Specializations. Journal of Functional and Logic Programming 1996(4) (1996)

    Google Scholar 

  9. Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. J. Log. Program. 41(1), 103–123 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  10. De Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B., Sørensen, M.H.: Conjunctive Partial Deduction: Foundations, Control, Algorihtms, and Experiments. Journal of Logic Programming 41(2-3), 231–277 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  11. Decorte, S., De Schreye, D., Leuschel, M., Martens, B., Sagonas, K.F.: Termination Analysis for Tabled Logic Programming. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol. 1463, pp. 111–127. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Dershowitz, N.: Termination of Rewriting. Journal of Symbolic Computation 3(1-2), 69–115 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  13. Gallagher, J.: Tutorial on Specialisation of Logic Programs. In: Proc. of the ACM Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM’93), pp. 88–98. ACM, New York (1993)

    Chapter  Google Scholar 

  14. Genaim, S., Codish, M., Gallagher, J.P., Lagoon, V.: Combining Norms to Prove Termination. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 126–138. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Giovannetti, E., Levi, G., Moiso, C., Palamidessi, C.: Kernel Leaf: A Logic plus Functional Language. Journal of Computer and System Sciences 42, 363–377 (1991)

    Article  Google Scholar 

  16. Glenstrup, A.J., Jones, N.D.: Termination analysis and specialization-point insertion in offline partial evaluation. ACM Trans. Program. Lang. Syst. 27(6), 1147–1215 (2005)

    Article  Google Scholar 

  17. Hanus, M.: The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming 19-20, 583–628 (1994)

    Article  MathSciNet  Google Scholar 

  18. Hanus, M.: Curry: An Integrated Functional Logic Language (2003), Available at, http://www.informatik.uni-kiel.de/~mh/curry

  19. Hanus, M. (ed.), Antoy, S., Engelke, M., Höppner, K., Koj, J., Niederau, P., Sadre, R., Steiner, F.: PAKCS 1.6.0: The Portland Aachen Kiel Curry System—User Manual. Technical report, University of Kiel, Germany (2004)

    Google Scholar 

  20. Holst, C.K.: Finiteness Analysis. In: Hughes, J. (ed.) Functional Programming Languages and Computer Architecture. LNCS, vol. 523, pp. 473–495. Springer, Heidelberg (1991)

    Google Scholar 

  21. Huet, G., Lévy, J.J.: Computations in orthogonal rewriting systems, Part I + II. In: Lassez, J.L., Plotkin, G.D. (eds.) Computational Logic – Essays in Honor of Alan Robinson, pp. 395–443 (1992)

    Google Scholar 

  22. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)

    MATH  Google Scholar 

  23. Lafave, L., Gallagher, J.P.: Constraint-based Partial Evaluation of Rewriting-based Functional Logic Programs. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol. 1463, pp. 168–188. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  24. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The Size-Change Principle for Program Termination. In: ACM Symposium on Principles of Programming Languages (POPL’01), vol. 28, pp. 81–92. ACM press, New York (2001)

    Chapter  Google Scholar 

  25. Lindenstrauss, N., Sagiv, Y.: Automatic termination analysis of logic programs. In: ICLP, pp. 63–77 (1997)

    Google Scholar 

  26. Loogen, R., López-Fraguas, F., Rodríguez-Artalejo, M.: A Demand Driven Computation Strategy for Lazy Narrowing. In: Penjam, J., Bruynooghe, M. (eds.) PLILP 1993. LNCS, vol. 714, pp. 184–200. Springer, Heidelberg (1993)

    Google Scholar 

  27. Moreno-Navarro, J.J., Rodríguez-Artalejo, M.: Logic Programming with Functions and Predicates: The language Babel. J. Logic Programming 12(3), 191–224 (1992)

    Article  MATH  Google Scholar 

  28. Peyton-Jones, S. (ed.): Haskell 98 Language and Libraries—The Revised Report. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  29. Ramos, J.G., Silva, J., Vidal, G.: Fast Narrowing-Driven Partial Evaluation for Inductively Sequential Systems. ACM SIGPLAN Notices (Proc. of ICFP’05) 40(9), 228–239 (2005)

    Article  Google Scholar 

  30. Slagle, J.R.: Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity. Journal of the ACM 21(4), 622–642 (1974)

    Article  MATH  MathSciNet  Google Scholar 

  31. Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. Appl. Algebra Eng. Commun. Comput. 16(4), 229–270 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  32. Verbaeten, S., Sagonas, K., De Schreye, D.: Termination Proofs for Logic Programs with Tabling. ACM Transactions on Computational Logic 2(1), 57–92 (2001)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical University of Valencia, Camino de Vera s/n, 46022 Valencia, Spain

    Gustavo Arroyo, J. Guadalupe Ramos, Josep Silva & Germán Vidal

Authors
  1. Gustavo Arroyo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. J. Guadalupe Ramos
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Josep Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Germán Vidal
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Germán Puebla

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Arroyo, G., Ramos, J.G., Silva, J., Vidal, G. (2007). Improving Offline Narrowing-Driven Partial Evaluation Using Size-Change Graphs. In: Puebla, G. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2006. Lecture Notes in Computer Science, vol 4407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71410-1_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-71410-1_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-71409-5

  • Online ISBN: 978-3-540-71410-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation