[Next] [Previous] [Up]

#### Problem # 21

Submitted by Paweł Urzyczyn

Date: 2007

Statement. Is higher-order matching decidable with many atoms?

[PRINT this PROBLEM]

It has recently been proved [Stirling, 2009] that the higher-order matching
problem is decidable. However, the proof method only applies to the “classical”
case of the problem: when all types are built from a single atom. Therefore, the
problem remains open for the generalized case of types built from an arbitrary
number of type variables.

A special case of the higher-order matching problem is the retraction problem,
ﬁrst mentioned in [de’Liguoro et al., 1992]. We say that a type is a retract of
a type (write ) iff there exists a type environment and terms

such that . The problem to decide if holds for given and
is decidable for a single atom [Padovani, 2001] but for many atoms it
remains an open question. For a discussion see [Regnier and Urzyczyn,
2001].
Even less is known about polymorphic retractions. For instance, it is
conjectured that and implies that and are isomorphic. A
conﬁrmation of this conjecture yields a negative answer to Problem 17,
see [Regnier and Urzyczyn, 2001].

##### References for # 21

[de’Liguoro et al., 1992] de’Liguoro, U., Piperno, A., and Statman, R.
(1992). Retracts in simply typed lambda-beta-eta-calculus. In Logic in
Computer Science, pages 461–469. IEEE Computer Society Press.

[Padovani, 2001] Padovani, V. (2001). Retracts in simple types. In
Abramsky, S., editor, Typed Lambda Calculi and Applications, volume 2044
of Lecture Notes in Computer Science, pages 376–384. Springer-Verlag.

[Regnier and Urzyczyn, 2001] Regnier, L. and Urzyczyn, P. (2001).
Retractions of types with many atoms. Technical Report 29, IML
Marseille. http://arxiv.org/abs/cs/0212005.

[Stirling, 2009] Stirling, C. (2009). Decidability of higher-order
matching. Logical Methods in Computer Science, 5(3).

[Next] [Previous] [Up]

Last modified: July 21, 2014