Non-structural Subtype Entailment in Automata Theory

  • Joachim Niehren
  • Tim Priesnitz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


Decidability of non-structural subtype entailment is a long standing open problem in programming language theory. In this paper, we apply automata theoretic methods to characterize the problem equivalently by using regular expressions and word equations. This characterization induces new results on non-structural subtype entailment, constitutes a promising starting point for further investigations on decidability, and explains for the first time why the problem is so difficult. The difficulty is caused by implicit word equations that we make explicit.


Regular Expression Function Symbol Type Inference Automaton Theory Type Constructor 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, September 1993.CrossRefGoogle Scholar
  2. 2.
    F. Baader and K. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Journal of Symbolic Computation, volume 21, pages 211–243, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    V. Durnev. Unsolvability of positive ∀∃ 3-theory of free groups. In Sibirsky mathematichesky jurnal, volume 36(5), pages 1067–1080, 1995. In Russian, also exists in English translation.MathSciNetGoogle Scholar
  4. 4.
    J. Eifrig, S. Smith, and V. Trifonow. Sound polymorphic type inference for objects. In ACM Conference on Object-Oriented Programming: Systems, Languages, and Applications, 1995.Google Scholar
  5. 5.
    J. Eifrig, S. Smith, and V. Trifonow. Type inference for recursively constrained types and its application to object-oriented programming. Elec. Notes in Theor. Comp. Science, 1, 1995.Google Scholar
  6. 6.
    Y. Fuh and P. Mishra. Type inference with subtypes. Theo. Comp. Science, 73, 1990.Google Scholar
  7. 7.
    F. Henglein and J. Rehof. The complexity of subtype entailment for simple types. In Proceedings of the 12th IEEE Symposium on Logic in Computer Science, pages 362–372, 1997.Google Scholar
  8. 8.
    F. Henglein and J. Rehof. Constraint automata and the complexity of recursive subtype entailment. In 25th Int. Conf. on Automata, Languages, & Programming, LNCS, 1998.Google Scholar
  9. 9.
    D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient inference of partial types. Journal of Computer and System Sciences, 49(2):306–324, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5:1–13, 1995.MathSciNetGoogle Scholar
  11. 11.
    G. Makanin. The problem of solvability of equations in a free semigroup. Math. USSR Sbornik, 32, 1977. (English translation).Google Scholar
  12. 12.
    J. C. Mitchell. Type inference with simple subtypes. The Journal of Functional Programming, 1(3):245–285, July 1991.zbMATHCrossRefGoogle Scholar
  13. 13.
    M. Muller, J. Niehren, and R. Treinen. The first-order theory of ordering constraints over feature trees. In IEEE Symposium on Logic in Computer Science, pages 432–443, 1998.Google Scholar
  14. 14.
    J. Niehren, M. Muller, and J.-M. Talbot. Entailment of atomic set constraints is PSPACE-complete. In 14 th IEEE Symposium on Logic in Computer Sience, pages 285–294, 1999.Google Scholar
  15. 15.
    J. Niehren and T. Priesnitz. Entailment of non-structural subtype constraints. In Asian Computing Science Conference, LNCS, pages 251–265. Springer-Verlag, Berlin, 1999.CrossRefGoogle Scholar
  16. 16.
    J. Palsberg, M. Wand, and P. O’Keefe. Type Inference with Non-structural Subtyping. Formal Aspects of Computing, 9:49–67, 1997.zbMATHCrossRefGoogle Scholar
  17. 17.
    W. Plandowski. Satisfiability of word equations with constants is in PSPACE. In Proc. of the 40th IEEE Symp. on Found. of Comp. Science, pages 495–500, 1999.Google Scholar
  18. 18.
    F. Pottier. Simplifying subtyping constraints. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming, pages 122–133, 1996.Google Scholar
  19. 19.
    F. Pottier. A framework for type inference with subtyping. In Proc. of the third ACM SIGPLAN International Conference on Functional Programming, pages 228–238, 1998.Google Scholar
  20. 20.
    F. Pottier. Type inference in the presence of subtyping: from theory to practice. PhD thesis, Institut de Recherche d’Informatique et d’Automatique, 1998.Google Scholar
  21. 21.
    J. Rehof. Minimal typings in atomic subtyping. In ACM Symposium on Principles of Programming Languages. ACM Press, 1997.Google Scholar
  22. 22.
    J. Rehof. The Complexity of Simple Subtyping Systems. PhD thesis, DIKU, Copenh., 1998.Google Scholar
  23. 23.
    K. U. Schulz. Makanin’s algorithm for word equations-two improvements and a generalization. In Word Equations and Related Topics, LNCS 572, pages 85–150, 1991.Google Scholar
  24. 24.
    Y. Vazhenin and B. Rozenblat. Decidability of the positive theory of a free countably generated semigroup. In Math. USSR Sbornik, volume 44, pages 109–116, 1983.zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Joachim Niehren
    • 1
  • Tim Priesnitz
    • 1
  1. 1.Programming Systems LabUniversität des SaarlandesSaarbrückenGermany

Personalised recommendations