Normalisation by Random Descent

Authors Vincent van Oostrom, Yoshihito Toyama



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.32.pdf
  • Filesize: 0.7 MB
  • 18 pages

Document Identifiers

Author Details

Vincent van Oostrom
Yoshihito Toyama

Cite AsGet BibTex

Vincent van Oostrom and Yoshihito Toyama. Normalisation by Random Descent. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.32

Abstract

We present abstract hyper-normalisation results for strategies. These results are then applied to term rewriting systems, both first and higher-order. For example, we show hyper-normalisation of the left--outer strategy for, what we call, left--outer pattern rewrite systems, a class comprising both Combinatory Logic and the lambda-calculus but also systems with critical pairs. Our results apply to strategies that need not be deterministic but do have Newman's random descent property: all reductions to normal form have the same length, with Huet and Lévy's external strategy being an example. Technically, we base our development on supplementing the usual notion of commutation diagram with a notion of order, expressing that the measure of its right leg does not exceed that of its left leg, where measure is an abstraction of the usual notion of length. We give an exact characterisation of such global commutation diagrams, for pairs of reductions, by means of local ones, for pairs of steps, we dub Dyck diagrams.
Keywords
  • strategy
  • hyper-normalisation
  • commutation
  • random descent

Metrics

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

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  2. H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 2nd revised edition, 1984. Google Scholar
  3. H.P. Barendregt, J.R.K. Kennaway, J.W. Klop, and M.R. Sleep. Needed reduction and spine strategies for the lambda calculus. Information &Computation, 75(3):191-231, 1987. URL: http://dx.doi.org/10.1016/0890-5401(87)90001-0.
  4. N. Dershowitz. On lazy commutation. In Languages: From Formal to Natural, volume 5533 of Lecture Notes in Computer Science, pages 59-82. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-01748-3_5.
  5. J.R.W. Glauert, R. Kennaway, and Z. Khasidashvili. Stable results and relative normalization. Journal of Logic and Computation, 10(3):323-348, 2000. URL: http://dx.doi.org/10.1093/logcom/10.3.323.
  6. M. Hanus and C. Prehofer. Higher-order narrowing with definitional trees. In Proceedings of the 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 138-152. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-61464-8_48.
  7. N. Hirokawa, A. Middeldorp, and G. Moser. Leftmost outermost revisited. In Proceedings of the 26th International Conference on Rewriting Techniques and Applications, volume 36 of Leibniz International Proceedings in Informatics, pages 209-222, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2015.209.
  8. Gérard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems, \setcounterRomancnt1\RomanRomancnt. In Computational Logic: Essays in Honor of Alan Robinson. The MIT Press, 1991. (accessed 27-4-2016). URL: http://pauillac.inria.fr/~levy/pubs/81robinson1.pdf.
  9. J.W. Klop. Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit Utrecht, 1980. (accessed 27-4-2016). URL: http://janwillemklop.nl/Jan_Willem_Klop/Bibliography_files/9.PhDthesis-total.pdf.
  10. R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3-29, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(97)00143-6.
  11. P.-A. Melliès. A stability theorem in rewriting theory. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pages 287-298. IEEE Computer Society Press, 1998. URL: http://dx.doi.org/10.1109/LICS.1998.705665.
  12. D. Miller. Unification of simply typed lambda-terms as logic programming. In Proceedings of the 8th International Conference on Logic Programming, pages 253-281. The MIT Press, 1991. (accessed 27-4-2016). URL: http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp91.pdf.
  13. M. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43(2):223-243, 1942. URL: http://dx.doi.org/10.2307/1968867.
  14. M.J. O'Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer, 1977. URL: http://dx.doi.org/10.1007/3-540-08531-9.
  15. V. van Oostrom. Finite family developments. In Proceedings of the 7th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 308-322. Springer, 1997. URL: http://dx.doi.org/10.1007/3-540-62950-5_80.
  16. V. van Oostrom. Random descent. In Proceedings of the 18th International Conference on Rewriting Techniques and Applications, volume 4533 of Lecture Notes in Computer Science, pages 314-328. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73449-9_24.
  17. V. van Oostrom. Confluence by decreasing diagrams - converted. In Proceedings of the 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 306-320. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70590-1_21.
  18. R.C. Sekar and I.V. Ramakrishnan. Programming in equational logic: Beyond strong sequentiality. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 230-241. IEEE Computer Society Press, 1990. URL: http://dx.doi.org/10.1109/LICS.1990.113749.
  19. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  20. Y. Toyama. Strong sequentiality of left-linear overlapping term rewriting systems. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, pages 274-284. IEEE Computer Society Press, 1992. URL: http://dx.doi.org/10.1109/LICS.1992.185540.
  21. Y. Toyama. Reduction strategies for left-linear term rewriting systems. In 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 Lecture Notes in Computer Science, pages 198-223. Springer, 2005. URL: http://dx.doi.org/10.1007/11601548_13.
  22. F. Winkler and B. Buchberger. A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In Proceedings of the Colloquium on Algebra, Combinatorics and Logic in Computer Science, Volume \setcounterRomancnt2\RomanRomancnt, volume 42 of Colloquia Mathematica Societatis J. Bolyai, pages 849-869, 1986. Google Scholar
  23. D.A. Wolfram. The Clausal Theory of Types, volume 21 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993. Google Scholar
  24. H. Zantema, B. König, and H.J.S. Bruggink. Termination of cycle rewriting. In Proceedings of the 25th International Conference on Rewriting Techniques and Applicationsand the 12th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, pages 476-490. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08918-8_33.
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