Behavior Update Word Action

Abstract

Controlled behavior updates descend to the realized range and compose along words.

Theorem 1.1 (Behavior updates are representative-independent and act by words).

$$\begin{array}{c}\forall U,Y,O:Type,\\ \forall F:U\to \left(Y\to Y\right),q:Y\to O,\\ (\forall u:U,y,y_p:Y,\mathrm{controlledBehavior}(F,q,y)=\mathrm{controlledBehavior}(F,q,y_p)\Rightarrow \mathrm{controlledBehavior}(F,q,F(u)(y))=\mathrm{controlledBehavior}(F,q,F(u)(y_p)))\wedge \\ (\forall u:U,y:Y,\mathrm{behaviorUpdate}(F,q,u)(\mathrm{rangeFactorization}(\mathrm{controlledBehavior}(F,q),y))=\mathrm{rangeFactorization}(\mathrm{controlledBehavior}(F,q),F(u)(y)))\wedge \\ (\forall b:\mathrm{range}(\mathrm{controlledBehavior}(F,q)),\mathrm{behaviorWordUpdate}(F,q,\mathrm{nil}(U))(b)=b)\wedge \\ (\forall v,w:\mathrm{List}(U),b:\mathrm{range}(\mathrm{controlledBehavior}(F,q)),\mathrm{behaviorWordUpdate}(F,q,\mathrm{append}(v,w))(b)=\mathrm{behaviorWordUpdate}(F,q,w)(\mathrm{behaviorWordUpdate}(F,q,v)(b)))\wedge \\ (\forall w:\mathrm{List}(U),y:Y,\mathrm{behaviorWordUpdate}(F,q,w)(\mathrm{rangeFactorization}(\mathrm{controlledBehavior}(F,q),y))=\mathrm{rangeFactorization}(\mathrm{controlledBehavior}(F,q),\mathrm{runWord}(F,w,y))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/RefinementClosure/BehaviorUpdateWordAction.behavior_update_well_defined (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equality of complete controlled behaviors is preserved after every input. The one-input update is transported through the canonical quotient-to-range equivalence, so it lives on the exact realized behavior range.

The named word update has the empty-word and concatenation laws. Its value on every realized behavior is the behavior of the source state after the imported left-to-right word execution.

References

• Truth anchor: D5/S3/ObserverMemory/RefinementClosure/BehaviorUpdateWordAction.behavior_update_well_defined
• Dependency: D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality