Semi-Unification and Type Inference

• To: types@theory.LCS.MIT.EDU
• Subject: Semi-Unification and Type Inference
• From: Dr. Hans Leiss <leiss%inf21@ztivax.siemens.com>
• Date: Thu, 19 Oct 89 12:07:27 EDT
• Sender: meyer@theory.LCS.MIT.EDU

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

• Prev: Earthquake
• Next: Undecidable Second-order Type-Scheme Problem
• Index(es):
  • Main
  • Thread