Computing with Infinite Terms and Infinite Reductions

• Autorzy: Ketema Jeroen , Simonsen Jakob Grue

Identyfikatory

DOI

10.3233/FI-2019-1866

• Języki publikacji: EN

Abstrakty

EN

We define computable infinitary rewriting by introducing computability to the study of strongly convergent infinite reductions over infinite first-order terms. Given computable infinitary reductions, we show that descendants and origins-essential to proving fundamental properties such as compression and confluence-are computable across such reductions.

Słowa kluczowe

EN

infinitary term rewriting; computability; descendants; origins; needed reductions

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 4
• Strony: 339--365
• Opis fizyczny: Bibliogr. 47 poz., rys.

Twórcy

autor

Ketema Jeroen

• Department of Computing, Imperial College London, London, United Kingdom

autor

Simonsen Jakob Grue

• Department of Computer Science, University of Copenhagen (DIKU), Copenhagen, Denmark

Bibliografia

• [1] Klop JW, van Oostrom V, de Vrijer R. Orthogonality. In: Term Rewriting Systems [28], Chapter 4, pp. 88-148, 2003.
• [2] Weihrauch K. Computable Analysis: An Introduction. Springer, New York, 2000. ISBN-978-3642569999.
• [3] Tucker JV, Zucker JI. Theory of Computation over Stream Algebras, and its Applications. In: Proceedings of the 17th International Symposium on Mathematical Foundations of Computer Science (MFCS’92), volume 629 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1992 pp. 62-80. doi: 0.1007/3-540-55808-X_6.
• [4] Barwise J. Infinitary Logic and Admissible Sets. Journal of Symbolic Logic, 1969. 34(2):226-252. doi:10.2307/2271099.
• [5] Kennaway R, Klop JW, Sleep R, de Vries FJ. Transfinite Reductions in Orthogonal Term Rewriting Systems. Information and Computation, 1995. 119(1):18-38. doi:10.1006/inco.1995.1075.
• [6] Simonsen JG. On modularity in infinitary term rewriting. Information and Computation, 2006. 204(6):957-988. doi:10.1016/j.ic.2006.02.005.
• [7] Kahrs S. Modularity of Convergence and Strong Convergence in Infinitary Rewriting. Logical Methods in Computer Science, 2010. 6(3:18):1-27. doi:10.2168/LMCS-6(3:18)2010.
• [8] Klop JW, de Vrijer RC. Infinitary Normalization. In: We Will Show Them! Essays in Honour of Dov Gabbay, volume 2. College Publications, London. 2005 pp. 169-192. ISBN-978-1904987123.
• [9] Zantema H. Normalization of Infinite Terms. In: Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), volume 5117 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2008 pp. 441-455. doi:10.1007/978-3-540-70590-1_30.
• [10] Kennaway R, Klop JW, Sleep MR, de Vries FJ. Infinitary Lambda Calculus. Theoretical Computer Science, 1997. 175(1):93-125. doi:10.1016/S0304-3975(96)00171-5.
• [11] Barendregt H, Klop JW. Applications of infinitary lambda calculus. Information and Computation, 2009. 207(5):559-582. doi:10.1016/j.ic.2008.09.003.
• [12] Ketema J, Simonsen JG. Infinitary Combinatory Reduction Systems. Information and Computation, 2011. 209(6):893-926. doi:10.1016/j.ic.2011.01.007.
• [13] Ketema J, Simonsen JG. Infinitary Combinatory Reduction Systems: Normalising Reduction Strategies. Logical Methods in Computer Science, 2010. 6(1:7):1-35. doi:10.2168/LMCS-6(1:7)2010.
• [14] Ketema J, Simonsen JG. Infinitary Combinatory Reduction Systems: Confluence. Logical Methods in Computer Science, 2009. 5(4:3):1-29. doi:10.2168/LMCS-5(4:3)2009.
• [15] Bahr P. Infinitary Term Graph Rewriting is Simple, Sound and Complete. In: Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), volume 15 of Leibniz International Proceedings in Informatics. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, 2012 pp. 69-84. doi:10.4230/LIPIcs.RTA.2012.69.
• [16] Bahr P. Modes of Convergence for Term Graph Rewriting. Logical Methods in Computer Science, 2012. 8(2:6):1-60. doi:10.2168/LMCS-8(2:6)2012.
• [17] Kahrs S. Infinitary rewriting: meta-theory and convergence. Acta Informatica, 2007. 44:91-121. doi:10.1007/s00236-007-0043-2.
• [18] Kahrs S. Infinitary Rewriting: Foundations Revisited. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, 2010 pp. 161-176. doi:10.4230/LIPIcs.RTA.2010.161.
• [19] Bahr P. Abstract Models of Transfinite Reductions. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, 2010 pp. 49-66. doi:10.4230/LIPIcs.RTA.2010.49.
• [20] Inverardi P, Zilli MV. Rational Rewriting. In: Proceedings of the 19th International Symposium on Mathematical Foundations of Computer Science (MFCS’94), volume 841 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1994 pp. 433-442. doi:10.1007/3-540-58338-6_90.
• [21] Corradini A, Gadducci F. Rational Term Rewriting. In: Proceedings of the 1st International Conference on Foundations of Software Science and Computation Structure (FoSSaCS’98), volume 1378 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1998 pp. 156-171. doi:10.1007/BFb0053548.
• [22] Corradini A, Drewes F. Term Graph Rewriting and Parallel Term Rewriting. In: Proceedings of the 6th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2011), volume 48 of Electronic Proceedings in Theoretical Computer Science. Open Publishing Association, Australia, 2011 pp. 3-18. doi:10.4204/EPTCS.48.3.
• [23] Aoto T, Ketema J. Rational Term Rewriting Revisited: Decidability and Confluence. In: Proceedings of the 6th International Conference on Graph Transformations (ICGT 2012), volume 7562 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2012 pp. 172-186. doi:10.1007/978-3-642-33654-6_12.
• [24] Vermaat M. Infinitary Rewriting in Coq. Master’s thesis, Vrije Universiteit, Amsterdam, 2010.
• [25] Endrullis J, Hansen HH, Hendriks D, Polonsky A, Silva A. Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic. Logical Methods in Computer Science, 2018. 14(1:3):1-44. doi:10.23638/LMCS-14(1:3)2018.
• [26] Baader F, Nipkow T. Term Rewriting and All That. Cambridge University Press, Cambridge, 1998. ISBN-978-0521779203.
• [27] Klop JW. Term Rewriting Systems. In: Abramsky S, Gabbay D, Maibaum T (eds.), Handbook of Logic in Computer Science, volume 2, pp. 1-116. Oxford University Press, Oxford. 1992. ISBN-978-0198537618.
• [28] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2003. ISBN-978-0521391153.
• [29] Fernàndez M. Models of Computation: An Introduction to Computability Theory. Undergraduate Topics in Computer Science. Springer, New York, 2009. ISBN-978-1848824331.
• [30] Jones ND. Computability and Complexity from a Programming Perspective. The MIT Press, Cambridge, MA, 1997. ISBN-978-0262100649.
• [31] Rogers Jr H. Theory of Recursive Functions and Effective Computability. The MIT Press, Cambridge, MA, paperback edition, 1987. ISBN-978-0262680523.
• [32] Sipser M. Introduction to the Theory of Computation. Thomson Course Technology, Boston, 2nd edition, 2006. ISBN-978-0534950972.
• [33] Kennaway R, de Vries FJ. Infinitary rewriting. In: Term Rewriting Systems [28], Chapter 12, pp. 668-711, 2003.
• [34] Ketema J. Böhm-Like Trees for Rewriting. Ph.D. thesis, Vrije Universiteit, Amsterdam, 2006.
• [35] Courcelle B. Fundamental Properties of Infinite Trees. Theoretical Computer Science, 1983. 25(2):95-169. doi:10.1016/0304-3975(83)90059-2.
• [36] Kleene SC. Recursive Functions and Intuitionistic Mathematics. In: Proceedings of the International Conference of Mathematicians, August 30-September 6, 1950, volume 1. American Mathematical Society, Providence, RI, USA, 1952 pp. 679-685.
• [37] Bauer A. König’s Lemma and the Kleene Tree, 2006. Unpublished tutorial note.
• [38] Bridges D, Richman F. Varieties of Constructive Mathematics, volume 97 of London Mathematical Society Lecture Notes Series. Cambridge University Press, Cambridge, 1987. ISBN-978-0521318020.
• [39] Rodenburg PH. Termination and Confluence in Infinitary Term Rewriting. Journal of Symbolic Logic, 1998. 63(4):1286-1296. doi:10.2307/2586651.
• [40] Miller LW. Normal Functions and Constructive Ordinal Notations. Journal of Symbolic Logic, 1976. 41(2):439-459. doi:10.2307/2272243.
• [41] Kleene SC. On Notation for Ordinal Numbers. Journal of Symbolic Logic, 1938. 3(4):150-155. doi:10.2307/2267778.
• [42] Phillips IC. Recursion Theory. In: Abramsky S, Gabbay DM, Maibaum TSE (eds.), Handbook of Logic in Computer Science, volume 1, pp. 79-188. Oxford University Press, Oxford, 1992. ISBN-978-0198537359.
• [43] Bethke I, Klop JW, de Vrijer RC. Descendants and Origins in Term Rewriting. Information and Computation, 2000. 159(1-2):59-124. doi:10.1006/inco.2000.2876.
• [44] Ketema J. Reinterpreting Compression in Infinitary Rewriting. In: Proceedings of the 23th International Conference on Rewriting Techniques and Applications (RTA 2012), volume 15 of Leibniz International Proceedings in Informatics. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, 2012 pp. 209-224. doi:10.4230/LIPIcs.RTA.2012.209.
• [45] Ko KI. Complexity Theory of Real Functions. Progress in Theoretical Computer Science. Birkhäuser, Boston, 1991. ISBN-978-1468468045.
• [46] Allouche JP, Shallit J. Automatic Sequences: Theory, Application, Generalizations. Cambridge University Press, Cambridge, 2003. ISBN-978-0521823326.
• [47] Bahr P. Modular Implementation of Programming Languages and a Partial-Order Approach to Infinitary Rewriting. Ph.D. thesis, University of Copenhagen, 2012.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).