Higher-kinded relational parametricity of pure Fω

TheoremFundamental theorem of higher-kinded parametricity for Fω#✓fully proved

The full binary higher-kinded fundamental theorem of pure Fω.

theorem fundamental {Δ : List Kind} {m : Nat} {Γ : Ctx Δ m}
    {t : Tm Δ m} {A : Ty Δ .star} (ht : Typing Γ t A)
    (ρ : KEnv SystemF.Rel Δ) (σ τ : Fin m → SystemF.Model)
    (hστ : ∀ i, ((Γ i).interpret ρ).holds (σ i) (τ i)) :
    (A.interpret ρ).holds (Tm.close σ t) (Tm.close τ t)

Uses 24 · Used by 1

Statement usesTerm contexts of pure Fω · Kinded semantic environment · Kinds of pure Fω · Scoped pure Fω terms · Closing Fω terms in the System F term model · Intrinsically kinded Fω type operators · Relational interpretation of Fω types · Typing rules of pure Fω · Untyped locally closed term model · Beta-invariant binary relations on the term model

Proof usesExtension of a kinded semantic environment · Kinded type variables of Fω · Semantic interpretation of kinds · Beta conversion of a closed Fω lambda application · Type-beta conversion in Fω · Type-beta conversion preserves the relational interpretation · Semantic evaluation of kinded type operators · Instantiation of an Fω type binder · Relational interpretation of an instantiated Fω type · Relational interpretation of a weakened Fω type · Renaming of Fω type operators · Kind algebra of beta-invariant relations · Beta equivalence in the untyped term model · Application in the untyped term model

Used byClosed typed Fω terms are related to themselves

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

Every closed-term typed expression is related to itself at every kind environment.

theorem fundamental_closed {Δ : List Kind} {Γ : Ctx Δ 0}
    {t : Tm Δ 0} {A : Ty Δ .star} (ht : Typing Γ t A)
    (ρ : KEnv SystemF.Rel Δ) :
    (A.interpret ρ).holds (Tm.eraseModel t) (Tm.eraseModel t)

Uses 11 · Used by 4

Statement usesTerm contexts of pure Fω · Kinded semantic environment · Kinds of pure Fω · Scoped pure Fω terms · Erasure of closed Fω terms to the term model · Intrinsically kinded Fω type operators · Relational interpretation of Fω types · Typing rules of pure Fω · Untyped locally closed term model · Beta-invariant binary relations on the term model

Proof usesFundamental theorem of higher-kinded parametricity for Fω

Used byNo closed Fω term inhabits \(\forall X, X\) · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations · No closed Fω term inhabits \(\forall F, \forall X, F\,X\)

DefinitionHigher-kinded identity type#✓fully proved

A genuine higher-kind identity type: ∀ F : * → *, ∀ X : *, F X → F X.

def higherIdType {Δ : List Kind} : Ty Δ .star :=
  .all (κ := .arrow .star .star) (.all (κ := .star)
    (.arr (.app (.var (.succ .zero)) (.var .zero))
      (.app (.var (.succ .zero)) (.var .zero))))

Uses 3 · Used by 3

Statement usesKinded type variables of Fω · Kinds of pure Fω · Intrinsically kinded Fω type operators

Used byTyping of the higher-kinded identity · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations

DefinitionHigher-kinded polymorphic identity term#✓fully proved

The pure higher-kinded polymorphic identity term.

def higherId {Δ : List Kind} {m : Nat} : Tm Δ m :=
  .tabs (κ := .arrow .star .star) (.tabs (κ := .star)
    (.lam (.app (.var (.succ .zero)) (.var .zero)) (.var 0)))

Uses 4 · Used by 1

Statement usesKinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators

Used byTyping of the higher-kinded identity

TheoremTyping of the higher-kinded identity#✓fully proved

The higher-kinded identity is typed in every existing term context.

theorem higherId_typed {Δ : List Kind} {m : Nat} (Γ : Ctx Δ m) :
    Typing Γ higherId higherIdType

Uses 9

Statement usesTerm contexts of pure Fω · Kinds of pure Fω · Typing rules of pure Fω · Higher-kinded polymorphic identity term · Higher-kinded identity type

