We investigate Girard's calculus Fm as a 'Curry style' type assignment system for pure lambda terms. First we show an example of a strongly normalizable term that is untypable in FM. Then we prove that every partial recursive function is nonuniformly represented in Fra (even if quantification is restricted to constructor variables of level 1). It follows that the type reconstruction problem is undecidable and cannot be recursively separated from normalization.
展开▼
