An analysis of ML typability
Assaf J. Kfoury, Jerzy Tiuryn, Paweł Urzyczyn · Journal of the ACM · 1994
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 0(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 can be reduced to each other in polynomial time. We believe this result is of independent interest.