[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