Document Open Access Logo

Leftmost Outermost Revisited

Authors Nao Hirokawa, Aart Middeldorp, Georg Moser

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.209.pdf
  • Filesize: 496 kB
  • 14 pages

Document Identifiers

Author Details

Nao Hirokawa
Aart Middeldorp
Georg Moser

Cite As Get BibTex

Nao Hirokawa, Aart Middeldorp, and Georg Moser. Leftmost Outermost Revisited. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 209-222, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.209

Abstract

We present an elementary proof of the classical result that the
leftmost outermost strategy is normalizing for left-normal orthogonal rewrite systems. Our proof is local and extends to hyper-normalization and weakly orthogonal systems. Based on the new proof, we study basic normalization, i.e., we study normalization if the set of considered starting terms is restricted to basic terms. This allows us to weaken the left-normality restriction. We show that the leftmost outermost strategy is hyper-normalizing for basically left-normal orthogonal rewrite systems. This shift of focus greatly extends the applicability of the classical result, as evidenced by the experimental data provided.

Subject Classification

Keywords
  • term rewriting
  • strategies
  • normalization

Metrics

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

References

  1. B. Accattoli. An abstract factorization theorem for explicit substitutions. In A. Tiwari, editor, Proc. 23rd International Conference on Rewriting Techniques and Applications, volume 15 of LIPIcs, pages 6-21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. doi: \doi10.4230/LIPIcs.RTA.2012.6. Google Scholar
  2. S. Antoy. Definitional trees. In H. Kirchner and G. Levi, editors, Proc. 3rd International Conference on Algebraic and Logic Programming, volume 632 of LNCS, pages 143-157. Springer, 1992. doi: \doi10.1007/BFb0013825. Google Scholar
  3. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  4. L. Bachmair and N. Dershowitz. Commutation, transformation, and termination. In J.H. Siekmann, editor, Proc. 8th International Conference on Automated Deduction, volume 230 of LNCS, pages 5-20, 1986. doi: \doi10.1007/3-540-16780-3_76. Google Scholar
  5. H.P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic. North-Holland, 2nd edition, 1984. Google Scholar
  6. K. Bimbó. Combinatory Logic: Pure, Applied and Typed. CRC Press, 2012. Google Scholar
  7. H. Comon. Sequentiality, monadic second-order logic and tree automata. Information and Computation, 157(1-2):25-51, 2000. doi: \doi10.1006/inco.1999.2838. Google Scholar
  8. H.B. Curry, J.R. Hindley, and J.P. Seldin. Combinatory Logic, Volume II, volume 65 of Studies in Logic. North-Holland, 1972. Google Scholar
  9. N. Dershowitz. On lazy commutation. In O. Grumberg, M. Kaminski, S. Katz, and S. Wintner, editors, Languages: From Formal to Natural: Essays Dedicated to Nissim Francez on the Occasion of His 65th Birthday, volume 5533 of LNCS, pages 59-82. Springer, 2009. doi: \doi10.1007/978-3-642-01748-3_5. Google Scholar
  10. M.-L. Fernández. Relaxing monotonicity for innermost termination. Information Processing Letters, 93(1):117-123, 2005. doi: \doi10.1016/j.ipl.2004.10.005. Google Scholar
  11. J. Giesl, R. Thiemann, and P. Schneider-Kamp. Proving and disproving termination of higher-order functions. In B. Gramlich, editor, Proc. 5th International Symposium on Frontiers of Combining Systems, volume 3717 of Lecture Notes in Artificial Intelligence, pages 216-231. Springer, 2005. doi: \doi10.1007/11559306_12. Google Scholar
  12. J.R. Hindley. The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis, University of Newcastle-upon-Tyne, 1964. Google Scholar
  13. J.R. Hindley and J.P. Seldin. Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, 2008. Google Scholar
  14. N. Hirokawa and G. Moser. Automated complexity analysis based on context-sensitive rewriting. In G. Dowek, editor, Proc. Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, volume 8560 of LNCS (ARCoSS), pages 257-271. Springer, 2014. doi: \doi10.1007/978-3-319-08918-8_18. Google Scholar
  15. G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems, I. In J.L. Lassez and G. Plotkin, editors, Computational Logic - Essays in Honor of Alan Robinson, pages 395-414. The MIT Press, 1991. Google Scholar
  16. G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems, II. In J.L. Lassez and G. Plotkin, editors, Computational Logic - Essays in Honor of Alan Robinson, pages 415-443. The MIT Press, 1991. Google Scholar
  17. R. Kashima. A proof of the standardization theorem in λ-calculus. Research Reports on Mathematical and Computing Sciences C-145, Tokyo Institute of Technology, 2000. Google Scholar
  18. S. Lucas. Needed reductions with context-sensitive rewriting. In M. Hanus, J. Heering, and K. Meinke, editors, Proc. 6th International Conference on Algebraic and Logic Programming, volume 1298 of LNCS, pages 129-143, 1997. doi: \doi10.1007/BFb0027007. Google Scholar
  19. V. . Normalisation in weakly orthogonal rewriting. In P. Narendran and M. Rusinowitch, editors, Proc. 10th International Conference on Rewriting Techniques and Applications, volume 1631 of LNCS, pages 60-74. Springer, 1999. doi: \doi10.1007/3-540-48685-2_5. Google Scholar
  20. M.J. O'Donnell. Computing in Systems Described by Equations, volume 58 of LNCS. Springer, 1977. doi: \doi10.1007/3-540-08531-9. Google Scholar
  21. J. van de Pol. JITty: A rewriter with strategy annotations. In S. Tison, editor, Proc. 13th International Conference on Rewriting Techniques and Applications, volume 2378 of LNCS, pages 367-370. Springer, 2002. doi: \doi10.1007/3-540-45610-4_26. Google Scholar
  22. M. Takahashi. Lambda-calculi with conditional rules. In M. Bezem and J.F. Groote, editors, Proc. International Conference on Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 406-417. Springer, 1993. doi: \doi10.1007/BFb0037121. Google Scholar
  23. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  24. Y. Toyama. Strong sequentiality of left-linear overlapping term rewriting systems. In Proc. 7th Annual Symposium on Logic in Computer Science, pages 274-284. IEEE Computer Society, 1992. doi: \doi10.1109/LICS.1992.185540. Google Scholar
  25. Y. Toyama. Reduction strategies for left-linear term rewriting systems. In A. Middeldorp, V. van Oostrom, F. van Raamsdonk, and R.C. de Vrijer, editors, Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of his 60th Birthday, volume 3838 of LNCS, pages 198-223, 2005. doi: \doi10.1007/11601548_13. 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