Documentation

SE.Transformation.Effect.Orthogonality

Effect Disjointness and Overlap #

Two operators have disjoint effects when their footprints share no dimension, and overlapping effects when they share at least one.

These are effect-domain facts derived from footprints. Footprints are upper bounds, so disjointness is the strong direction: a step of one operator preserves every dimension the other may change. Overlap records only that the operators may touch a common dimension.

They do not derive the canonical OrthogonalityRelation vocabulary, which also contains conflicting and dependent. The canonical lookup remains the declared reference. The theorems comparing the two are consistency checks on the declared entries, not derivations of them.

source
def SE.Transformation.overlapB (a b : OperatorCode) :
Bool

Whether two operators share an effect dimension.

Equations
Instances For
    source
    def SE.Transformation.EffectsDisjoint (a b : OperatorCode) :
    Prop

    The footprints of two operators share no dimension.

    Equations
    Instances For
      source
      def SE.Transformation.EffectsOverlap (a b : OperatorCode) :
      Prop

      The footprints of two operators share at least one dimension.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance SE.Transformation.instDecidableEffectsDisjoint (a b : OperatorCode) :
        Decidable (EffectsDisjoint a b)
        Equations
        source
        @[instance_reducible]
        instance SE.Transformation.instDecidableEffectsOverlap (a b : OperatorCode) :
        Decidable (EffectsOverlap a b)
        Equations
        source
        theorem SE.Transformation.effectsDisjoint_iff (a b : OperatorCode) :
        EffectsDisjoint a b ↔ ∀ (d : Dimension), d ∈ footprint a → ¬d ∈ footprint b

        Effect disjointness is exactly the absence of a shared dimension.

        source
        theorem SE.Transformation.effectsOverlap_iff (a b : OperatorCode) :
        EffectsOverlap a b ↔ ∃ (d : Dimension), d ∈ footprint a ∧ d ∈ footprint b

        Effect overlap is exactly the presence of a shared dimension.

        source
        theorem SE.Transformation.StateModel.step_preserves_of_effectsDisjoint {M : StateModel} {a b : OperatorCode} (hab : EffectsDisjoint a b) {d : Dimension} (hd : d ∈ footprint a) {s t : M.State} (h : M.step b s t) :
        M.agree d s t

        If two operators have disjoint effects, a step of the second preserves every dimension that the first may change.

        source
        theorem SE.Transformation.declared_orthogonal_effects_disjoint (a b : OperatorCode) (h : orthogonality? a b = some OrthogonalityRelation.orthogonal) :
        EffectsDisjoint a b

        Consistency check: every declared orthogonal pair has disjoint effects.

        The declared entries are not derived from footprints. This theorem records that the footprints do not contradict the declared orthogonal pair.

        source
        theorem SE.Transformation.declared_overlapping_effects_overlap (a b : OperatorCode) (h : orthogonality? a b = some OrthogonalityRelation.overlapping) :
        EffectsOverlap a b

        Consistency check: every declared overlapping pair has overlapping effects.

        Footprint overlap shows only that the operators may touch a common dimension.