Compositionality of update propagation: Laxed PutPut

Compatibility of update propagation with update composition (the infamous Putput law) is fundamental for the mathematical modelling of bx, but is not easy to ensure in practical scenarios. This severely restricts practical applicability of elegant algebraic models based on Putput, while leaving practical bx without solid algebraic support is also unsatisfactory. The paper aims to mitigate these problems, and presents the following findings. It is known that PutPut trivially holds for the sequential composition of two inserts or two deletes (what Johnson and Rosebrugh called the monotonic Putput); it also holds for the relational (pullback based) composition of a delete followed by an insert (the mixed Putput). In the present paper, we will see that relational Putput can fail for the relational composition of an insert followed by a delete, which represents a wide class of practically interesting examples. We will also analyze different ways of update composition, and discuss their interaction with update propagation. We will see that update propagation and Putput need a 2-categorical setting, formulate a notion of lax Putput, and show that it is much wider applicable to practical situations than the ordinary strict Putput.