On completeness and parametricity in the realizability semantics of System F

TL;DR

This paper explores the relationships between completeness, realizability, and parametricity in System F, showing their equivalence for positive types through a general semantic framework based on closure operators.

Contribution

It introduces a broad class of realizability semantics for System F and proves a comprehensive completeness result for positive types, unifying existing results.

Findings

Completeness for positive types in realizability semantics.

Closed realizers satisfy parametricity conditions.

Typability, realizability, and parametricity are equivalent for closed normal λ-terms.

Abstract

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.