[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.