Relational parametricity for System F

The object language is exactly the pure Church-style System F signature of the preceding ledger block. No term former, type former, typing rule, or reduction rule is added. The metatheory adds relations on beta-equivalence classes of closed typed terms, relational environments for free type variables, and related closing substitutions.

Observable equality is compatible beta equality from chapter 5. Arrows are interpreted by relation lifting and universals quantify over all external relations between closed endpoint types. Unrestricted beta identity extension is false by proposition 6.15; only the Boolean and natural observation instances in proposition 6.14 are used.

The abstraction theorem is proved by induction on Church typing in theorem 6.10, with type substitution handled by lemma 6.8 and representative independence by lemma 10.6. Self-parametricity and parametric emptiness are corollary 6.11, corollary 6.13. Polymorphic application and iterator naturality are proposition 6.16, theorem 6.17. Counter representation independence is theorem 6.18.

The theorem covers a pure, strongly normalizing calculus. Fixpoints require strict admissible relations, mutable state requires world-indexed relations, and recursive types require a nonstructural construction; none is in this signature. The precise order-theoretic repair for least fixed points is proposition 10.23. The internal-logic and effectful-PE comparisons are delimited by definition 10.24, definition 10.25; neither transfers an identity-extension or effectful abstraction theorem to the pure signature.

The Kappa companion in artifacts/ch10-parametricity-calculator/ executes finite witnesses for identity, graph and arrow lifting, the two-step counter client, and the strictness failure of a singleton fixed-point relation. Finite witness enumeration proves neither the abstraction theorem nor semantic identity extension.