Ãø¼Ô
Frank Pfenning
¥¿¥¤¥È¥ë
On the Undecidability of Partial Polymorphic Type Reconstruction
Æü»þ
January 1992
³µÍ×
We prove that partial type reconstruction for the pure polymorphic ¦Ë-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 ¦Ë-calculus, which implies undecidability of partial type reconstruction for ¦ËML as introduced by Harper, Mitchell, and Moggi. ¦Ë ^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J
¥«¥Æ¥´¥ê
CMUTR
Category: CMUTR
Institution: Department of Computer Science, Carnegie
        Mellon University
Abstract: We prove that partial type reconstruction for the pure
        polymorphic ¦Ë-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 ¦Ë-calculus, which implies undecidability 
        of partial type reconstruction for ¦ËML as introduced 
        by Harper, Mitchell, and Moggi.
        ¦Ë 
        ^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J^[$@&K^[(J
Number: CMU-CS-92-105
Bibtype: TechReport
Month: jan
Author: Frank Pfenning
Title: On the Undecidability of Partial Polymorphic Type Reconstruction
Year: 1992
Address: Pittsburgh, PA
Super: @CMUTR