Parametricity and variants of Girard's J operator

The Girard-Reynolds polymorphic lambda-calculus is generally regarded as a calculus of parametric polymorphism in which all well-formed terms are stro ngly normalizing with respect to beta-reductions. Girard demonstrated that the addition of a simple "non-parametric" operation, J, to the calculus all ows the definition of a non-normalizing term. Since the type of J is not in habited by any closed term, one might suspect that this may play a role in defining a non-normalizing term using it. We demonstrate that this is not t he case by giving a simple variant, J', of J whose type is otherwise inhabi ted and which causes normalization to fail. It appears that impredictivity is essential to the argument, predictive variants of the polymorphic lambda -calculus admit non-parametric operations without sacrificing normalization . (C) 1999 Elsevier Science B.V. All rights reserved.