Zhendong Su
Alexander Aiken
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.
- 1.A. Aiken and E. Wimmers. Type Inclusion Constraints and Type Inference. In Proceedings of the 1993 Conference on Functional Programming Languages and Computer Architecture, pages 31-41, Copenhagen, Denmark, June 1993.]] Google Scholar
Digital Library
- 2.A. Aiken, E. Wimmers, and T.K. Lakshman. Soft Typing with Conditional Types. In Proceedings of the 21th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 163-173, January 1994.]] Google ScholarDigital Library
- 3.A. Aiken, E. Wimmers, and J. Palsberg. Optimal Representations of Polymorphic Types with Subtyping. In Proceedings of 3rd International Symposium on Theoretical Aspects of Computer Software (TACS'97), pages 47-76, 1997.]] Google ScholarDigital Library
- 4.R. Amadio and L. Cardelli. Subtyping Recursive Types. ACM Transactions on Programming Languages and Systems, 15(4):575-631, 1993.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 6.A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In Proceedings of Trees in Algebra and Programming (CAAP'96), volume 1059 of Lecture Notes in Computer Science, pages 30-43. Springer-Verlag, 1996.]] Google ScholarDigital Library
- 7.J. B. uchi. Weak second order logic and finite automata. Z. Math. Logik, Grundlag. Math., 5:66-62, 1960.]]Google Scholar
- 8.H. Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387-411, 1990.]]Google ScholarCross Ref
- 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.]]Google Scholar
- 10.H. Comon and R. Treinen. Ordering constraints on trees. In S. Tison, editor, Colloquium on Trees in Algebra and Programming, volume 787 of Lecture Notes in Computer Science, pages 1-14, Edinburgh, Scotland, 11-13 April 1994. Springer Verlag.]] Google ScholarDigital Library
- 11.H. Comon and R. Treinen. The first-order theory of lexicographic path orderings is undecidable. Theoretical Computer Science, 176:67-87, April 1997.]] Google ScholarDigital Library
- 12.M. F.ahndrich and A. Aiken. Making Set-Constraint Based Program Analyses Scale. In First Workshop on Set Constraints at CP'96, Cambridge, MA, August 1996. Available as Technical Report CSD-TR-96-917, University of California at Berkeley.]] Google ScholarDigital Library
- 13.C. Flanagan and M. Felleisen. Componential Set-Based Analysis. In Proceedings of the 1997 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 1997.]] Google ScholarDigital Library
- 14.C. Flanagan, M. Flatt, S. Krishnamurthi, S. Weirich, and M. Felleisen. Catching Bugs in the Web of Program Invariants. In Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 23-32, May 1996.]] Google ScholarDigital Library
- 15.F. Gecseg and M. Steinby. Tree Automata. Akademiai Kiado, 1984.]]Google Scholar
- 16.N. Heintze. Set Based Analysis of ML Programs. In Proceedings of the 1994 ACM Conference on LISP and Functional Programming, pages 306-17, June 1994.]] Google ScholarDigital Library
- 17.F. Henglein and J. Rehof. The Complexity of Subtype Entailment for Simple Types. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 352-361, 1997.]] Google ScholarDigital Library
- 18.F. Henglein and J. Rehof. Constraint Automata and the Complexity of Recursive Subtype Entailment. In Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP), pages 616-627, 1998.]] Google ScholarDigital Library
- 19.D. Kozen, J. Palsberg, and M.I. Schwartzbach. Efficient Recursive Subtyping. In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 419-428, 1993.]] Google ScholarDigital Library
- 20.D. Kozen, J. Palsberg, and M.I. Schwartzbach. Efficient Inference of Partial Types. Journal of Computer and System Sciences (JCSS), 49(2):306-324, 1994.]] Google ScholarDigital Library
- 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.]]Google ScholarCross Ref
- 22.S. Marlow and P. Wadler. A Practical Subtyping System For Erlang. In Proceedings of the International Conference on Functional Programming (ICFP '97), pages 136-149, June 1997.]] Google ScholarDigital Library
- 23.R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348-375, December 1978.]]Google ScholarCross Ref
- 24.J.C. Mitchell. Type Inference with Simple Types. Journal of Functional Programming, 1(3):245-285, 1991.]]Google ScholarCross Ref
- 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.]]Google Scholar
- 26.J. Niehren, M. M. uller, and J. Talbot. Entailment of Atomic Set Constraints is PSPACE-Complete. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 285-294, 1999.]] Google ScholarDigital Library
- 27.J. Niehren and T. Priesnitz. Entailment of Non- Structural Subtype Constraints. In Asian Computing Science Conference, number 1742 in LNCS, pages 251- 265. Springer, December 1999.]] Google ScholarDigital Library
- 28.J. Niehren and T. Priesnitz. Non-Structural Subtype Entailment in Automata Theory. In Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS'01), number 2215 in LNCS, pages 360-384. Springer, 2001.]] Google ScholarDigital Library
- 29.M. Odersky and P. Wadler. Pizza into Java: Translating theory into practice. In Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 146-159, Paris, France, January 1997.]] Google ScholarDigital Library
- 30.J. Palsberg and P. O'Keefe. A Type System Equivalent to Flow Analysis. ACM Transactions on Programming Languages and Systems, 17(4):576-599, 1995.]] Google ScholarDigital Library
- 31.J. Palsberg and M. I. Schwartzbach. Object-Oriented Type Inference. In Proceedings of the ACM Conference on Object-Oriented programming: Systems, Languages, and Applications, pages 146-161, October 1991.]] Google ScholarDigital Library
- 32.E.L. Post. A Variant of a Recursively Unsolvable Problem. Bull. of the Am. Math. Soc., 52, 1946.]]Google Scholar
- 33.F. Pottier. Simplifying Subtyping Constraints. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP '96), pages 122-133, May 1996.]] Google ScholarDigital Library
- 34.F. Pottier. Simplifying subtyping constraints: a theory. To appear in Information & Computation, August 2000.]] Google ScholarDigital Library
- 35.M.O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society, 141:1-35, 1969.]]Google Scholar
- 36.J. Rehof. The Complexity of Simple Subtyping Systems. PhD thesis, DIKU, 1998.]]Google Scholar
- 37.O. Shivers. Control Flow Analysis in Scheme. In Proceedings of the 1988 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 164-174, June 1988.]] Google ScholarDigital Library
- 38.B. Steensgaard. Points-to Analysis in Almost Linear Time. In Proceedings of the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 32-41, January 1996.]] Google ScholarDigital Library
- 39.Z. Su and A. Aiken. Entailment with conditional equality constraints. In Proceedings of European Symposium on Programming, pages 170-189, April 2001.]] Google ScholarDigital Library
- 40.R. Treinen. A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14(5):437-457, November 1992.]] Google ScholarDigital Library
- 41.R. Treinen. Predicate logic and tree automata with tests. In J. Tiuryn, editor, Foundations of Software Science and Computation Structures, volume LNCS 1784, pages 329-343. Springer, 2000.]] Google ScholarDigital Library
- 42.V. Trifonov and S. Smith. Subtyping Constrained Types. In Proceedings of the 3rd International Static Analysis Symposium, pages 349-365, September 1996.]] Google ScholarDigital Library
- 43.K.N. Venkataraman. Decidability of the purely existential fragment of the theory of term algebras. Journal of the ACM, 34(2):492-510, April 1987.]] Google ScholarDigital Library
- 44.P. Wolper and B. Boigelot. An automata-theoretic approach to presburger arithmetic constraints. In Static Analysis Symposium, pages 21-32, 1995.]] Google ScholarDigital Library
- The first-order theory of subtyping constraints
Recommendations
The first-order theory of subtyping constraints
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 ...
Proof Theory for First Order Łukasiewicz Logic
TABLEAUX '07: Proceedings of the 16th international conference on Automated Reasoning with Analytic Tableaux and Related MethodsAn approximate Herbrand theorem is proved and used to establish Skolemization for first-order ï ukasiewicz logic. Proof systems are then defined in the framework of hypersequents. In particular, extending a hypersequent calculus for propositional ï ...
Higher-order subtyping and its decidability
We define the typed lambda calculus F^ω (F-omega-meet), a natural generalization of Girard's system Fω (F-omega) with intersection types and bounded polymorphism. A novel aspect of our presentation is the use of term rewriting techniques to present ...
Comments