LIPIcs.FSCD.2018.27.pdf
- Filesize: 470 kB
- 15 pages
Document
Homogeneity Without Loss of Generality
Author
-
Part of:
Volume:
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-07-04
Cite As Get BibTex
Pawel Parys. Homogeneity Without Loss of Generality. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.27
Abstract
We consider higher-order recursion schemes as generators of infinite trees. A sort (simple type) is called homogeneous when all arguments of higher order are taken before any arguments of lower order. We prove that every scheme can be converted into an equivalent one (i.e, generating the same tree) that is homogeneous, that is, uses only homogeneous sorts. Then, we prove the same for safe schemes: every safe scheme can be converted into an equivalent safe homogeneous scheme. Furthermore, we compare two definition of safe schemes: the original definition of Damm, and the modern one. Finally, we prove a lemma which illustrates usefulness of the homogeneity assumption. The results are known, but we prove them in a novel way: by directly manipulating considered schemes.
Subject Classification
ACM Subject Classification
- Theory of computation → Rewrite systems
Keywords
- higher-order recursion schemes
- lambda-calculus
- homogeneous types
- safe schemes
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Alfred V. Aho. Indexed grammars - an extension of context-free grammars. J. ACM, 15(4):647-671, 1968. URL: http://dx.doi.org/10.1145/321479.321488.
- William Blum. Type homogeneity is not a restriction for safe recursion schemes. CoRR, abs/1701.02118, 2017. URL: http://arxiv.org/abs/1701.02118.
- William Blum and C.-H. Luke Ong. The safe lambda calculus. Logical Methods in Computer Science, 5(1), 2009. URL: http://dx.doi.org/10.2168/LMCS-5(1:3)2009.
- Luca Breveglieri, Alessandra Cherubini, Claudio Citrini, and Stefano Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996. URL: http://dx.doi.org/10.1142/S0129054196000191.
- Christopher H. Broadbent. On collapsible pushdown automata, their graphs and the power of links. PhD thesis, University of Oxford, 2011. URL: https://ora.ox.ac.uk/objects/uuid:aaa328fe-60be-4abe-8f84-97dbd9e0a3fe.
- Arnaud Carayol and Olivier Serre. Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 165-174, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.73.
- Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered tree-pushdown systems. In 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, pages 163-177, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.163.
- Łukasz Czajka. Coinductive techniques in infinitary lambda-calculus. CoRR, abs/1501.04354, 2015. URL: http://arxiv.org/abs/1501.04354.
- Werner Damm. The IO- and OI-hierarchies. Theor. Comput. Sci., 20:95-207, 1982. URL: http://dx.doi.org/10.1016/0304-3975(82)90009-3.
- Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 452-461, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.34.
- Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theor. Comput. Sci., 175(1):93-125, 1997. URL: http://dx.doi.org/10.1016/S0304-3975(96)00171-5.
- Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries. Meaningless terms in rewriting. Journal of Functional and Logic Programming, 1999(1), 1999. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-01/A99-01.html.
- Teodor Knapik, Damian Niwinski, and Paweł Urzyczyn. Deciding monadic theories of hyperalgebraic trees. In TLCA, pages 253-267, 2001. URL: http://dx.doi.org/10.1007/3-540-45413-6_21.
- Teodor Knapik, Damian Niwiński, and Paweł Urzyczyn. Higher-order pushdown trees are easy. In Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, pages 205-222, 2002. URL: http://dx.doi.org/10.1007/3-540-45931-6_15.
- Gregory M. Kobele and Sylvain Salvati. The IO and OI hierarchies revisited. Inf. Comput., 243:205-221, 2015. URL: http://dx.doi.org/10.1016/j.ic.2014.12.015.
- Paweł Parys. On the significance of the collapse operation. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 521-530, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.62.
- Paweł Parys. The complexity of the diagonal problem for recursion schemes. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, pages 45:1-45:14, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2017.45.
- Sylvain Salvati and Igor Walukiewicz. Simply typed fixpoint calculus and collapsible pushdown automata. Mathematical Structures in Computer Science, 26(7):1304-1350, 2016. URL: http://dx.doi.org/10.1017/S0960129514000590.