OAI/Computability/TypeSystem/Profiles.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Finite component order for the exact signed graphs of the manuscript.

  1. def OAI.PureTypeSystem.Profile line 10

    Source documentation

    Sorts assigned to the full normal form.

    def Profile {S : Type u} (P : Specification S) (Γ : List (Expr S))
    (T : Expr S) : Set S := {s | HasType P Γ T.normalForm (.sort s)}

    Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType

  2. def OAI.PureTypeSystem.AxProfile line 13
  3. def OAI.PureTypeSystem.OutProfile line 16
  4. def OAI.PureTypeSystem.FeasibleProfile line 21

    Source documentation

    Semantic feasible profiles. Normal witnesses are retained, rather than assuming the manuscript's characterization of this finite set.

    def FeasibleProfile {S : Type u} (P : Specification S) (I : Set S) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Specification

  5. structure OAI.PureTypeSystem.ProfileTriple line 24
  6. inductive OAI.PureTypeSystem.PrimaryEdge line 31

    Source documentation

    The sign is true for a domain edge and false for a positive edge.

    inductive PrimaryEdge {S : Type u} (P : Specification S) :
    Set S → Set S → Bool → Prop
  | inclusion {I J} : FeasibleProfile P I → FeasibleProfile P J →
      J ⊂ I → PrimaryEdge P I J false
  | domain {I J K} : ProfileTriple P I J K → PrimaryEdge P I K true
  | codomain {I J K} : ProfileTriple P I J K → PrimaryEdge P J K false

/-- Finite directed walks, with repeated edges permitted and parity retained. -/

    Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.FeasibleProfile, OAI.PureTypeSystem.ProfileTriple

  7. inductive OAI.PureTypeSystem.SignedPath line 39

    Source documentation

    Finite directed walks, with repeated edges permitted and parity retained.

    inductive SignedPath {V : Type*} (E : V → V → Bool → Prop) : V → V → Bool → Prop
  | nil (v) : SignedPath E v v false
  | cons {u v w p q} : E u v p → SignedPath E v w q →
      SignedPath E u w (Bool.xor p q)
  8. def OAI.PureTypeSystem.Reach line 44
  9. def OAI.PureTypeSystem.PositivePath line 47
  10. def OAI.PureTypeSystem.IsComponent line 51

    Source documentation

    A full strongly connected component, not merely a connected subset.

    def IsComponent {V : Type*} (E : V → V → Bool → Prop) (C : Set V) : Prop :=
…
  11. theorem OAI.PureTypeSystem.SignedPath.singleton line 58
  12. theorem OAI.PureTypeSystem.SignedPath.append line 61
  13. theorem OAI.PureTypeSystem.SignedPath.parity_unique line 68
  14. theorem OAI.PureTypeSystem.Reach.refl line 82
  15. theorem OAI.PureTypeSystem.Reach.trans line 84
  16. theorem OAI.PureTypeSystem.Reach.single line 89
  17. theorem OAI.PureTypeSystem.PositivePath.parity line 97
  18. theorem OAI.PureTypeSystem.PositivePath.reach line 102
  19. theorem OAI.PureTypeSystem.IsComponent.connected line 110
  20. theorem OAI.PureTypeSystem.IsComponent.between line 114
  21. def OAI.PureTypeSystem.ObservationLayers line 122

    Source documentation

    Positive closure of the sort-profile seeds.

    def ObservationLayers {S : Type u} (P : Specification S) (C : Set (Set S)) :
    Set (Set S) := {I | ∃ s, {s} ∈ C ∧ (AxProfile P s).Nonempty ∧
…

    Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.AxProfile

  22. inductive OAI.PureTypeSystem.SecondaryEdge line 126
  23. def OAI.PureTypeSystem.DirectLayer line 134
  24. def OAI.PureTypeSystem.ActiveLayer line 138
  25. def OAI.PureTypeSystem.PlainLayer line 141
  26. def OAI.PureTypeSystem.FreeLayer line 146
  27. def OAI.PureTypeSystem.ForbiddenConfiguration line 153

    Source documentation

    The finite-graph obstruction excluded by system-wide weak normalization. It is not an extra hypothesis on the normalization theorem.

    def ForbiddenConfiguration {S : Type u} (P : Specification S) (C : Set (Set S)) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Specification

  28. theorem OAI.PureTypeSystem.PlainLayer.active line 164
  29. theorem OAI.PureTypeSystem.PlainLayer.predecessor line 168
  30. theorem OAI.PureTypeSystem.FreeLayer.active line 181
  31. theorem OAI.PureTypeSystem.FreeLayer.sign_unique line 185
  32. theorem OAI.PureTypeSystem.FreeLayer.edge_sign line 194
  33. theorem OAI.PureTypeSystem.FreeLayer.direct_sign line 199
  34. theorem OAI.PureTypeSystem.Expr.normalForm_idem line 208
  35. theorem OAI.PureTypeSystem.Expr.normalForm_rename line 214
  36. theorem OAI.PureTypeSystem.HasType.lookup_sorted line 224
  37. theorem OAI.PureTypeSystem.HasType.neutral_type_sorted line 235
  38. theorem OAI.PureTypeSystem.Profile.normalForm line 255
  39. theorem OAI.PureTypeSystem.Profile.of_normal line 258
  40. theorem OAI.PureTypeSystem.Profile.sort line 262
  41. theorem OAI.PureTypeSystem.Profile.neutral line 274
  42. theorem OAI.PureTypeSystem.Profile.neutral_axiom line 286
  43. theorem OAI.PureTypeSystem.Profile.pi line 292
  44. theorem OAI.PureTypeSystem.Profile.converts line 305
  45. theorem OAI.PureTypeSystem.Profile.growth line 309
  46. theorem OAI.PureTypeSystem.Profile.feasible line 323
  47. def OAI.PureTypeSystem.Reach.component line 334
  48. theorem OAI.PureTypeSystem.Reach.mem_component line 336
  49. theorem OAI.PureTypeSystem.Reach.component_isComponent line 338
  50. theorem OAI.PureTypeSystem.Reach.component_eq line 341
  51. def OAI.PureTypeSystem.Reach.predecessors line 350
  52. def OAI.PureTypeSystem.Reach.rank line 351
  53. theorem OAI.PureTypeSystem.Reach.mem_predecessors line 353
  54. theorem OAI.PureTypeSystem.Reach.rank_mono line 356
  55. theorem OAI.PureTypeSystem.Reach.reverse_of_rank_eq line 361
  56. theorem OAI.PureTypeSystem.Reach.component_eq_of_rank_eq line 371
  57. theorem OAI.PureTypeSystem.PlainLayer.predecessor_path line 380
  58. theorem OAI.PureTypeSystem.PlainLayer.component_plain line 387
  59. def OAI.PureTypeSystem.IsComponent.signing line 397
  60. theorem OAI.PureTypeSystem.IsComponent.signing_path line 400
  61. theorem OAI.PureTypeSystem.IsComponent.signing_cross line 406