The first-order theory of subtyping constraints

ABSTRACT

We investigate the first-order of subtyping constraints. We show that the first-order theory of non-structural subtyping is undecidable, and we show that in the case where all constructors are either unary or nullary, the first-order theory is decidable for both structural and non-structural subtyping. The decidability results are shown by reduction to a decision problem on tree automata. This work is a step towards resolving long-standing open problems of the decidability of entailment for non-structural subtyping.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165188]
• 2: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 3: Alexander Aiken , Edward L. Wimmers , Jens Palsberg, Optimal Representations of Polymorphic Types with Subtyping (Extended Abstract), Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.47-76, September 23-26, 1997
• 4: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 5: L. O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen, May 1994. DIKU report 94/19.
• 6: Alexandre Boudet , Hubert Comon, Diophantine Equations, Presburger Arithmetic and Finite Automata, Proceedings of the 21st International Colloquium on Trees in Algebra and Programming, p.30-43, April 22-24, 1996
• 7: J. B. uchi. Weak second order logic and finite automata. Z. Math. Logik, Grundlag. Math., 5:66-62, 1960.
• 8: H. Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387-411, 1990.
• 9: H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications. Available on: http://www.grappa.univ-lille3.fr/tata, 1999.
• 10: Hubert Comon , Ralf Treinen, Ordering Constraints on Trees, Proceedings of the 19th International Colloquium on Trees in Algebra and Programming, p.1-14, April 11-13, 1994
• 11: Hubert Comon , Ralf Treinen, The first-order theory of lexicographic path orderings is undecidable, Theoretical Computer Science, v.176 n.1-2, p.67-87, April 20, 1997 [doi>10.1016/S0304-3975(96)00049-7]
• 12: Manuel Fahndrich , Alex Aiken, Making Set-Constraint Program Analyses Scale, University of California at Berkeley, Berkeley, CA, 1996
• 13: Cormac Flanagan , Matthias Felleisen, Componential set-based analysis, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.235-248, June 16-18, 1997, Las Vegas, Nevada, United States
• 14: Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Stephanie Weirich , Matthias Felleisen, Catching bugs in the web of program invariants, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.23-32, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 15: F. Gecseg and M. Steinby. Tree Automata. Akademiai Kiado, 1984.
• 16: Nevin Heintze, Set-based analysis of ML programs, Proceedings of the 1994 ACM conference on LISP and functional programming, p.306-317, June 27-29, 1994, Orlando, Florida, United States
• 17: F. Henglein , J. Rehof, The complexity of subtype entailment for simple types, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.352, June 29-July 02, 1997
• 18: Fritz Henglein , Jakob Rehof, Constraint Automata and the Complexity of Recursive Subtype Entailment, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.616-627, July 13-17, 1998
• 19: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient recursive subtyping, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.419-428, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158700]
• 20: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient inference of partial types, Journal of Computer and System Sciences, v.49 n.2, p.306-324, Oct. 1994 [doi>10.1016/S0022-0000(05)80051-0]
• 21: M.J. Maher. Complete axiomatizations of the algebras of the finite, rational and infinite trees. In Proceedings of the Third IEEE Symposium on Logic in Computer Science, pages 348-357, Edinburgh, UK, 1988. Computer Society Press.
• 22: Simon Marlow , Philip Wadler, A practical subtyping system for Erlang, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.136-149, June 09-11, 1997, Amsterdam, The Netherlands
• 23: R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348-375, December 1978.
• 24: J.C. Mitchell. Type Inference with Simple Types. Journal of Functional Programming, 1(3):245-285, 1991.
• 25: M. M. uller, J. Niehren, and R. Treinen. The first-order theory of ordering constraints over feature trees. Discrete Mathematics and Theoretical Computer Science, 4(2):193-234, September 2001.
• 26: Joachim Niehren , Martin Müller , Jean-Marc Talbot, Entailment of Atomic Set Constraints is PSPACE-Complete, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.285, July 02-05, 1999
• 27: Joachim Niehren , Tim Priesnitz, Entailment of Non-structural Subtype Constraints, Proceedings of the 5th Asian Computing Science Conference on Advances in Computing Science, p.251-265, December 10-12, 1999
• 28: Joachim Niehren , Tim Priesnitz, Non-structural Subtype Entailment in Automata Theory, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.360-384, October 29-31, 2001
• 29: Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
• 30: Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.4, p.576-599, July 1995 [doi>10.1145/210184.210187]
• 31: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type inference, Conference proceedings on Object-oriented programming systems, languages, and applications, p.146-161, October 06-11, 1991, Phoenix, Arizona, United States
• 32: E.L. Post. A Variant of a Recursively Unsolvable Problem. Bull. of the Am. Math. Soc., 52, 1946.
• 33: François Pottier, Simplifying subtyping constraints, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.122-133, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 34: François Pottier, Simplifying subtyping constraints: a theory, Information and Computation, v.170 n.2, p.153-183, November 1, 2001 [doi>10.1006/inco.2001.2963]
• 35: M.O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society, 141:1-35, 1969.
• 36: J. Rehof. The Complexity of Simple Subtyping Systems. PhD thesis, DIKU, 1998.
• 37: O. Shivers, Control flow analysis in scheme, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.164-174, June 20-24, 1988, Atlanta, Georgia, United States
• 38: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 39: Zhendong Su , Alexander Aiken, Entailment with Conditional Equality Constraints, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.170-189, April 02-06, 2001
• 40: Ralf Treinen, A new method for undecidability proofs of first order theories, Journal of Symbolic Computation, v.14 n.5, p.437-457, Nov. 1992 [doi>10.1016/0747-7171(92)90016-W]
• 41: Ralf Treinen, Predicate Logic and Tree Automata with Tests, Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000, p.329-343, March 25-April 02, 2000
• 42: Valery Trifonov , Scott F. Smith, Subtyping Constrained Types, Proceedings of the Third International Symposium on Static Analysis, p.349-365, September 24-26, 1996
• 43: K. N. Venkataraman, Decidability of the purely existential fragment of the theory of term algebras, Journal of the ACM (JACM), v.34 n.2, p.492-510, April 1987 [doi>10.1145/23005.24037]
• 44: Pierre Wolper , Bernard Boigelot, An Automata-Theoretic Approach to Presburger Arithmetic Constraints (Extended Abstract), Proceedings of the Second International Symposium on Static Analysis, p.21-32, September 25-27, 1995