2026-07-26T02:11:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10540 2024-03-06T10:46:10Z ddc:004 open_access

Sequence Types for Hereditary Permutators Vial, Pierre hereditary permutators Böhm trees intersection types coinduction ridigity sequence types non-idempotent intersection The invertible terms in Scott’s model D_infty are known as the hereditary permutators. Equivalently, they are terms which are invertible up to beta eta-conversion with respect to the composition of the lambda-terms. Finding a type-theoretic characterization to the set of hereditary permutators was problem # 20 of TLCA list of problems. In 2008, Tatsuta proved that this was not possible with an inductive type system. Building on previous work, we use an infinitary intersection type system based on sequences (i.e., families of types indexed by integers) to characterize hereditary permutators with a unique type. This gives a positive answer to the problem in the coinductive case. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pierre Vial 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.33 urn:nbn:de:0030-drops-105404 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.33 eng https://creativecommons.org/licenses/by/3.0/legalcode