Efficient recursive subtyping

authors: Dexter Kozen, Jens Palsberg, Michael I Schwartzbach
year: 1993
url: https://dl.acm.org/doi/pdf/10.1145/158511.158700
publisher: ACM Press
abstract: Subtyping in the presence of recursive types for the λ-calculus was studied by Amadio and Cardelli in 1991 [1]. In that paper they showed that the problem of deciding whether one recursive type is a sub-type of another is decidable in exponential time. In this paper we give an O(n2) algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states. It is known that equality of recursive types and the covariant Bo¨hm order can be decided efficiently by means of finite automata. Our results extend the automata-theoretic approach to handle orderings based on contravariance.