  |
First-Order Theory of Subtyping Constraints
Author: Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf TreinenEditor:
We investigate the first-order theory of subtyping constraints. We show
that the first-order theory of non-structural 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
non-structural 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.
|