Abstract
In this paper, we show the decidability and NP-completeness of the satisfiability problem for non-structural subtyping constraints in quasi-lattices. This problem, first introduced by Smolka in 1989, is important for the typing of logic and functional languages. The decidability result is obtained by generalizing Trifonov and Smith’s algorithm over lattices, to the case of quasi-lattices with a complexity in O(m υ M υ n 3), where m (resp. M) stands for the number of minimal (resp. maximal) elements of the quasi-lattice, v is the number of unbounded variables and n is the number of constraints. Similarly, we extend Pottier’s algorithm for computing explicit solutions to the case of quasi-lattices. Finally we evoke some applications of these results to type inference in constraint logic programming and functional programming languages.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Coquery, E.: Tclp: a generic type checker for constraint logic programs, http://pauillac.inria.fr/~coquery/tclp/
Coquery, E., Fages, F.: From typing constraints to typed constraint systems in CHR. In: Third workshop on Rule-based Constraint Reasoning and Programming, CP 2001, Cyprus (December 2001)
Coquery, E., Fages, F.: Tclp: overloading, subtyping and parametric polymorphism made practical for constraint logic programming. Technical report, INRIA Rocquencourt (2002)
Coquery, E., Fages, F.: Subtyping constraints in quasi-lattices. Technical report, INRIA Rocquencourt (September 2003)
Fages, F., Coquery, E.: Typing constraint logic programs. Theory and Practice of Logic Programming 1 (November 2001)
Frey, A.: Satisfying subtype inequalities in polynomial space. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, Springer, Heidelberg (1997)
Frühwirth, T.: Theory and practice of constraint handling rules. Journal of Logic Programming, Special Issue on Constraint Logic Programming 37(1-3), 95–138 (1998)
Palsberg, J., Zhao, T., Jim, T.: Automatic discovery of covariant read-only fields. In: Ninth International Workshop on Foundations of Object-Oriented Languages (January 2002)
Pottier, F.: A versatile constraint-based type inference system. Nordic Journal of Computing 7(4), 312–347 (2000)
Pottier, F.: Simplifying subtyping constraints: a theory. Information & Computation 170(2), 153–183 (2001)
Pratt, V., Tiuryn, J.: Satisfiability of inequalities in a poset. Fundamenta Informaticae 28(1-2), 165–182 (1996)
Smolka, G.: Logic Programming over Polymorphically Order-Sorted Types. PhD thesis, Universitat Kaiserslautern (1989)
Trifonov, V., Smith, S.: Subtyping constrained types. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 349–365. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coquery, E., Fages, F. (2003). Subtyping Constraints in Quasi-lattices. In: Pandya, P.K., Radhakrishnan, J. (eds) FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2003. Lecture Notes in Computer Science, vol 2914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24597-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-24597-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20680-4
Online ISBN: 978-3-540-24597-1
eBook Packages: Springer Book Archive