[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----] 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 ------------------------------------------------------------------------