[Next] [Previous] [Up]

#### Problem # 20 [SOLVED]

Submitted by Mariangiola Dezani-Ciancaglini

Date: 2006

Statement. Type theoretic characterisation of hereditary permutations

[PRINT this PROBLEM]

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 label does not occur in ;
- each variable occurs exactly once;
- the head variable is the ﬁrst abstracted variable;
- all other variables occur at one level lower than their abstractions.

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.

##### References for # 20

[Barendregt, 1984] Barendregt, H. (1984). The Lambda Calculus. Its
Syntax and Semantics. North-Holland, second edition.

[Bergstra and Klop, 1980] Bergstra, J. A. and Klop, J. W. (1980).
Invertible terms in the lambda calculus. Theoretical Computer Science,
11:19–37.

[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.

[Kurata, 2002] Kurata, T. (2002). Intersection and singleton
type assignment characterizing ﬁnite Böhm-trees. Information and
Computation, 178(1):1–11.

[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 .

[Next] [Previous] [Up]

Last modified: July 21, 2014