Composition Constraints from Effects

RestoresOn M a b D says that in model M, applying b after a returns every dimension in D to its starting agreement.

The results here are necessary conditions only. An operator cannot restore a dimension that it cannot touch. That a footprint relationship is compatible with restoration does not show that any pair restores anything: actual restoration needs further laws on the model.

def SE.Transformation.RestoresOn (M : StateModel) (a b : OperatorCode) (D : List Dimension) : Prop

Applying b after a returns every dimension in D to its starting agreement.

Equations

• SE.Transformation.RestoresOn M a b D = ∀ (s t : M.State), M.step a s t → ∃ (u : M.State), M.step b t u ∧ ∀ (d : SE.Transformation.Dimension), d ∈ D → M.agree d s u

theorem SE.Transformation.restoration_needs_footprint {M : StateModel} {a b : OperatorCode} {D : List Dimension} {s t : M.State} (hr : RestoresOn M a b D) (hs : M.step a s t) {C : List Dimension} (hC : C ∈ requirements a) (hD : ∀ (d : Dimension), d ∈ C → d ∈ D) : ∃ (d : Dimension), d ∈ C ∧ d ∈ footprint b

Necessary condition for restoration: if b after a restores a set of dimensions containing every member of a required clause C of a, then some member of C lies in the footprint of b.

theorem SE.Transformation.declared_inverseLike_footprint_necessary (a b : OperatorCode) (h : composition? a b = some CompositionRelation.inverseLike) (C : List Dimension) : C ∈ requirements a → ∃ (d : Dimension), d ∈ C ∧ d ∈ footprint b

Necessary footprint condition for declared inverse-like pairs: every required clause of the first operator contains a dimension in the footprint of the second.

This does not show that the second operator restores anything.