Efficient Recursive Subtyping

Abstract

Subtyping in the presence of recursive types for the lambda-calculus was studied by Amadio and Cardelli in 1991. They showed that the problem of deciding whether one recursive type is a subtype of another is decidable in exponential time.

In this paper we give an O(n^2) 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 Böhm order can be decided efficiently by means of finite automata. Our results extend the automata-theoretic approach to handle orderings based on contravariance.