eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
33:1
33:15
10.4230/LIPIcs.FSCD.2019.33
article
Sequence Types for Hereditary Permutators
Vial, Pierre
1
Inria, Nantes, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.33/LIPIcs.FSCD.2019.33.pdf
hereditary permutators
Böhm trees
intersection types
coinduction
ridigity
sequence types
non-idempotent intersection