Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Theoretical Aspects of Computer Software

TACS 2001: Theoretical Aspects of Computer Software pp 360–384Cite as

Non-structural Subtype Entailment in Automata Theory

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2215))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, September 1993.

    Article  Google Scholar 

  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.

    Article  MATH  MathSciNet  Google Scholar 

  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.

    MathSciNet  Google Scholar 

  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. 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. Y. Fuh and P. Mishra. Type inference with subtypes. Theo. Comp. Science, 73, 1990.

    Google Scholar 

  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. 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. D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient inference of partial types. Journal of Computer and System Sciences, 49(2):306–324, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  10. D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5:1–13, 1995.

    MathSciNet  Google Scholar 

  11. G. Makanin. The problem of solvability of equations in a free semigroup. Math. USSR Sbornik, 32, 1977. (English translation).

    Google Scholar 

  12. J. C. Mitchell. Type inference with simple subtypes. The Journal of Functional Programming, 1(3):245–285, July 1991.

    Article  MATH  Google Scholar 

  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. 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. J. Niehren and T. Priesnitz. Entailment of non-structural subtype constraints. In Asian Computing Science Conference, LNCS, pages 251–265. Springer-Verlag, Berlin, 1999.

    Chapter  Google Scholar 

  16. J. Palsberg, M. Wand, and P. O’Keefe. Type Inference with Non-structural Subtyping. Formal Aspects of Computing, 9:49–67, 1997.

    Article  MATH  Google Scholar 

  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. F. Pottier. Simplifying subtyping constraints. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming, pages 122–133, 1996.

    Google Scholar 

  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. 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. J. Rehof. Minimal typings in atomic subtyping. In ACM Symposium on Principles of Programming Languages. ACM Press, 1997.

    Google Scholar 

  22. J. Rehof. The Complexity of Simple Subtyping Systems. PhD thesis, DIKU, Copenh., 1998.

    Google Scholar 

  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. 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.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Systems Lab, Universität des Saarlandes, Saarbrücken, Germany

    Joachim Niehren & Tim Priesnitz

Authors
  1. Joachim Niehren
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tim Priesnitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Tokyo Institute of Technology Graduate School of Information Science and Engineering, 2-12-1 Oo-okayama, Meguro-ku, Tokyo, 152-8552, Japan

    Naoki Kobayashi

  2. Department of Computer and Information Science, University of Pennsylvania, 200 S. 33rd St., Philadelphia, PA, 19104, USA

    Benjamin C. Pierce

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Niehren, J., Priesnitz, T. (2001). Non-structural Subtype Entailment in Automata Theory. In: Kobayashi, N., Pierce, B.C. (eds) Theoretical Aspects of Computer Software. TACS 2001. Lecture Notes in Computer Science, vol 2215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45500-0_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-45500-0_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42736-0

  • Online ISBN: 978-3-540-45500-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation