The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus (Q1314360): Difference between revisions

The starting point of the paper is the observation (due to J.-Y. Girard) that no term of System F (also called polymorphic, or second-order \(\lambda\)-calculus) can discriminate over types. Indeed, in all the intended models, terms are understood as essentially constant functions on input types. It follows that it is consistent to add to \(F\) the following axiom (C): If \(M:\;\forall X\sigma\) and \(X\not\in FV(\sigma)\), then \(M\tau= M\tau'\) for any pair of types \(\tau\), \(\tau'\). The paper studies the system Fc=F+C and proves that, in Fc, any type acts as a generic input (that is, as a variable). Formally, it is proved that, for any two terms \(M,M':\;\forall X\sigma\) (no restriction on \(\sigma\)), if \(M\tau=N\tau\) for all type \(\tau\), then \(M=N\) (genericity theorem). The proof is syntactic and difficult. Since in Fc two terms can be equal without their subterms being equal, the paper introduces the crucial notion of generalizer of two Fc-equal terms: roughly put, a term can be instantiated to the two terms by type substitutions and then proved equal to them via axiom C. The paper ends with a discussion on models, showing that both PER, dl-based, and ``dinatural'' models satisfy axiom C.