[Prev][Next][Index][Thread]
semi-unification is undecidable
Date: Mon, 25 Sep 89 14:51:12 EDT
UNDECIDABILITY OF THE SEMI-UNIFICATION PROBLEM
(A.J. Kfoury, J. Tiuryn, and P. Urzyczyn)
September 25, 1989
We are happy to announce the undecidability of the following problem. Given a
finite set of ordered pairs of terms (t1,u1), ..., (tn,un), the terms are over
the language consisting of one binary operation symbol. Are there
substitutions S,R1,...,Rn, such that
Ri(S(ti))=S(ui), holds for every i?
This is the original semi-unification problem, as stated in our LICS'89
paper. The proof of its undecidability procceds as follows.
1. We establish the undecidability of the following problem. Given a
deterministic Turing machine M, does there exist a constant K such that for
every instantaneous description, ID, of M the number of different ID's
reachable from the given one is at most K? The proof of this crucial result
is obtained by easily adopting the proof of the main result of "The
undecidability of the Turing machine IMMORTALITY problem", Harvard Ph.D.
Thesis by Philip K. Hooper, 1965. For the reference to this thesis we are
grateful to Albert R. Meyer.
2. We show a recursive reducibility of the above problem to the problem of
semi-unification.
An immediate consequence of our result is the undecidability of the typability
problem for an extension of ML which allows for a polymorphic recursion. It
follows from our LICS'89 paper where we have established a polynomial-time
equivalence of the semi-unification problem and the above problem.