Proof usesKinded type variables of Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Renaming of Fω type operators

TheoremClosed inhabitants of the higher-kinded identity type are identities#✓fully proved

Every closed-term inhabitant is beta-identity at every kind-correct instantiation.

The inhabitant is arbitrary, not the manually defined higherId. The input is any locally closed model term; no CBV termination or normalization is claimed.

theorem higher_kinded_identity {Δ : List Kind} {t : Tm Δ 0}
    (ht : Typing Fin.elim0 t higherIdType)
    (F : Ty Δ (.arrow .star .star)) (A : Ty Δ .star) (x : SystemF.Model) :
    SystemF.BetaEq
      (SystemF.Model.app (Tm.eraseModel (.tapp (.tapp t F) A)) x) x

Uses 21

Statement usesKinds of pure Fω · Scoped pure Fω terms · Erasure of closed Fω terms to the term model · Intrinsically kinded Fω type operators · Typing rules of pure Fω · Higher-kinded identity type · Beta equivalence in the untyped term model · Untyped locally closed term model · Application in the untyped term model

Proof usesKinded semantic environment · Extension of a kinded semantic environment · Kinded type variables of Fω · Semantic interpretation of kinds · Semantic evaluation of kinded type operators · Relational interpretation of Fω types · Closed typed Fω terms are related to themselves · Kind algebra of beta-invariant relations · Reflexivity of beta equivalence · Beta-invariant binary relations on the term model · Relation of two terms beta-equal to a fixed term · Total beta-invariant relation

TheoremHigher-kinded identity inhabitants preserve admissible relations#✓fully proved

Different higher-kind type instantiations preserve every admissible binary relation.

theorem higher_kinded_related {Δ : List Kind} {t : Tm Δ 0}
    (ht : Typing Fin.elim0 t higherIdType)
    (F G : Ty Δ (.arrow .star .star)) (A B : Ty Δ .star)
    (Φ : SystemF.Rel → SystemF.Rel) (R : SystemF.Rel)
    {x y : SystemF.Model} (hxy : (Φ R).holds x y) :
    (Φ R).holds
      (SystemF.Model.app (Tm.eraseModel (.tapp (.tapp t F) A)) x)
      (SystemF.Model.app (Tm.eraseModel (.tapp (.tapp t G) B)) y)

Uses 14

Statement usesKinds of pure Fω · Scoped pure Fω terms · Erasure of closed Fω terms to the term model · Intrinsically kinded Fω type operators · Typing rules of pure Fω · Higher-kinded identity type · Untyped locally closed term model · Application in the untyped term model · Beta-invariant binary relations on the term model

Proof usesKinded semantic environment · Kinded type variables of Fω · Semantic interpretation of kinds · Closed typed Fω terms are related to themselves · Total beta-invariant relation

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

The empty relation excludes all closed-term inhabitants of ∀ X : *, X.

theorem forall_var_uninhabited {Δ : List Kind} (t : Tm Δ 0) :
    ¬ Typing Fin.elim0 t (.all (κ := .star) (.var .zero))

Uses 11

Statement usesKinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω

Proof usesKinded semantic environment · Semantic interpretation of kinds · Closed typed Fω terms are related to themselves · Beta-invariant binary relations on the term model · Empty beta-invariant relation · Total beta-invariant relation

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

A constant empty operator excludes ∀ F : * → *, ∀ X : *, F X.

theorem higher_result_uninhabited {Δ : List Kind} (t : Tm Δ 0) :
    ¬ Typing Fin.elim0 t (.all (κ := .arrow .star .star)
      (.all (κ := .star) (.app (.var (.succ .zero)) (.var .zero))))

Uses 11

Statement usesKinded type variables of Fω · Kinds of pure Fω · Scoped pure Fω terms · Intrinsically kinded Fω type operators · Typing rules of pure Fω

Proof usesKinded semantic environment · Semantic interpretation of kinds · Closed typed Fω terms are related to themselves · Beta-invariant binary relations on the term model · Empty beta-invariant relation · Total beta-invariant relation

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.