Submitted by Mariangiola Dezani-Ciancaglini
Statement. Type theoretic characterisation of hereditary permutations
According to [Bergstra and Klop, 1980, Barendregt, 1984] (Deﬁnition 21.2.9) a closed lambda-term is a hereditary permutation if the Böhm tree has the following properties:
The problem is to ﬁnd a type assignment system in which all and only the hereditary
permutations get types of a ﬁxed shape.
Many other sets of -terms have been characterised in this way, see for example [Kurata, 2002, Dezani-Ciancaglini et al., 2005] and the references there.
Solution: Makoto Tatsuta proved [Tatsuta, 2008] that the set of all hereditary permutations is not recursively enumerable, and therefore cannot be characterized by typability in a ﬁnitary type-assignment system. On the other hand, there is a system such that a term can be assigned a certain countably inﬁnite family of types in that system if and only if it is a hereditary permutation.
[Dezani-Ciancaglini et al., 2005] Dezani-Ciancaglini, M., Honsell, F., and Motohama, Y. (2005). Compositional characterization of -terms using intersection types. Theoretical Computer Science, 340(3):459–495.
[Tatsuta, 2008] Tatsuta, M. (2008). Types for hereditary permutators. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA. http://nii.ac.jp/TechReports/07-010E.html .