[Prev][Next][Index][Thread]

Semi-Unification and Type Inference



Date: Thu, 19 Oct 89 16:49:04 +0100

    DECIDABILITY OF THE SEMI-UNIFICATION PROBLEM IN TWO VARIABLES
                     (H.Leiss, October 19, 1989)


Concerning the announcement of A.J.Kfoury/J.Tiuryn/P.Urcyczyn of the
undecidability of semi-unification (in the types@theory of Sept 25),
I want to point out that in June '89 I have shown decidability of the 
semi-unification problem in two variables. This has been reported at
the Computer Science Logic '89 conference, and the paper will (hope-
fully) appear in the proceedings to be published as Springer LNCS.
It also contains a reduction calculus for semi-unification problems
for which I couldn't find any example of nonterminating reductions.

To me it seems extremely unlikely that unsolvable semi-unification
problems will be generated by typability checks for `natural' ML+ programs.


Hans Leiss, 
Siemens AG, 
Otto-Hahn-Ring 6,
D-8000 Munich 83