Subtyping Algebraconcept:subtyping-algebra

raw-formationclaim:raw-formation

Raw formation checking agrees with distinct record names, admitted map keys, a deferred's admitted error column, and no type variable outside a template; a declared service carrier is a strict formation site (decisions rows 288, 297)

The raw-formation claim, used by every checked boundary's certificate.

Module

Effect4.Program.Formation

∀ {Op : Type} [inst : Effect4.Program.ScopedOp Op] (program : Effect4.Program.Eff Op)
  (table : List Effect4.Program.Row)
  (services : optParam (List (Prod Effect4.ServiceKey Effect4.Program.Ty)) List.nil),
  Iff (Eq (Effect4.Program.Formation.checkInput program table services) Option.none)
    (Effect4.Program.Formation.InputFormed program table services)

subn-reflclaim:subn-refl

Reflexivity of normalized subtyping

Module

Effect4.Laws.Program.TypeAlgebra

Literature

TAPL, §15.2, p. 182 (definitionUsed)

∀ (a : Effect4.Program.Ty), Eq (a.subN a) Bool.true

subn-transclaim:subn-trans

Transitivity of normalized subtyping

Module

Effect4.Laws.Program.TypeAlgebra

Literature

TAPL, §15.2, p. 182 (proofTechnique)

∀ {a b c : Effect4.Program.Ty},
  Eq (a.subN b) Bool.true → Eq (b.subN c) Bool.true → Eq (a.subN c) Bool.true

subn-equiv-iffclaim:subn-equiv-iff

Kernel of subN is syntactic normal form equality

The kernel of the checker's order is equality of normal forms.

Module

Effect4.Laws.Program.TypeAlgebra

Literature

TAPL, §16.3, p. 218 (adaptedResult)

∀ (a b : Effect4.Program.Ty),
  Iff (And (Eq (a.subN b) Bool.true) (Eq (b.subN a) Bool.true)) (Eq a.normalize b.normalize)

normalize-idemclaim:normalize-idem

Normalization idempotence

Construction is total; no checked partial constructor is needed.

Module

Effect4.Program.Ty

∀ (t : Effect4.Program.Ty), Eq t.normalize.normalize t.normalize

sub-antisymm-canonicalclaim:sub-antisymm-canonical

Antisymmetry of subtyping on canonical representatives CTy

Module

Effect4.Laws.Program.TypeAlgebra

Literature

Castagna2024, audit P6 (adaptedResult)

∀ (a b : Effect4.Program.CTy),
  Eq (a.toRaw.sub b.toRaw) Bool.true → Eq (b.toRaw.sub a.toRaw) Bool.true → Eq a b

template-match-completeclaim:template-match-complete

The match of a template by bounds is complete: on a template that is its own normal form, is admissible and holds no nominal reference, a normal request below some instance has a match, from any seed that the instance agrees with; no premise asks where a parameter first occurs or where never stands; the match is sound by its guard (matchB_sound), its bindings are the least (matchB_least), an argument list is checked at one final list of bindings (matchArgsB_sound), and smaller arguments have a match with smaller bindings (matchArgsB_monotone); every template of the tree is in reach, as a finite check; the row check and a binder term read the match by bounds with no guard (slice UNGUARD); it does not match under a union head or a nominal reference, and it establishes nothing of tsgo's inference (decisions rows 299, 303)

The match by bounds is complete: a normal request below some instance of the template has a match. The template is normal, admissible and holds no nominal reference. No premise asks where a parameter first occurs, and none asks where never stands: Ty.anchored and Ty.bottomFree (src/Effect4/Laws/Program/Template.lean) are not premises.

Module

Effect4.Laws.Program.Bounds

∀ (seed : Effect4.Program.Bounds.Subst) {t r : Effect4.Program.Ty},
  Effect4.Program.Bounds.TemplateOK t →
    r.Normal →
      ∀ {τ : Effect4.Program.Bounds.Subst},
        (∀ (j : Nat) (u : Effect4.Program.Ty),
            Eq (List.lookup j seed) (Option.some u) →
              Eq (Effect4.Program.Ty.instantiate τ (Effect4.Program.Ty.var j)).normalize
                u.normalize) →
          Eq (r.sub (Effect4.Program.Ty.instantiate τ t).normalize) Bool.true →
            Exists fun σ => Eq (Effect4.Program.Bounds.matchB seed t r) (Option.some σ)

slice-lattice-minimalclaim:slice-lattice-minimal

For a monotone map from the type slices of one program to a preorder of types: a minimal valid slice exists below each valid slice, the one-pass descent ends at one below its start, a refined query has a minimal slice below a minimal slice of the wider query, and the join of two valid slices is valid for the join of their queries; no statement names Eff, Ty or the checker (decisions rows 282, 286)

The claim slice-lattice-minimal, as one statement: its four parts, for one monotone view. A minimal valid type slice exists below each valid slice (Theorem 4.5). The descent ends at one, below its start. A refined query has a minimal slice below a minimal slice of the wider query (Theorem 4.6). The join of two valid slices is valid for the join of their queries (Theorem 4.7). It is the pointer that the claim's row needs, and it adds nothing to its four parts.

Module

Effect4.Laws.Slice.Lattice

∀ {α : Type u} {T : Type v} [inst : LE T] [DecidableEq α] [Std.IsPreorder T]
  [inst_3 : DecidableLE T] [inst_4 : Max T] [Std.LawfulOrderSup T] (v : Effect4.SliceView α T),
  And
    (∀ {q : T} {s : Effect4.Slice α},
      v.Valid q s → Exists fun m => And (Effect4.Slice.instLE.le m s) (v.Minimal q m))
    (And
      (∀ {q : T} {s : Effect4.Slice α},
        v.Valid q s → And (Effect4.Slice.instLE.le (v.descend q s) s) (v.Minimal q (v.descend q s)))
      (And
        (∀ {q₁ q₂ : T} {m₂ : Effect4.Slice α},
          inst.le q₁ q₂ →
            v.Minimal q₂ m₂ →
              Exists fun m₁ => And (Effect4.Slice.instLE.le m₁ m₂) (v.Minimal q₁ m₁))
        (∀ {q₁ q₂ : T} {a b : Effect4.Slice α},
          v.Valid q₁ a →
            v.Valid q₂ b → v.Valid (inst_4.max q₁ q₂) (Effect4.Slice.instMax.max a b))))

union-rule-liftclaim:union-rule-lift

A member rule lifted to every type by reading the union members of the normal form and joining the answers: it answers the least answer at never; at one normal union member it is the member rule, up to the join with the least answer; two types with one normal form have one answer; a member rule that is monotone in the order lifts to a monotone rule; a property of a value and an answer that the join keeps on each side passes from the union members to the lifted rule; the join law is an equation at a type, at a pair of types and at a carrier whose order is antisymmetric (lift_union_eq, lift_union_eq_pair, lift_union_eq_of_antisymm), and a map with the four properties of the lifted rule is the lifted rule, at a type and at a pair of types (lift_unique, lift_unique_pair); its order is read in Lean core's classes: a carrier with those classes is a carrier of answers (AnswerOrder.ofCore), and the checker's order on raw types is the order of canonical types by definition (subN_iff_le); the two record rules are its instances, and the fiber rule is the first converted rule (union-rule-extend) (decisions rows 282, 285, 293, 298, 300)

The claim union-rule-lift, as one statement: its five parts of the brief, for one member rule. The lifted rule answers the least answer at never. At a normal type that is one union member it is the member rule, up to the join with the least answer. Two types with one normal form have one answer. A member rule that is monotone in the order lifts to a monotone rule. A property of a value and an answer that the join keeps on each side passes from the union members to the lifted rule. It is the pointer that the claim's row needs, and it adds nothing to its parts. lift_all, lift_upper and lift_least stand beside it.

Module

Effect4.Laws.Program.UnionRule

∀ {α : Type} [inst : Effect4.Program.UnionRule.Answer α]
  [inst_1 : Effect4.Program.UnionRule.AnswerOrder α] (rule : Effect4.Program.Ty → Option α),
  And (Eq (Effect4.Program.UnionRule.lift rule Effect4.Program.Ty.never) (Option.some inst.bot))
    (And
      (∀ {t : Effect4.Program.Ty},
        t.Normal →
          Eq t.isMember Bool.true →
            Eq (Effect4.Program.UnionRule.lift rule t) (Option.map (inst.join inst.bot) (rule t)))
      (And
        (∀ {s t : Effect4.Program.Ty},
          Eq s.normalize t.normalize →
            Eq (Effect4.Program.UnionRule.lift rule s) (Effect4.Program.UnionRule.lift rule t))
        (And
          (Effect4.Program.UnionRule.Below rule rule →
            ∀ {s t : Effect4.Program.Ty} {b : α},
              Eq (s.subN t) Bool.true →
                Eq (Effect4.Program.UnionRule.lift rule t) (Option.some b) →
                  Exists fun a =>
                    And (Eq (Effect4.Program.UnionRule.lift rule s) (Option.some a))
                      (inst_1.le a b))
          (∀ {V : Type} {In : V → Effect4.Program.Ty → Prop} {P : V → α → Prop},
            (∀ {v : V} {t : Effect4.Program.Ty}, In v t → In v t.normalize) →
              (∀ {v : V} {t : Effect4.Program.Ty},
                  In v t → Exists fun m => And (List.instMembership.mem t.members m) (In v m)) →
                (∀ {v : V} (a b : α), P v a → P v (inst.join a b)) →
                  (∀ {v : V} (a b : α), P v b → P v (inst.join a b)) →
                    (∀ {m : Effect4.Program.Ty} {a : α} {v : V},
                        m.Normal →
                          Eq m.isMember Bool.true → Eq (rule m) (Option.some a) → In v m → P v a) →
                      ∀ {t : Effect4.Program.Ty} {a : α} {v : V},
                        Eq (Effect4.Program.UnionRule.lift rule t) (Option.some a) →
                          In v t → P v a))))

union-rule-extendclaim:union-rule-extend

A converted eliminator of the checker is the full fallback of its member rule: the member rule's own answer where the member rule answers at the raw target, and the lifted rule over every normalized union member elsewhere; for every UnionRule.Eliminator it agrees with the member rule, it is the lifted rule where the member rule refuses, and it keeps every answer of the earlier guarded rule (Eliminator.extendAll_laws); it answers a least answer at never; its answer a puts the target below C a in Ty.subN, and an answer b is above a exactly when the target is below C b; a retained member that the member rule refuses refuses the whole target; it is monotone at every smaller type (Eliminator.extendAll_mono), and its answer equals the lifted rule's up to the order (Eliminator.extendAll_lift); the fiber, list and exit rules are instances (fiberTy, Checker.listOf?, Checker.exitOf?); the cause rule reads two heads, so it is the full fallback of Member.cause with four member facts of an upper type (causeInputError_upper); the option rule reads the normal form alone, so it is the lifted rule of Member.option, and it is the earlier normalized-head rule where the normal form has at most one member and is not never (optionTy_eq_normal; decisions row 304); the guarded rule's laws stay for their earlier consumers (Eliminator.extend_laws); it does not establish checker-monotone or anything that tsgo accepts (decisions rows 292 to 294, 296, 298 and 304; slice P2b)

The full-fallback contract, without a proper-union refusal. Consumer: the fiber classifier reader.

Module

Effect4.Laws.Program.UnionRule

∀ {α : Type} [inst : Effect4.Program.UnionRule.Answer α]
  [inst_1 : Effect4.Program.UnionRule.AnswerOrder α] {rule : Effect4.Program.Ty → Option α}
  {C : α → Effect4.Program.Ty},
  Effect4.Program.UnionRule.Eliminator rule C →
    And
      (∀ {t : Effect4.Program.Ty} {a : α},
        Eq (rule t) (Option.some a) →
          Eq (Effect4.Program.UnionRule.extendAll rule t) (Option.some a))
      (And
        (∀ {t : Effect4.Program.Ty},
          Eq (rule t) Option.none →
            Eq (Effect4.Program.UnionRule.extendAll rule t) (Effect4.Program.UnionRule.lift rule t))
        (And
          (Exists fun a =>
            And
              (Eq (Effect4.Program.UnionRule.extendAll rule Effect4.Program.Ty.never)
                (Option.some a))
              (∀ (b : α), inst_1.le a b))
          (And
            (∀ {t : Effect4.Program.Ty} {a : α},
              Eq (Effect4.Program.UnionRule.extendAll rule t) (Option.some a) →
                And (Eq (t.subN (C a)) Bool.true)
                  (∀ (b : α), Iff (inst_1.le a b) (Eq (t.subN (C b)) Bool.true)))
            (∀ {t : Effect4.Program.Ty} {a : α},
              Eq (Effect4.Program.UnionRule.extend rule t) (Option.some a) →
                Eq (Effect4.Program.UnionRule.extendAll rule t) (Option.some a)))))

variance-semiringclaim:variance-semiring

The variance semiring: Var4, the four parity sets of the signed paths that reach an occurrence (bi, co, contra, inv), with join and composition, is a commutative idempotent semiring with bi as zero and co as one, ordered by inclusion with join as least upper bound; on the declared alphabet's image the walk's composition (Bounds.comp) is its product and the reference's Boolean reading (Ty.Variance.select) is its select (Bounds.comp_toVar4, Ty.Variance.select_toVar4); the polarity of a template's parameter is one fold of the generated TyAlgebra at a reading of the heads (Ty.polarity, HeadReading.sub); it establishes no subtyping fact of Ty (the OpenAI math review, slice VAR-1)

The variance semiring (claim variance-semiring): join and composition form a commutative idempotent semiring with bi as zero and co as one, composition distributes over join, and the order is a preorder whose join is +. A step of instantiate-respects-polarity (slice VAR-2) and of the row census (slice VAR-3).

Module

Effect4.Laws.Program.Polarity

And (∀ (a b : Effect4.Program.Var4), Eq (instHAdd.hAdd a b) (instHAdd.hAdd b a))
  (And
    (∀ (a b c : Effect4.Program.Var4),
      Eq (instHAdd.hAdd (instHAdd.hAdd a b) c) (instHAdd.hAdd a (instHAdd.hAdd b c)))
    (And (∀ (a : Effect4.Program.Var4), Eq (instHAdd.hAdd a a) a)
      (And (∀ (a : Effect4.Program.Var4), Eq (instHAdd.hAdd Effect4.Program.Var4.bi a) a)
        (And (∀ (a b : Effect4.Program.Var4), Eq (instHMul.hMul a b) (instHMul.hMul b a))
          (And
            (∀ (a b c : Effect4.Program.Var4),
              Eq (instHMul.hMul (instHMul.hMul a b) c) (instHMul.hMul a (instHMul.hMul b c)))
            (And (∀ (a : Effect4.Program.Var4), Eq (instHMul.hMul Effect4.Program.Var4.co a) a)
              (And
                (∀ (a : Effect4.Program.Var4),
                  Eq (instHMul.hMul Effect4.Program.Var4.bi a) Effect4.Program.Var4.bi)
                (And
                  (∀ (a b c : Effect4.Program.Var4),
                    Eq (instHMul.hMul a (instHAdd.hAdd b c))
                      (instHAdd.hAdd (instHMul.hMul a b) (instHMul.hMul a c)))
                  (And (∀ (a : Effect4.Program.Var4), Eq (a.le a) Bool.true)
                    (∀ (a b c : Effect4.Program.Var4),
                      Eq ((instHAdd.hAdd a b).le c) ((a.le c).and (b.le c))))))))))))

instantiate-respects-polarityclaim:instantiate-respects-polarity

Instantiation respects polarity: if every parameter's two bindings are related by raw Ty.sub at the parameter's polarity in a template (a bivariant parameter asks nothing, an invariant one both directions), the two instances are related; with matchArgsB_monotone it gives a smaller answer at a smaller request where the answer reads its parameters at co or bi; no semantic variance, nothing of tsgo's inference (slice VAR-2)

Instantiation respects polarity (claim instantiate-respects-polarity, slice VAR-2): if every parameter's two bindings are related by Ty.sub at the parameter's polarity in t (a bivariant parameter asks nothing, an invariant one both directions), the two instances are related. It is the probe's eval_respects at the model of Ty (raw Ty.sub, each head read at its variance, HeadReading.sub). Its consumers are checker-monotone's share at a row (with Bounds.matchArgsB_monotone, at an answer that reads its parameters at co or bi) and HO-4's instantiated rows. It establishes no semantic variance and nothing of tsgo's inference.

Module

Effect4.Laws.Program.Polarity

∀ (t : Effect4.Program.Ty) (σ σ' : Effect4.Program.Ty.Subst),
  (∀ (i : Nat),
      Eq
        ((Effect4.Program.Ty.polarity Effect4.Program.HeadReading.sub i t).select
          ((σ.at i).sub (σ'.at i)) ((σ'.at i).sub (σ.at i)))
        Bool.true) →
    Eq ((Effect4.Program.Ty.instantiate σ t).sub (Effect4.Program.Ty.instantiate σ' t)) Bool.true

checked-types-closedclaim:checked-types-closed

A formed program that the checker admits has closed types: at a closed environment, a typing signature with closed atoms and closed service carriers, and annotations formed outside a template; no premise on a row or on a layer reference; the whole-program checker has the same property, and an admitted program has closed types with no premise (typeOfProgram_closed, AdmittedProgram.closed); the checker alone does not have it (decisions rows 288 point 6 a, 297)

A formed program that the checker admits has closed types, at a closed environment and a signature with closed atoms and closed service carriers (the claim checked-types-closed). The annotations are formed outside a template, so each states a closed type (Formation.closed_of_formed), and each rule of the checker keeps closed types closed (hasTy_closed). The path is any path: the checker's answer does not depend on it.

Module

Effect4.Laws.Program.Typing.Closed

∀ {Op : Type} [inst : Effect4.Program.ScopedOp Op] (sig : Effect4.Program.Signature Op),
  Effect4.Program.ClosedSig sig →
    ∀ {env : Effect4.Program.TyEnv},
      (∀ (t : Effect4.Program.Ty), List.instMembership.mem env t → Eq t.closed Bool.true) →
        ∀ {p : List Nat} {e : Effect4.Program.Eff Op} {t : Effect4.Program.EffTy},
          Effect4.Program.Formation.Formed (Effect4.Program.Formation.programSites e) →
            Eq (Effect4.Program.Checker.check sig env p e) (Except.ok t) →
              And (Eq t.answer.closed Bool.true) (Eq t.error.closed Bool.true)