[TYPES] Decidability of polymorphic recursion revisited

[camarao at dcc.ufmg.br]

> Has the issue involving type inferece algorithm from the article
> "Decidable Type Inference For Polymorphic Recursion" by Lucilia
> Figueiredo and Carlos Camarao and undecidability of the problem been
> resolved or is it an "open problem"?

It is not an open problem. Typability in the Milner-Mycroft calculus
[1] is equivalent to decidability of the semi-unification problem
(SUP) [2], and that is undecidable [3].

For years we believed that we had constructed a proof of SUP's
decidability. We found an error in that argumentation, after some
time. The work mentioned in your question was not published (thanks to
referees) because it contradicted an already published proof of the
contrary (in which no error was found).

You might wish to read a draft of a paper we are working on (available
from www.dcc.ufmg.br/~camarao/SUP), about the nice correspondence
(discovered in [3]) between SUP instances and intercell
Turing-Machines (ITMs). One direction (ITM->SUP) is fundamental to the
proof of SUP's undecidability in [3]. Looking at the other direction,
we characterize when SUP is decidable, and when it is not (very
rarely). The abstract is below.

Regards,

Carlos

=====================================================================
"The undecidability of the semi-unification problem (\SUP) has been
proved by Kfoury, Tiuryn and Urzyczyn, using a reduction from the
boundedness problem for Turing Machines. The proof is based on
constructing, for any given symmetric intercell Turing Machine (SITM)
{\em M}, an instance $\Gamma$ of \SUP\ such that $M$ is bounded if and
only if $\Gamma$ has a solution. In this paper we do the reverse,
i.e.~for an arbitrary instance $\Gamma$ of \SUP\ we construct a SITM
$\mathbb{I}(\Gamma)$ which gives an interpretation for $\Gamma$ with
the properties, proved in this paper, that, not only $\Gamma$ has a
solution if and only if $\mathbb{I}(\Gamma)$ is bounded, but also that
if $\Gamma$ has no solution then: i) if Henglein's rewriting system
does not terminate with input $\Gamma$, then $\mathbb{I}(\Gamma)$ has
a wandering configuration, and ii) if Henglein's rewriting system does
terminate with input $\Gamma$ (and $\Gamma$ has no solution), then
$\mathbb{I}(\Gamma)$ has a resiling configuration (i.e.~a periodic
configuration that is the initial configuration of a computation
history with non-zero tape span).

The interpretation of an arbitrary semi-unification instance $\Gamma$
of \SUP\ is done by defining, for each equation or inequality of
$\Gamma$, a corresponding {\em path equation\/} induced by $\Gamma$ (a
concept introduced by Kfoury et al.). We prove that for each path
equation induced by an arbitrary instance $\Gamma$ of \SUP\ there
exist computation histories of $\mathbb{I}(\Gamma)$ of a certain form
and, vice-versa, each computation history of $\mathbb{I}(\Gamma)$ is
contained in the set of computation histories represented by a path
equation induced by $\Gamma$.

Using this framework, we distinguish subclasses of \SUP\ that are
decidable from those that are undecidable. We prove that this
characterization separates instances of \SUP\ for which Henglein's
rewriting system for semi-unification does and does not terminate
(this yields examples for which Henglein's rewriting system loops
forever). Our characterization has been inspired by recent work on the
existence of non-periodic configurations of Turing Machines with no
halting configuration, by Blondel, Cassaigne and Nichitiu."

[1] Alan Mycroft,
    Polymorphic type schemes and recursive definitions,
    Proceedings of the International Symposium on Programming, 1984,
    LNCS 167, 217--239, Springer-Verlag.

[2] Fritz Henglein,
    Type Inference with Polymorphic Recursion,
    ACM TOPLAS 1993, 15(2), 253--289.

[3] A.J. Kfoury, J. Tiuryn and P. Urzyczyn,
    The undecidability of the semi-unification problem,
    Information and Computation 1993, 102(1), 83--101.