Submitted by Jakob Rehof
Statement. Is the subtype entailment problem decidable?
Problem Origin. First stated in [Pottier, 1996] and [Trifonov and Smith, 1996]. The present formulation is from [Henglein and Rehof, 1998].
We ask if the entailment problem with simple subtyping constraints over non-structurally ordered trees is decidable. Non-structurally ordered trees have a least element, , and a greatest element, , which can be compared to any tree regardless of its tree domain (shape). Simple type expressions, , are ﬁnite terms built from , and a binary constructor. Such expressions can be interpreted as denoting trees, and formal inequality constraints of the form can consequently be valuated in the non-structural order on trees. For a ﬁnite set of constraints of constraints and terms and , we consider the entailment , or, equivalently, validity of the ﬁrst-order Horn implication , where are the variables occurring in , and .
The problem ﬁrst appears in slightly different forms in the papers [Pottier, 1996] and [Trifonov and Smith, 1996] for the purpose of simplifying subtyping constraints. It was studied in the form presented here in [Henglein and Rehof, 1998] (following the formulation in [Henglein and Rehof, 1997] for simple types), where it was shown to be to be PSPACE-hard. The full ﬁrst-order theory of subtyping constraints has been shown to be undecidable [Su et al., 2002], but the question of decidability of entailment remains open [Rehof, 1998]. Further references can be found in [Rehof, 1998] and [Niehren and Priesnitz, 2003].
[Henglein and Rehof, 1998] Henglein, F. and Rehof, J. (1998). Constraint automata and the complexity of recursive subtype entailment. In International Colloquium on Automata, Languages, and Programming, volume 1443 of Lecture Notes in Computer Science, pages 616–627. Springer-Verlag.
[Su et al., 2002] Su, Z., Aiken, A., Niehren, J., Priesnitz, T., and Treinen, R. (2002). The ﬁrst-order theory of subtyping constraints. In Symposium on Principles of Programming Languages, pages 203–216. ACM Press.
[Trifonov and Smith, 1996] Trifonov, V. and Smith, S. (1996). Subtyping constrained types. In Static Analysis Symposium, volume 1145 of Lecture Notes in Computer Science, pages 349–365. Springer-Verlag.