The first-order theory of subtyping constraints

We investigate the first-order theory of subtyping constraints. We show that the first-order theory of nonstructural subtyping is undecidable, and we show that in the case where all constructors are either unary or nullary, the first-order theory is decidable for both structural and nonstructural subtyping. The decidability results are shown by reduction to a decision problem on tree automata. This work is a step towards resolving long-standing open problems of the decidability of entailment for non-structural subtyping.

• Type: Conference
• Year: 2002
• Where: POPL
• Authors: Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, Ralf Treinen
• Keywords: First-order Theory, Long-standing Open Problems, Nonstructural Subtyping, POPL 2002, Programming Languages