[Prev][Next][Index][Thread]
Re: Decidable polymorphic recursion?
At 1/11/2002 02:13 PM -0200, Carlos Camarao de Figueiredo wrote:
>Francois Pottier writes:
>> I have had a quick look at your paper. I must be missing something
>> obvious, but I fail to understand how it doesn't contradict
>> Henglein's undecidability result. Henglein proves that
>> semi-unification is reducible to typability in ML+FIX (i.e. given an
>> expression, is there a valid typing judgement for it?). As far as as
>> I understand, your paper claims:
>>
>> 1. typability in ML+FIX is equivalent to typability in ML'+FIX'.
>> 2. typability in ML'+FIX' is decidable, since algorithm T0 computes principal
>> typings.
>>
>> Taken together, these facts lead to a contradiction. What am I missing?
>> I would very much like to understand where the subtlety lies.
>
>Well... we believe that Henglein's proof [1] that semiunification is
>reducible to type inference for ML+FIX has an incorrection, in theorem
>3 (page 268), which states the equivalence of type systems MM' and
>MM'' (defined in the paper). By rule (TAUT'') we can derive, for
>example, A{x:a},a |- x:Int, since (a,a) <= (Int,a) (where (M1,M2) <=
>(N1,N2) is defined in page 262, 1st paragraph). However A{x:a} |-
>x:Int cannot be derived in MM'.
>
>[1] F. Henglein, Type inference with polymorphic recursion,
> ACM TOPLAS, 253--289, 15(2), 1993.
The reduction from MM' to MM'' in my TOPLAS 1993 paper [henglein93c]
indeed has a subtle, yet rather easily fixed error. It was absent in
both my thesis [he89a] and the first publication of this reduction, my
LFP 88 paper [he88c]. But that error has nothing to do with the
undecidability of polymorphic recursion (Milner-Mycroft typability)
since it occurs in the reduction of polymorphic recursion to
semiunification, not in the reduction the other way round.
[The error in my paper, by the way, was caught by Mikael Rittri in 94.
His fix and my own fix are described in his paper on dimension
inference [rittri95]. His description of my fix is rather brief. It
is the one that results in basically the same reduction as in my
thesis and which I intended to -- but evidently failed to -- capture
in a compositional manner in the TOPLAS paper. If there is interest
in it I can present the fix and the intuition behind it in this
forum.]
Below I'll make some remarks about the decidability claim in the paper
by Figueiredo and Camarao, and why I'm willing to wage basically any
amount that that claim is false.
The undecidability of Milner-Mycroft typability is a consequence of
(a) the undecidability of semiunifiability, and
(b) the (effective) reducibility of semiunifiability to Milner-Mycroft
typability.
ad (a) Undecidability of semiunifiability was shown by Kfoury, Tiuryn
and Urzyczyn [ktu90b, ktu93] in a reduction from Hooper's
undedicability proof for the 'mortality problem' for Turing Machines.
ad (b) Reducibility of semiunifiability to Milner-Mycroft typability
is proved independently by Kfoury, Tiuryn and Urzyczyn, and myself in
a number of papers, including my thesis [he89a, ktu89, henglein93c,
ktu93b]. It is covered in Section 4.2 of my TOPLAS paper,
pp. 273-277. Note that the above post erroneously states that the
error in the reduction from MM' to MM'' occurs in my "proof [1] that
semiunification is reducible to type inference". It's in the converse
direction.
To attack undecidability of Milner-Mycroft typability you have to find
an unfixable error in at least one of those two results, that is
identify an error and give a watertight proof of the opposite. At the
risk of sounding unfriendly: I bet you can't.
This is a slippery area of research, indeed it has a history of too
optimistic complexity claims, including published papers in highly
esteemed conferences, claiming e.g. feasible type inference for
Damas-Milner (ML) typing and System F, and -- yes, we have had it
before, more than 10 years ago -- decidability of Milner-Mycroft
typability. But now we know better.
Fritz
References:
@inproceedings{he88c,
AUTHOR = "Henglein, Fritz",
BOOKTITLE = "Proc. ACM Conf. on LISP and Functional Programming
(LFP), Snowbird, Utah",
ENTRYDATE = "4:31pm 4/4/1988",
KEY = "Fritz Henglein",
MONTH = "July",
PUBLISHER = "ACM Press",
PAGES = "184-197",
TITLE = "Type Inference and Semi-Unification",
YEAR = "1988"}
@phdthesis{he89a,
AUTHOR = "Henglein, Fritz",
ENTRYDATE = "3:15pm 12/16/1988",
KEY = "F.",
MONTH = "April",
SCHOOL = "Rutgers University",
TITLE = "Polymorphic Type Inference and Semi-Unification",
YEAR = "1989",
NOTE = "Available as NYU Technical Report 443, May 1989, from New
York University, Courant Institute of Mathematical
Sciences, Department of Computer Science, 251 Mercer
St., New York, N.Y.\ 10012, USA."}
@inproceedings{ktu89,
AUTHOR = "Kfoury, A. and Tiuryn, J. and Urzyczyn, P.",
BOOKTITLE = "Proc. 4th IEEE Symposium on Logic in Computer Science (LICS)",
ENTRYDATE = "4:18pm 3/5/1989",
KEY = "A.",
MONTH = "June",
TITLE = "Computational Consequences and Partial Solutions of a Generalized Unification Problem",
YEAR = "1989"}
@InProceedings{ktu90b,
author = "Kfoury, A. and Tiuryn, J. and Urzyczyn, P.",
title = "The Undecidability of the Semi-Unification Problem",
booktitle = "Proc. 22nd Annual ACM Symp. on Theory of Computation
(STOC), Baltimore, Maryland",
year = "1990",
pages = "468-476",
month = "May"
}
@article{ktu93,
author = "A. J. Kfoury and Jerzy Tiuryn and Pawel Urzyczyn",
title = "The Undecidability of the Semi-unification Problem",
journal = "Information and Computation",
volume = "102",
number = "1",
pages = "83-101",
year = "1993" }
@Article{henglein93c,
author = "Henglein, Fritz",
title = "Type Inference with Polymorphic Recursion",
journal = "ACM Transactions on Programming Languages and
Systems (TOPLAS)",
year = "1993",
volume = "15",
number = "2",
pages = "253-289",
month = "April",
annote = "Also DIKU Semantics Report D-127"
}
@article{KTU93b,
author = "A. J. Kfoury , J. Tiuryn , P. Urzyczyn",
title = "Type reconstruction in the presence of polymorphic recursion",
journal = "ACM Transactions on Programming Languages and Systems (TOPLAS)",
volume = "15",
number = "2",
year = "1993",
month = "April "}
@InProceedings{rittri95,
author = "Rittri, Mikael",
title = "Dimension Inference under Polymorphic Recursion",
pages = "147-159",
booktitle = "Proc. ACM Conf.\ on Functional Programming Languages
and Computer Architecture (FPCA), La Jolla, California",
year = "1995",
publisher = "ACM Press",
month = "June"
}
------------------------------------------------------------------------
Fritz Henglein, Ph.D., Assoc. Prof. Email: henglein@it.edu
The IT University of Copenhagen Tel.: +45-38 16 88 88 (ITU)
Glentevej 67 Tel.: +45-38 16 88 21 (office)
DK-2400 Copenhagen Fax: +45-38 16 88 99 (ITU)
Denmark URL: http://www.it.edu
------------------------------------------------------------------------