[Next]  [Previous]  [Up]  

Problem # 21

Submitted by Paweł Urzyczyn
Date: 2007
Statement. Is higher-order matching decidable with many atoms?


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, first 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

Γ ⊢ F  : ρ → τ    and     Γ ⊢ G  : τ → ρ
such that G ∘ F = βη I  . 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 confirmation 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]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014