Efficient recursive subtyping

ABSTRACT

Subtyping in the presence of recursive types for the &lgr;-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.

REFERENCES

• 1: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.104-118, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99600]
• 2: Luca Cardelli, Amber, Proceedings of the Thirteenth Spring School of the LITP on Combinators and Functional Programming Languages, p.21-47, May 06-10, 1985
• 3: Luca Cardelli. Typeful programming. In Lecl. Notes for the IFIP Advanced Seminar on Formal Methods in Programming Language Semantics, 1989.
• 4: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 5: Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci., 25:95-169, 1983.
• 6: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 7: Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. In Proc. 33rd IEEE Symp. Found. Comput. Sci., October 1992. To appear. Also PB-394, Computer Science Department, Aarhus University, April 1992.
• 8: Patrick M. O'Keefe , Mitchell Wand, Type inference for partial types is decidable, Symposium proceedings on 4th European symposium on programming, p.408-417, January 1992, Rennes, France
• 9: Satish Thatte, Type Inference with Partial Types, Proceedings of the 15th International Colloquium on Automata, Languages and Programming, p.615-629, July 11-15, 1988

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures; Procedures, functions, and subroutines

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

General Terms:
Algorithms, Languages