Skip to main content
SpringerLink
Log in

POP* and Semantic Labeling Using SAT

  • Conference paper
Interfaces: Explorations in Logic, Language and Computation (ESSLLI 2008, ESSLLI 2009)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6211))

  • 486 Accesses

Abstract

The polynomial path order ( POP* for short) is a termination method that induces polynomial bounds on the innermost runtime complexity of term rewrite systems (TRSs for short). Semantic labeling is a transformation technique used for proving termination.

In this paper, we propose an efficient implementation of POP* together with finite semantic labeling. This automation works by a reduction to the problem of boolean satisfiability. We have implemented the technique and experimental results confirm the feasibility of our approach. By semantic labeling the analytical power of POP* is significantly increased.

This research is supported by FWF (Austrian Science Fund) projects P20133.

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. Anderson, H., Khoo, S., Andrei, S., Luca, B.: Calculating polynomial runtime properties. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 230–246. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. TCS 236(1-2), 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  3. Avanzini, M., Hirokawa, N., Middeldorp, A., Moser, G.: Proving termination of scheme programs by rewriting, http://cl-informatik.uibk.ac.at/~zini/publications/SchemeTR07.pdf

  4. Avanzini, M., Moser, G.: Complexity analysis by rewriting. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 130–146. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Avanzini, M., Moser, G.: Dependency pairs and polynomial path orders. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 48–62. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Avanzini, M., Moser, G.: Polynomial path orders and the rules of predicative recursion with parameter substitution. In: Proc. 10th WST (2009)

    Google Scholar 

  7. Avanzini, M., Moser, G.: Complexity analysis by graph rewriting. In: Proc. 11th FLOPS. LNCS. Springer, Heidelberg (to appear, 2010)

    Google Scholar 

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

    Google Scholar 

  9. Bellantoni, S., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. CC 2, 97–110 (1992)

    MATH  MathSciNet  Google Scholar 

  10. Bonfante, G., Marion, J., Péchoux, R.: Quasi-interpretation synthesis by decomposition. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 410–424. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Dershowitz, N.: Orderings for term-rewriting systems. In: 20th Annual Symposium on Foundations of Computer Science, pp. 123–131. IEEE, Los Alamitos (1979)

    Google Scholar 

  12. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Google Scholar 

  13. Giesl, J., Swiderski, S., Schneider-Kamp, P., Thiemann, R.: Automated termination analysis for Haskell: From term rewriting to programming languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 297–312. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–380. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. TCS 105(1), 129–140 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  16. Koprowski, A.: Tpa: Termination proved automatically. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 297–312. Springer, Heidelberg (2006)

    Google Scholar 

  17. Koprowski, A., Middeldorp, A.: Predictive labeling with dependency pairs using SAT. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 410–425. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 47–61. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Lescanne, P.: Termination of rewrite systems by elementary interpretations. Formal Aspects of Computing 7(1), 77–90 (1995)

    Article  MATH  Google Scholar 

  20. Moser, G., Schnabl, A.: Proving quadratic derivational complexities using context dependent interpretations. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 276–290. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  22. Rosendahl, M.: Automatic complexity analysis. In: Proc. 4th FPCA, pp. 144–156 (1989)

    Google Scholar 

  23. Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and SAT solving. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 267–282. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. TeReSe: Term Rewriting Systems. CTTCS, vol. 55. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  25. Tseitin, G.: On the complexity of derivation in propositional calculus. SCML, Part 2, 115–125 (1968)

    Google Scholar 

  26. Zantema, H.: Termination of term rewriting by semantic labelling. FI 24(1/2), 89–105 (1995)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Martin Avanzini

Authors
  1. Martin Avanzini
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Stanford University, Stanford,, CA, USA

    Thomas Icard

  2. Tilburg University, Tilburg, The Netherlands

    Reinhard Muskens

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Avanzini, M. (2010). POP* and Semantic Labeling Using SAT. In: Icard, T., Muskens, R. (eds) Interfaces: Explorations in Logic, Language and Computation. ESSLLI ESSLLI 2008 2009. Lecture Notes in Computer Science(), vol 6211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14729-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14729-6_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14728-9

  • Online ISBN: 978-3-642-14729-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation