State Model

A state model interprets Transformation operators over abstract transformation configurations. A state is a configuration: it may contain referents, representations, components, relations, containment, bindings, lineage, evidence, and standing. No concrete configuration representation is assumed.

A model supplies:

• the states;
• an agreement equivalence for each effect dimension;
• an atomic step relation for each operator, relating a before-configuration to an after-configuration.

step op s t is the intrinsic effect of one application of op. It does not include incidental changes, which belong to separate operator steps or compound transformations.

A model must satisfy two laws.

• Frame: a step leaves every dimension outside the operator footprint unchanged.
• Change: for every required clause of the operator, a step changes at least one dimension in that clause.

Two generic results follow.

• Preservation: if agreement on a set of dimensions suffices for a relation, and the operator footprint avoids them, a step preserves the relation.
• Breakage: if, for some required clause, agreement on every dimension in the clause is required for a relation, every step breaks the relation.

Only the sufficient direction of breakage follows from the laws. The converse is a property of the maximal model for relations defined exactly by dimension agreement.

structure SE.Transformation.StateModel : Type 1

A state model: configurations, per-dimension agreement, and atomic operator steps.

• State : Type

  The transformation configurations.

• agree : Dimension → self.State → self.State → Prop

  Agreement of two configurations with respect to one dimension.

• agree_equiv (d : Dimension) : Equivalence (self.agree d)

  Agreement in each dimension is an equivalence.

• step : OperatorCode → self.State → self.State → Prop

  step op s t: t is the result of one atomic application of op to s.

• frame {op : OperatorCode} {s t : self.State} : self.step op s t → ∀ (d : Dimension), ¬d ∈ footprint op → self.agree d s t

  Frame law: dimensions outside the footprint are unchanged.

• change {op : OperatorCode} {s t : self.State} : self.step op s t → ∀ (C : List Dimension), C ∈ requirements op → ∃ (d : Dimension), d ∈ C ∧ ¬self.agree d s t

  Change law: every required clause has a dimension that changes.

def SE.Transformation.StateModel.AgreementSuffices (M : StateModel) (D : List Dimension) (P : M.State → M.State → Prop) : Prop

Agreement on every dimension in D suffices for the relation P.

Equations

• M.AgreementSuffices D P = ∀ (s t : M.State), (∀ (d : SE.Transformation.Dimension), d ∈ D → M.agree d s t) → P s t

def SE.Transformation.StateModel.AgreementRequired (M : StateModel) (d : Dimension) (P : M.State → M.State → Prop) : Prop

The relation P requires agreement on the dimension d: whenever P holds, the configurations agree on d.

Equations

• M.AgreementRequired d P = ∀ (s t : M.State), P s t → M.agree d s t

theorem SE.Transformation.StateModel.step_preserves {M : StateModel} {D : List Dimension} {P : M.State → M.State → Prop} {op : OperatorCode} {s t : M.State} (hP : M.AgreementSuffices D P) (hD : ∀ (d : Dimension), d ∈ D → ¬d ∈ footprint op) (h : M.step op s t) : P s t

Frame-based preservation: if agreement on D suffices for P and the footprint of op avoids D, a step of op preserves P.

theorem SE.Transformation.StateModel.step_breaks {M : StateModel} {P : M.State → M.State → Prop} {op : OperatorCode} {s t : M.State} {C : List Dimension} (hC : C ∈ requirements op) (hP : ∀ (d : Dimension), d ∈ C → M.AgreementRequired d P) (h : M.step op s t) : ¬P s t

Required-change breakage: if some required clause C of op has the property that P requires agreement on every dimension in C, then every step of op breaks P.

def SE.Transformation.maximalModel : StateModel

The maximal model. A step of op may change any dimensions inside the footprint, and must change at least one dimension in every required clause. It satisfies the two laws and assumes nothing further.

Equations

• One or more equations did not get rendered due to their size.

theorem SE.Transformation.maximalModel_step_exists (op : OperatorCode) : ∃ (s : maximalModel.State), ∃ (t : maximalModel.State), maximalModel.step op s t

Satisfiability: every operator has an admissible step in the maximal model, so the frame law and the clause requirements are consistent.

def SE.Transformation.agreementOn (S : List Dimension) : maximalModel.State → maximalModel.State → Prop

Agreement on exactly the dimensions in S, in the maximal model.

Equations

• SE.Transformation.agreementOn S s t = ∀ (d : SE.Transformation.Dimension), d ∈ S → s d = t d

theorem SE.Transformation.maximalModel_breaks_agreementOn_iff (op : OperatorCode) (S : List Dimension) : (∀ (s t : maximalModel.State), maximalModel.step op s t → ¬agreementOn S s t) ↔ ∃ (C : List Dimension), C ∈ requirements op ∧ ∀ (d : Dimension), d ∈ C → d ∈ S

Model-specific completeness. In the maximal model, every step of op breaks agreement on S exactly when S contains some required clause of op.

This shows that the clause condition of StateModel.step_breaks is tight for relations defined exactly by dimension agreement. It is a property of the maximal model, not a consequence of the two laws.