On non-structural subtype entailment
Aleksy Schubert
TL;DR
This paper proves that the non-structural subtype entailment problem for finite and regular type expressions is decidable within PSPACE, resolving a long-standing open question since 1996.
Contribution
It establishes the PSPACE complexity of the non-structural subtype entailment problem, closing a gap in the understanding of its decidability and complexity.
Findings
The problem is in PSPACE.
Decidability of the problem is confirmed.
Closes a gap since 1996.
Abstract
We prove that the non-structural subtype entailment problem for finite and regular type expressions is in PSPACE. In this way we close a decidability and complexity gap pending since 1996.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · semigroups and automata theory · Logic, Reasoning, and Knowledge