Relational parametricity for pure System F

TheoremFundamental theorem of relational parametricity for System F#✓fully proved

The fundamental binary relational-parametricity theorem of pure System F.

A syntactic-model adaptation of Reynolds' abstraction theorem (1983, Sections 3 and 8), following Wadler's related-environment formulation (1989, Section 6); see the module's provenance and model qualifications.

theorem fundamental {n m : Nat} {Γ : Ctx n m} {t : Tm n m} {A : Ty n}
    (ht : Typing Γ t A) (ρ : Fin n → Rel) (σ τ : Fin m → Model)
    (hστ : ∀ i, ((Γ i).interpret ρ).holds (σ i) (τ i)) :
    (A.interpret ρ).holds (Tm.close σ t) (Tm.close τ t)
Uses 15 · Used by 1
Statement usesTerm variable contexts of System F · Untyped locally closed term model · Beta-invariant binary relations on the term model · Scoped terms of pure System F · Closing System F terms in the term model · Scoped types of pure System F · Binary logical relation of a System F type · Extrinsic typing of pure System F terms
Proof usesBeta equivalence in the untyped term model · Application in the untyped term model · Beta conversion of a closed System F lambda application · Instantiating the newest type binder of a type · Relational interpretation of an instantiated System F type · Relational interpretation of a weakened System F type · Type-variable renaming in System F types
Used byClosed typed System F terms are related to themselves

TheoremClosed typed System F terms are related to themselves#✓fully proved

Every closed typed term is related to itself under arbitrary relations.

theorem fundamental_closed {n : Nat} {Γ : Ctx n 0} {t : Tm n 0} {A : Ty n}
    (ht : Typing Γ t A) (ρ : Fin n → Rel) :
    (A.interpret ρ).holds (Tm.eraseModel t) (Tm.eraseModel t)
Uses 9 · Used by 3
Statement usesTerm variable contexts of System F · Untyped locally closed term model · Beta-invariant binary relations on the term model · Scoped terms of pure System F · Erasure of closed System F terms to the term model · Scoped types of pure System F · Binary logical relation of a System F type · Extrinsic typing of pure System F terms
Proof usesFundamental theorem of relational parametricity for System F
Used byNo closed System F term inhabits \(\forall X, X\) · Closed inhabitants of the polymorphic identity type are identities · Polymorphic identity inhabitants preserve admissible relations

DefinitionPolymorphic identity type#✓fully proved

The polymorphic identity type, universally quantified at any type depth.

def polyIdType {n : Nat} : Ty n := .all (.arr (.var 0) (.var 0))
Uses 1 · Used by 3
Statement usesScoped types of pure System F
Used byTyping of the polymorphic identity · Closed inhabitants of the polymorphic identity type are identities · Polymorphic identity inhabitants preserve admissible relations

DefinitionPolymorphic identity term#✓fully proved

The pure polymorphic identity term.

def polyId {n m : Nat} : Tm n m := .tabs (.lam (.var 0) (.var 0))
Uses 2 · Used by 1
Statement usesScoped terms of pure System F · Scoped types of pure System F
Used byTyping of the polymorphic identity

TheoremTyping of the polymorphic identity#✓fully proved

The polymorphic identity is well typed in any existing term context.

theorem polyId_typed {n m : Nat} (Γ : Ctx n m) :
    Typing Γ polyId polyIdType
Uses 7
Statement usesTerm variable contexts of System F · Extrinsic typing of pure System F terms · Polymorphic identity term · Polymorphic identity type
Proof usesScoped terms of pure System F · Scoped types of pure System F · Type-variable renaming in System F types

TheoremClosed inhabitants of the polymorphic identity type are identities#✓fully proved

Every closed inhabitant acts as identity after every type instantiation.

The conclusion is full-beta conversion in the existing erased term model, for an arbitrary locally closed input. It makes no CBV termination claim. This consumer specializes the free-theorem method of Wadler (1989, Figure 1) to the declared syntactic model; it applies to every typed inhabitant.

theorem polymorphic_identity {t : Tm 0 0}
    (ht : Typing Fin.elim0 t polyIdType) (A : Ty 0) (x : Model) :
    BetaEq (Model.app (Tm.eraseModel (.tapp t A)) x) x
Uses 13
Statement usesBeta equivalence in the untyped term model · Untyped locally closed term model · Application in the untyped term model · Scoped terms of pure System F · Erasure of closed System F terms to the term model · Scoped types of pure System F · Extrinsic typing of pure System F terms · Polymorphic identity type
Proof usesReflexivity of beta equivalence · Beta-invariant binary relations on the term model · Relation of two terms beta-equal to a fixed term · Binary logical relation of a System F type · Closed typed System F terms are related to themselves

Type instantiations preserve every admissible binary input relation.

theorem polymorphic_related {t : Tm 0 0}
    (ht : Typing Fin.elim0 t polyIdType) (A B : Ty 0) (R : Rel)
    {x y : Model} (hxy : R.holds x y) :
    R.holds (Model.app (Tm.eraseModel (.tapp t A)) x)
      (Model.app (Tm.eraseModel (.tapp t B)) y)
Uses 9
Statement usesUntyped locally closed term model · Application in the untyped term model · Beta-invariant binary relations on the term model · Scoped terms of pure System F · Erasure of closed System F terms to the term model · Scoped types of pure System F · Extrinsic typing of pure System F terms · Polymorphic identity type
Proof usesClosed typed System F terms are related to themselves

TheoremNo closed System F term inhabits \(\forall X, X\)#✓fully proved

The empty relation rules out every closed inhabitant of forall X, X.

theorem forall_var_uninhabited (t : Tm 0 0) :
    ¬ Typing Fin.elim0 t (.all (.var 0))
Uses 6
Statement usesScoped terms of pure System F · Scoped types of pure System F · Extrinsic typing of pure System F terms
Proof usesBeta-invariant binary relations on the term model · Empty beta-invariant relation · Closed typed System F terms are related to themselves
8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.