Document Open Access Logo

Conditional Complexity

Authors Cynthia Kop, Aart Middeldorp, Thomas Sternagel

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.223.pdf
  • Filesize: 0.56 MB
  • 18 pages

Document Identifiers

Author Details

Cynthia Kop
Aart Middeldorp
Thomas Sternagel

Cite As Get BibTex

Cynthia Kop, Aart Middeldorp, and Thomas Sternagel. Conditional Complexity. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 223-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.223

Abstract

We propose a notion of complexity for oriented conditional term rewrite systems. This notion is realistic in the sense that it measures not only successful computations but also partial computations that result in a failed rule application. A transformation to unconditional context-sensitive rewrite systems is
presented which reflects this complexity notion, as well as a technique to derive runtime and derivational complexity bounds for the latter.

Subject Classification

Keywords
  • conditional term rewriting
  • complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. Antoy, B. Brassel, and M. Hanus. Conditional narrowing without conditions. In Proc. 5th PPDP, pages 20-31, 2003. \doi10.1145/888251.888255. Google Scholar
  2. M. Avanzini and G. Moser. Tyrolean complexity tool: Features and usage. In Proc. 24th RTA, volume 21 of Leibniz International Proceedings in Informatics, pages 71-80, 2013. \doi10.4230/LIPIcs.RTA.2013.71. Google Scholar
  3. J. Avenhaus and C. Loría-Sáenz. On conditional rewrite systems with extra variables and deterministic logic programs. In Proc. 5th LPAR, volume 822 of LNAI, pages 215-229, 1994. \doi10.1007/3-540-58216-9_40. Google Scholar
  4. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  5. G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with polynomial interpretation termination proof. JFP, 11(1):33-53, 2001. Google Scholar
  6. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott. All About Maude - A High-Performance Logical Framework, volume 4350 of LNCS. Springer, 2007. Google Scholar
  7. T.F. Şerbănuţă and G. Roşu. Computationally equivalent elimination of conditions. In Proc. 17th RTA, volume 4098 of LNCS, pages 19-34, 2006. \doi10.1007/11805618_3. Google Scholar
  8. J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Proving termination of programs automatically with AProVE. In Proc. 7th IJCAR, volume 8562 of LNCS, pages 184-191, 2014. \doi10.1007/978-3-319-08587-6_13. Google Scholar
  9. K. Gmeiner and N. Nishida. Notes on structure-preserving transformations of conditional term rewrite systems. In Proc. 1st WPTE, volume 40 of OASICS, pages 3-14, 2014. \doi10.4230/OASIcs.WPTE.2014.3. Google Scholar
  10. N. Hirokawa and G. Moser. Automated complexity analysis based on the dependency pair method. In Proc. 4th IJCAR, volume 5195 of LNAI, pages 364-380, 2008. \doi10.1007/978-3-540-71070-7_32. Google Scholar
  11. N. Hirokawa and G. Moser. Automated complexity analysis based on context-sensitive rewriting. In Proc. Joint 25th RTA and 12th TLCA, volume 8560 of LNCS, pages 257-271, 2014. \doi10.1007/978-3-319-08918-8_18. Google Scholar
  12. D. Hofbauer and C. Lautemann. Termination proofs and the length of derivations (preliminary version). In Proc. 3rd RTA, volume 355 of LNCS, pages 167-177, 1989. \doi10.1007/3-540-51081-8_107. Google Scholar
  13. S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1), 1998. Google Scholar
  14. S. Lucas. Context-sensitive rewriting strategies. Information and Computation, 178(1):294-343, 2002. \doi10.1006/inco.2002.3176. Google Scholar
  15. S. Lucas, C. Marché, and J. Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95(4):446-453, 2005. \doi10.1016/j.ipl.2005.05.002. Google Scholar
  16. S. Lucas and J. Meseguer. 2D dependency pairs for proving operational termination of CTRSs. In Proc. 10th WRLA, volume 8663 of LNCS, pages 195-212, 2014. \doi10.1007/978-3-319-12904-4_11. Google Scholar
  17. M. Marchiori. Unravelings and ultra-properties. In M. Hanus and M. Rodríguez-Artalejo, editors, Proc. 5th ICALP, volume 1139 of LNCS, pages 107-121. Springer, 1996. \doi10.1007/3-540-61735-3_7. Google Scholar
  18. M. Marchiori. On deterministic conditional rewriting. Computation Structures Group Memo 405, MIT Laboratory for Computer Science, 1997. Google Scholar
  19. A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. Zankl. Joint spectral radius theory for automated complexity analysis of rewrite systems. In Proc. 4th CAI, volume 6742 of LNCS, pages 1-20, 2011. \doi10.1007/978-3-642-21493-6_1. Google Scholar
  20. G. Moser and A. Schnabl. The derivational complexity induced by the dependency pair method. Logical Methods in Computer Science, 7(3), 2011. \doi10.2168/LMCS-7(3:1)2011. Google Scholar
  21. N. Nishida, M. Sakai, and T. Sakabe. Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity. Logical Methods in Computer Science, 8:1-49, 2012. \doi10.2168/LMCS-8(3:4)2012. Google Scholar
  22. L. Noschinski, F. Emmes, and J. Giesl. Analyzing innermost runtime complexity of term rewriting by dependency pairs. Journal of Automated Reasoning, 51(1):27-56, 2013. \doi10.1007/s10817-013-9277-6. Google Scholar
  23. E. Ohlebusch. Transforming conditional rewrite systems with extra variables into unconditional systems. In Proc. 6th LPAR, volume 1705 of LNCS, pages 111-130, 1999. \doi10.1007/3-540-48242-3_8. Google Scholar
  24. E. Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. \doi10.1007/978-1-4757-3661-8. Google Scholar
  25. F. Schernhammer and B. Gramlich. VMTL - a modular termination laboratory. In Proc. 20th RTA, volume 5595 of LNCS, pages 285-294, 2009. \doi10.1007/978-3-642-02348-4_20. Google Scholar
  26. F. Schernhammer and B. Gramlich. Characterizing and proving operational termination of deterministic conditional term rewriting systems. Journal of Logic and Algebraic Programming, 79(7):659-688, 2010. \doi10.1016/j.jlap.2009.08.001. Google Scholar
  27. T. Sternagel and A. Middeldorp. Conditional confluence (system description). In Proc. Joint 25th RTA and 12th TLCA, volume 8560 of LNCS, pages 456-465, 2014. \doi10.1007/978-3-319-08918-8_31. Google Scholar
  28. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  29. P. Viry. Elimination of conditions. Journal of Symbolic Computation, 28(3):381-401, 1999. \doi10.1006/jsco.1999.0288. Google Scholar
  30. H. Zankl and M. Korp. Modular complexity analysis for term rewriting. Logical Methods in Computer Science, 10(1:19):1-33, 2014. \doi10.2168/LMCS-10(1:19)2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact