[Prev][Next][Index][Thread]
ML Type-Checking is DEXP-complete
Date: Fri, 22 Sep 89 17:24:16 EDT
To: types@theory.LCS.MIT.EDU
A TIGHT LOWER BOUND ON THE COMPLEXITY OF THE TYPABILITY PROBLEM IN ML
(A.J. Kfoury, J. Tiuryn, and P. Urzyczyn)
September 22, 1989
With this note we announce that we have proved that the problem of typability
in ML is EXPTIME hard, thereby improving the PSPACE lower bound given in the
paper by P.C. Kanellakis and J.C. Mitchell "Polymorphic unification and ML
typing" (POPL'89). Thus, putting it together with the known EXPTIME algorithm
that solves the problem, it follows that the problem becomes EXPTIME-complete.
The proof uses two intermediate concepts:
-- a special kind of an automaton with two push-down stores, we refer
to it as stratified 2pds automaton,
-- a fragment of the semi-unification problem (see our paper of LICS'89 for the
necessary definitions), to which we refer as acyclic semi-unification
problem.
Then the proof breaks into three steps.
1. A polynomial-time reduction of the problem of acceptance of a PSPACE
Alternating Turing Machine to the problem of boundedness of stratified 2pds
automata (an automaton M is bounded iff there is a constant K such that M
can reach at most K different instantaneous descriptions from any given one).
2. A polynomial-time reduction of the problem of boundedness of stratified
2pds automata to the problem of acyclic semi-unification.
3. A polynomial-time equivalence between acyclic semi-unification and ML
typability. We establish equivalence, rather than one-way reduction, since
we believe that this result may be of independent interest.
All the reductions in 1--3 are relatively natural.