Abstract
We carry out an analysis of typability of terms in ML. Our main result is that this problem is DEXPTIME-hard, where by DEXPTIME we mean DTIME\((2^{n^{O(1)} } )\). This, together with the known exponential-time algorithm that solves the problem, yields the DEXPTIME-completeness result. This settles an open problem of P. Kanellakis and J.C. Mitchell.
Part of our analysis is an algebraic characterization of ML typability in terms of a restricted form of semi-unification, which we identify as acyclic semi-unification. We prove that ML typability and acyclic semi-unification are log-space equivalent problems. We believe this result is of independent interest.
(Extended Summary)
This work is partly supported by NSF grant CCR-8901647 and by a grant of the Polish Ministry of National Education, No. RP.I.09
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Clément, D., Despeyroux, J., Despeyroux, T., Kahn, G., “A simple applicative language: Mini-ML”, Proc. ACM Conference on Lisp and Functional Programming, pp 13–27, 1986.
Chandra, A.K., Kozen, D. and Stockmeyer, L. “Alternation,” J. Assoc. Comput. Mach. 28:1, pp 114–133, 1981.
Dwork, C., Kanelakis, P., Mitchell, J.C., “On the sequential nature of unification”, J. of Logic Programming, 1, pp 35–50, 1984.
Damas, L. and Milner, R., “Principal type schemes for functional programs,” Proc. 9-th ACM Symp. Principles of Prog. Lang., pp 207–212, 1982.
Henglein, F., “Type inference and semi-unification”, Proc. ACM Symp. LISP and Functional Programming, July 1988.
Kanellakis, P., Mitchell, J.C., “Polymorphic unification and ML typing”, Proc. 16-th Symp. on Principles of Prog. Lang., pp 105–115, Jan 1989.
Kapur, D., Musser, D., Narendran, P., and Stillman, J., “Semi-unification”, Proc. of 8-th Conference on Foundations of Software Technology and Theoretical Computer Science, Pune, India, Dec. 1988.
Kfoury, A.J., Tiuryn, J. and Urzyczyn, P., “Computational consequences and partial solutions of a generalized unification problem”, Proc. of IEEE 4-th LICS 1989.
Kfoury, A.J., Tiuryn, J. and Urzyczyn, P., “Undecidability of the semi-unification problem” Manuscript, October 1989.
Milner, R., “A theory of type polymorphism in programming”, J. of Computer and System Sciences, Vol. 17, pp 348–375, 1978.
Milner, R., “The standard ML core language”, Polymorphism, II (2), October 1985.
Paterson, M.S., Wegman, M.N., “Linear unification”, JCSS, 16, pp 158–167, 1978.
Tyszkiewicz, J. “Typability in the finitely typed lambda calculus is PTIME-complete,” MS thesis, University of Warsaw, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kfoury, A.J., Tiuryn, J., Urzyczyn, P. (1990). ML typability is dexptime-complete. In: Arnold, A. (eds) CAAP '90. CAAP 1990. Lecture Notes in Computer Science, vol 431. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52590-4_50
Download citation
DOI: https://doi.org/10.1007/3-540-52590-4_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52590-5
Online ISBN: 978-3-540-47042-7
eBook Packages: Springer Book Archive