Abstract
We present a new constraint system called Ines. Its constraints are conjunctions of inclusions \(t_1 \subseteq t_2\)between first-order terms (without set operators) which are interpreted over non-empty sets of trees. The existing systems of set constraints can express Ines constraints only if they include negation. Their satisfiability problem is NEXPTIME-complete. We present an incremental algorithm that solves the satisfiability problem of Ines constraints in cubic time. We intend to apply Ines constraints for type analysis for a concurrent constraint programming language.
Chapter PDF
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
A. Aiken, D. Kozen, and E. Wimmers. Decidability of Systems of Set Constraints with Negative Constraints. Information and Computation, 1995.
A. Aiken and E. Wimmers. Solving Systems of Set Constraints. In Proc. 7 th LICS pp. 329–340. IEEE, 1992.
A. Aiken and E. Wimmers. Type Inclusion Constraints and Type Inference. In Proc. 6 th FPCA, pp. 31–41. 1993.
A. Aiken, E. Wimmers, and T. Lakshman. Soft Typing with Conditional Types. In Proc. 21 st POPL. ACM, 1994.
L. Bachmair, H. Ganzinger, and U. Waldmann. Set Constraints are the Monadic Class. In Proc. 8 th LICS, pp. 75–83. IEEE, 1993.
H. P. Barendregt. The Type Free Lambda Calculus. In Barwise [7], 1977.
J. Barwise, ed. Handbook of Mathematical Logic. Number 90 in Studies in Logic. North-Holland, 1977.
D. Basin and H. Ganzinger. Automated Complexity Analysis Based on Ordered Resolution. In 11 th LICS. IEEE, 1996.
W. Charatonik and L. Pacholski. Negative set constraints with equality. In Proc. 9 th LICS, pp. 128–136. 1994.
W. Charatonik and L. Pacholski. Set constraints with projections are in NEXPTIME. In Proc. 35 th FOCS, pp. 642–653. 1994.
W. Charatonik and A. Podelski. The Independence Property of a Class of Set Constraints. In Proc. 2nd CP. LNCS 1118, Springer, 1996.
H. Comon and P. Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7:371–425. 1989.
R. Gilleron, S. Tison, and M. Tommasi. Solving Systems of Set Constraints with Negated Subset Relationships. In Proc. 34 nd FOCS, pp. 372–380. 1993.
N. Heintze. Set Based Analysis of ML Programs. Technical Report CMU-CS-93-193, School of Computer Science, Carnegie Mellon University. July 1993.
N. Heintze and J. Jaffar. A Decision Procedure for a Class of Set Constraints (Extended Abstract). In Proc. 5 th LICS, pp. 42–51. IEEE, 1990.
D. Kozen. Logical aspects of set constraints. In Proc. CSL, pp. 175–188. 1993.
M. J. Maher. Logic semantics for a class of committed-choice programs. In J.-L. Lassez, ed., Proc. 4 th ICLP, pp. 858–876. The MIT Press, 1987.
M. J. Maher. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In Proc. 3 rd LICS, pp. 348–457. IEEE, 1988.
A. I. Malc'ev. Axiomatizable Classes of Locally Free Algebras of Various Type. In The Metamathematics of Algebraic Systens: Collected Papers 1936–1967, ch. 23, pp. 262–281. North-Holland, 1971.
D. McAllester. Automatic Recognition of Tractability in Inference Relations. Journal of the ACM, 40(2), Apr. 1993.
D. McAllester and R. Givan. Taxonomic Syntax for First-Order Inference. Journal of the ACM, 40(2), Apr. 1993.
D. McAllester, R. Givan, D. Kozen, and C. Witty. Tarskian Set Constraints. In Proc. 11 th LICS. IEEE, 1996.
M. Müller. Type Analysis for a Higher-Order Concurrent Constraint Language. Doctoral Dissertation. Universität des Saarlandes, Technische Fakultät, 66041 Saarbrücken, Germany. In preparation.
M. Müller, J. Niehren, and A. Podelski. Inclusion Constraints over Non-Empty Sets of Trees. Full version: http://www.ps.uni-sb.de/Papers/ines97.html.
J. Niehren. Functional Computation as Concurrent Computation. In 23 rd POPL, pp. 333–343. ACM, 1996.
J. Niehren and M. Müller. Constraints for Free in Concurrent Computation. In Proc. 1 st ASIAN, LNCS 1023, pp. 171–186. Springer, 1995.
The Oz Programming System. Programming Systems Lab, Universität des Saarlandes. Available at http://www.ps.uni-sb.de/www/oz/.
V. A. Saraswat. Concurrent Constraint Programming. The MIT Press, 1993.
G. Smolka. The Oz Programming Model. In J. van Leeuwen, ed., Computer Science Today, LNCS 1000, pp. 324–343. Springer, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Müller, M., Niehren, J., Podelski, A. (1997). Inclusion constraints over non-empty sets of trees. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030609
Download citation
DOI: https://doi.org/10.1007/BFb0030609
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive