2026-07-25T15:15:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9197 2024-03-06T10:43:36Z ddc:004 open_access

Homogeneity Without Loss of Generality Parys, Pawel higher-order recursion schemes lambda-calculus homogeneous types safe schemes 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pawel Parys 2018 Is Part Of LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2018.27 urn:nbn:de:0030-drops-91972 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.27 eng https://creativecommons.org/licenses/by/3.0/legalcode