Skip to main content
SpringerLink
Log in

Entailment of Non-structural Subtype Constraints

  • Conference paper
  • First Online:
Advances in Computing Science — ASIAN’99 (ASIAN 1999)

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

Included in the following conference series:

Abstract

Entailment of subtype constraints was introduced for constraint simplification in subtype inference systems. Designing an efficient algorithm for subtype entailment turned out to be surprisingly difficult. The situation was clarified by Rehof and Henglein who proved entailment of structural subtype constraints to be coNP-complete for simple types and PSPACE-complete for recursive types. For entailment of non-structural subtype constraints of both simple and recursive types they proved PSPACE-hardness and conjectured PSPACE-completeness but failed in finding a complete algorithm. In this paper, we investigate the source of complications and isolate a natural subproblem of non-structural subtype entailment that we prove PSPACE-complete. We conjecture (but this is left open) that the presented approach can be extended to the general case.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Aït-Kaci, A. Podelski, and G. Smolka. A feature-based constraint system for logic programming with entailment. Theoretical Computer Science, 122(1-2):263–283, Jan. 1994.

    Article  MATH  MathSciNet  Google Scholar 

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

  3. W. Charatonik and A. Podelski. Set constraints with intersection. In Proceedings of the 12 th IEEE Symposium on Logic in Computer Science, pages 352–361, Warsaw, Poland, 1997.

    Google Scholar 

  4. J. Dörre. Feature logics with weak subsumption constraints. In Annual Meeting of the ACL (Association of Computational Logics), pages 256–263, 1991.Entailment of Non-structural Subtype Constraints 265

    Google Scholar 

  5. J. Dörre and W. C. Rounds. On subsumption and semiunification in feature algebras. In Proceedings of the 5 th IEEE Symposium on Logic in Computer Science, pages 300–310, 1990.

    Google Scholar 

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

  7. J. Eifrig, S. Smith, and V. Trifonow. Type inference for recursively constrained types and its application to object-oriented programming. Elec. Notes in Theoretical Computer Science, 1, 1995.

    Google Scholar 

  8. Y. Fuh and P. Mishra. Type inference with subtypes. Theoretical Computer Science, 73, 1990.

    Google Scholar 

  9. F. Henglein and J. Rehof. The complexity of subtype entailment for simple types. In Proceedings of the 12 th IEEE Symposium on Logic in Computer Science, pages 362–372, Warsaw, Poland, 1997.

    Google Scholar 

  10. F. Henglein and J. Rehof. Constraint automata and the complexity of recursive subtype entailment. In Proceedings of the 25 th Int. Conf. on Automata, Languages, and Programming, LNCS, 1998.

    Google Scholar 

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

    Article  MATH  Google Scholar 

  12. J. C. Mitchell. Foundations for Programming Languages. The MIT Press, Cambridge, MA, 1996.

    Google Scholar 

  13. M. Müller, J. Niehren, and A. Podelski. Ordering constraints over feature trees. Constraints an International Journal, Special Issue on CP’97, 5(1-2), Jan. 2000. To appear.

    Google Scholar 

  14. M. Müller, 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, 21-24 June 1998.

    Google Scholar 

  15. J. Niehren, M. Müller, and J.-M. Talbot. Entailment of atomic set constraints is PSPACEcomplete. In IEEE Symposium on Logic in Computer Sience, 2-5, July 1999. to appear.

    Google Scholar 

  16. F. Pottier. Simplifying subtyping constraints. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming, pages 122–133. ACM Press, New York, May 1996.

    Chapter  Google Scholar 

  17. F. Pottier. A framework for type inference with subtyping. In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming, pages 228–238, Sept. 1998.

    Google Scholar 

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

  19. J. Rehof. Minimal typings in atomic subtyping. In ACM Symposium on Principles of Programming Languages. ACM Press, 1997.

    Google Scholar 

  20. J. Rehof. The Complexity of Simple Subtyping Systems. PhD thesis, DIKU, University of Copenhagen, 1998.

    Google Scholar 

  21. G. Smolka and R. Treinen. Records for logic programming. Journal of Logic Programming, 18(3):229–258, Apr. 1994.

    Article  MATH  MathSciNet  Google Scholar 

  22. V. Trifonov and S. Smith. Subtyping constrained types. In Proceedings of the 3 rd International Static Analysis Symposium, volume 1145 of LNCS, pages 349–365, Aachen, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität des Saarlandes, Programming Systems Lab, 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. Chennai Mathematical Institute, 92 G.N. Chetty Road, T. Nagar, Chennai, 600 017, India

    P. S. Thiagarajan

  2. School of Computing, National University of Singapore, Lower Kent Ridge Road, Singapore, 119260

    Roland Yap

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Niehren, J., Priesnitz, T. (1999). Entailment of Non-structural Subtype Constraints. In: Thiagarajan, P.S., Yap, R. (eds) Advances in Computing Science — ASIAN’99. ASIAN 1999. Lecture Notes in Computer Science, vol 1742. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46674-6_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-46674-6_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66856-5

  • Online ISBN: 978-3-540-46674-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation