Abstract
Subtype satisfiability is an important problem for designing advanced subtype systems and subtype-based program analysis algorithms. The problem is well understood if the atomic types form a lattice. However, little is known about subtype satisfiability over posets. In this paper, we investigate algorithms for and the complexity of subtype satisfiability over general posets.We present a uniform treatment of different flavors of subtyping: simple versus recursive types and structural versus non-structural subtype orders.Our results are established through a new connection of subtype constraints and modal logic. As a consequence, we settle a problem left open by Tiuryn and Wand in 1993.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
Ben-Ari, M., Halpern, J.Y., Pnueli, A.: Deterministic propositional dynamic logic: Finite models, complexity, and completeness. Journal of Computer and System Sciences 25(3), 402–417 (1982)
Blackburn, P., Gaiffe, B., Marx, M.: Variable free reasoning on finite trees. In: Proceedings of Mathematics of Language, pp. 17–30 (2003)
Blackburn, P., Meyer-Viol, W.: Linguistics, logic, and finite trees. Logic Journal of the IGPL 2, 3–29 (1994)
Eifrig, J., Smith, S., Trifonov, V.: Sound polymorphic type inference for objects. In: OOPSLA, pp. 169–184 (1995)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18, 194–211 (1979)
Flanagan, C., Felleisen, M.: Componential set-based analysis. ACM Transactions on Programming Languages and Systems 21(2), 370–416 (1999)
Frey, A.: Satisfying subtype inequalities in polynomial space. Theoretical Computer Science 277, 105–117 (2002)
Fuh, Y., Mishra, P.: Type inference with subtypes. Theoretical Computer Science 73(2), 155–175 (1990)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press, Cambridge (2000)
Henglein, F., Rehof, J.: The complexity of subtype entailment for simple types. In: LICS, pp. 362–372 (1997)
Henglein, F., Rehof, J.: Constraint automata and the complexity of recursive subtype entailment. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 616–627. Springer, Heidelberg (1998)
Hoang, M., Mitchell, J.: Lower bounds on type inference with subtypes. In: POPL, pp. 176–185 (1995)
Kozen, D., Palsberg, J., Schwartzbach, M.I.: Efficient inference of partial types. Journal of Computer and System Sciences 49(2), 306–324 (1994)
Kracht, M.: Inessential features. In: Retoré, C. (ed.) LACL 1996. LNCS (LNAI), vol. 1328, pp. 43–62. Springer, Heidelberg (1997)
Kuncak, V., Rinard, M.: Structural subtyping of non-recursive types is decidable. In: LICS, pp. 96–107 (2003)
Mitchell, J.: Coercion and type inference. In: POPL, pp. 175–185 (1984)
Mitchell, J.C.: Type inference with simple subtypes. The Journal of Functional Programming 1(3), 245–285 (1991)
Niehren, J., Priesnitz, T.: Entailment of non-structural subtype constraints. In: Asian Computing Science Conference, pp. 251–265 (1999)
Niehren, J., Priesnitz, T.: Non-structural subtype entailment in automata theory. Information and Computation 186(2), 319–354 (2003)
Niehren, J., Priesnitz, T., Su, Z.: Complexity of subtype satisfiability over posets (2005), Available at http://www.ps.uni-sb.de/papers
Palm, A.: Propositional tense logic for trees. In: Proceedings of the Sixth Meeting on Mathematics of Language, pp. 74–87 (1999)
Palsberg, J., Wand, M., O’Keefe, P.: Type Inference with Non-structural Subtyping. Formal Aspects of Computing 9, 49–67 (1997)
Pottier, F.: Simplifying subtyping constraints. In: ICFP, pp. 122–133 (1996)
Pottier, F.: Type inference in the presence of subtyping: from theory to practice. PhD thesis, INRIA (1998)
Pratt, V., Tiuryn, J.: Satisfiability of inequalities in a poset. Fundamenta Informaticae 28, 165–182 (1996)
Rabin, M.O.: Decidability of second-order theories and automata on infinte trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)
Rehof, J.: The Complexity of Simple Subtyping Systems. PhD thesis, DIKU (1998)
Seidl, H.: Haskell overloading is DEXPTIME-complete. Information Processing Letters 52(2), 57–60 (1994)
Spaan, E.: Complexity of Modal Logics. PhD thesis, University of Amsterdam (1993)
Su, Z., Aiken, A., Niehren, J., Priesnitz, T., Treinen, R.: First-order theory of subtyping constraints. In: POPL, pp. 203–216 (2002)
Tiuryn, J.: Subtype inequalities. In: LICS, pp. 308–315 (1992)
Tiuryn, J., Wand, M.: Type reconstruction with recursive types and atomic subtyping. In: Theory and Practice of Software Development, pp. 686–701 (1993)
Trifonov, V., Smith, S.: Subtyping constrained types. In: SAS, pp. 349–365 (1996)
Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. Journal Computer & System Science 32(2), 183–221 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Niehren, J., Priesnitz, T., Su, Z. (2005). Complexity of Subtype Satisfiability over Posets. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)