Joseph (Yossi) Gil
ABSTRACT
We consider the type system formed by a finite set of primitive types such as integer, character, real, etc., and three type construction operators: (i) Cartesian product, (ii) disjoint sum, and (iii) recursive type definitions. Type equivalence is defined to obey the arithmetical rules: commutativity and associativity of product and sum and distributivity of product over sum. We offer a compact representation of the types in this system as multivariate algebraic functions. This type system admits two natural notions of subtyping: "multiplicative", which roughly corresponds to the notion of object-oriented subtyping, and "additive", which seems to be more appropriate in our context. Both kinds of subtyping can be efficiently computed if no recursive definitions are allowed. Our main result is that additive subtyping is undecidable in the general case. Perhaps surprisingly, this undecidability result is by reduction from Hilbert's Tenth Problem (HIO): the solution of Diophantine equations.
- 1.R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575-631, 1993.]] Google Scholar
Digital Library
- 2.K. Arnold and J. Gosling. The Java Programming Language. The Java Series. Addison-Wesley, 1996.]] Google ScholarDigital Library
- 3.J. Auerbach. The #type system. Unpublished Manuscript, IBM T. J. Watson Research Center, P.O. Box 704, Yorktown Heights, NY 10598, 1998.]]Google Scholar
- 4.J. Auerbach, C. Barton, M. Chu-Carroll, and M. Raghavachari. Mockingbird: Flexible stub compilation from pairs of declarations. In M. G. Gouda, editor, The 19 th IEEE International Conference on Distributed Computing Systems (ICDCS), Austin, Texas, May-June 1999.]] Google ScholarDigital Library
- 5.J. Auerbach and M. Chu-Carroll. The Mockingbird system: A compiler based approach to maximally interoperable distributed programming. Technical Report RC20718, IBM T. J. Watson Research Center, EO. Box 704, Yorktown Heights, NY 10598, 1997.]]Google Scholar
- 6.J. Avotins, G. Maughan, and C. Mingins. Language processor construction: The case for YOOCC and TROOPER. In Proceedings of TOOLS USA'95, 1995.]]Google Scholar
- 7.J. Avotins, C. Mingins, and H. Schmidt. Yes! an objectoriented compiler compiler YOOCC. In Proceedings of TOOLS USA'95, 1995.]]Google Scholar
- 8.S. Basu and M.-E Roy. On the combinatorial and algebraic complexity of quantifier elimination. J. ACM, 43(6):1002- 1045, Nov. 1996.]] Google ScholarDigital Library
- 9.M. Brandt and E Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae, 33(4):309-338, May 1998.]] Google ScholarDigital Library
- 10.G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proceeding of the 2 nd GI Conference on Automata Theory and Formal Languages, pages 134-183, New York, 1975. Springer Verlag.]] Google Scholar
- 11.G.E. Collins. Quantifier elimination by cylindrical algebraic decomposition-twenty years of progress. In B. E Caviness and J. R. Johnson, editors, Quantier Elimination and Cylindrical Algebraic Decomposition, pages 8-23. Springer Verlag, New York, 1998.]]Google ScholarCross Ref
- 12.T.H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. MIT Press, Cambridge, Massachusetts, 1990.]] Google ScholarDigital Library
- 13.D. Cox, J. Little, and D. O'Shea. Ideals, Varieties andAlgorithms. Undergraduate Texts in Mathematics. Springer Verlag, second edition, 1996.]] Google ScholarDigital Library
- 14.E Datum. Subtyping with union types, intersection types and recursive types. In Hagiya and Mitchell {20}, pages 687-706.]] Google Scholar
- 15.J. Davenport and J. Heintz. Real quantifier elimination if doubly exponential. J. Symb. Comput., 5:29-35, 1988.]] Google ScholarDigital Library
- 16.R. Di Cosmo. Isomorphisms of Types: from A-calculus to information retrieval and language design. Birkhiuser, 1995.]] Google ScholarDigital Library
- 17.J. Gil and D. H. Lorenz. SOOP - A synthesizer of an objectoriented parser. In Proceedings of the 16 International Conference on Technology of Object-Oriented Languages and Systems, pages 81-96, Versailles, France, Mar. 6-10 1995. TOOLS 16 Europe Conference, Prentice-Hall.]]Google Scholar
- 18.C. F. Goldfarb. The SGML Handbook. Clarendon Press, Oxford, 1990.]] Google ScholarDigital Library
- 19.C. E Goldfarb and P. Prescod. The XML Handbook. Charles E Goldfarb Series. Prentice-Hall, 1998.]] Google ScholarDigital Library
- 20.M. Hagiya and J. C. Mitchell, editors. Proceedings of the 2 nd International Symposium on Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, Sendai, Japan, Apr. 1994. Springer Verlag.]] Google ScholarDigital Library
- 21.M. Hofri. Probabilistic Analysis of Algorithms. Springer- Verlag New York Inc., 1987.]] Google ScholarDigital Library
- 22.J. Ichibia, editor. Ada Programming Language. ANSI/MIL- STD-1815A. Ada Joint Program Office, Department of Defense, Washington, DC, 1983.]]Google Scholar
- 23.C. B. Jay. The FISh programming definition. Available as http: //www-sta f f.mcs .uts. edu. au/au/~cbj/- Publications/lastest_fish.ps. gz, Oct. 1998.]]Google Scholar
- 24.J. E Jones. Universal Diophantine equation. Journal of Symbolic Logic, 47(3):547-571, 1982.]]Google ScholarCross Ref
- 25.B. W. Kernighan and D. M. Ritchie. The C Programming Language. Software Series. Prentice-Hail, second edition, 1988.]] Google ScholarDigital Library
- 26.D. Kozen, J. Palsberg, and M. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5, 1995.]]Google Scholar
- 27.W. Kuich and A. Salomaa. Semirings, Automata, Languages, volume 5 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1986.]] Google ScholarDigital Library
- 28.L. Lamport. ITEX: A Document Preparation System. Addison-Wesley, 1986.]] Google ScholarDigital Library
- 29.J. V. Matijasevi. Enumerable sets are Diophantine. Soviet Mathematics. Doklady, 11(2):354-358, 1970. This is an English translation of the original paper in Russian (1970).]]Google Scholar
- 30.Y. V. Matiyasevich. Hilbert's tenth problem. MIT Press, 1993.]] Google ScholarDigital Library
- 31.B. Meyer. Object-Oriented Software Construction. Prentice- Hail, second edition, 1997.]] Google ScholarDigital Library
- 32.R. J. Parikh. On context-free languages. J. ACM, 13(4):570- 581, 1966.]] Google ScholarDigital Library
- 33.O. Patashnik. BIBTLfing, 8 Feb. 1988. Documentation for general BIBTEX users.]]Google Scholar
- 34.L. C. Paulson. MLfor the Working Programmer. Cambridge University Press, Cambridge, 1991.]] Google ScholarDigital Library
- 35.M. Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1:71-89, 1991.]]Google ScholarCross Ref
- 36.J. Robinson. Hilbert's tenth problem. In Proc. Syrup. Pure Math., 20, pages 191-194. Amer. Math. Soc., Providence, Rhode Island, 1971.]]Google Scholar
- 37.A. Salomaa. Formal Languages. Academic Press, New York and London, 1973.]] Google ScholarDigital Library
- 38.A. Salomaa and M. Soittola. Automata-Theoretic Aspects of Formal Power Series. Springer-Verlag, 1978.]] Google ScholarDigital Library
- 39.R. Sedgewick and P. Flajolet. An Introduction to the Analysis of Algorithms. Addison-Wesley Publishing Company, Inc., 1996.]] Google ScholarDigital Library
- 40.T. Sekiguchi and A. Yonezawa. A complete type inference system for subtyped recursive types. In Hagiya and Mitchell 20, pages 667-685.]] Google ScholarDigital Library
- 41.B. Stroustrup. The C++ Programming Language. Addison- Wesley, third edition, 1997.]] Google ScholarDigital Library
- 42.A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, CA, second edition, 1951.]]Google Scholar
- 43.N. Wirth. The programming language Pascal. Acta Informatica, 1:35-63, 1971.]]Google ScholarDigital Library
- 44.Recommendation x.208: Speficiation of abstract syntax notation one (ASN.1), Mar. 1988.]]Google Scholar
- 45.R. E. Zippel. Effective Polynomial Computation. Kluwer Academic Publishers, Boston, Dordrecht, London, 1993.]]Google Scholar
Index Terms
- Subtyping arithmetical types
Recommendations
Subtyping arithmetical types
We consider the type system formed by a finite set of primitive types such as integer, character, real, etc., and three type construction operators: (i) Cartesian product, (ii) disjoint sum, and (iii) recursive type definitions. Type equivalence is ...
On subtyping, wildcards, and existential types
FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like ProgramsWildcards are an often confusing part of the Java type system: the behaviour of wildcard types is not fully specified by subtyping, due to wildcard capture, and the rules for type checking are often misunderstood. Their very formulation seems somehow '...
Subtyping recursive types
We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, ...
Comments