×

zbMATH — the first resource for mathematics

On the undecidability of partial polymorphic type reconstruction. (English) Zbl 0789.03017
Summary: We prove that partial type reconstruction for the pure polymorphic \(\lambda\)-calculus is undecidable by a reduction from the second-order unification problem, extending a previous result by H.-J. Boehm. We show further that partial type reconstruction remains undecidable even in a very small predicative fragment of the polymorphic \(\lambda\)-calculus, which implies undecidability of partial type reconstruction for \(\lambda^{ML}\) as introduced by Harper, Mitchell, and Moggi.

MSC:
03B40 Combinatory logic and lambda calculus
03D35 Undecidability and degrees of sets of sentences
PDF BibTeX XML Cite