| Summary: | We investigate completeness and parametricity for a general class of
realizability semantics for System F defined in terms of closure operators over
sets of $\lambda$-terms. This class includes most semantics used for
normalization theorems, as those arising from Tait's saturated sets and
Girard's reducibility candidates.
We establish a completeness result for positive types which subsumes those
existing in the literature, and we show that closed realizers satisfy
parametricity conditions expressed either as invariance with respect to logical
relations or as dinaturality. Our results imply that, for positive types,
typability, realizability and parametricity are equivalent properties of closed
normal $\lambda$-terms.
|
|---|