An algebraic semantics for bidirectional model synchronization

The GSDLAB technical reports are published as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author’s copyright. These works may not be reposted without the explicit permission of the copyright holder. A Product Line of Lax Lenses. Zinovy Diskin1,2 The goal of the present document is to support the taxonomy for bidirectional model synchronization developed in [1] with a formal semantics. The taxonomy is 3D so that each synchronization type is characterized by a triple of coordinates (x, y, z), in which x classifies the organizational symmetry of the case, y is for the informational symmetry, and z is for incrementality of the update propagation operations. Different types of delta lenses (algebraic structures modeling bx) can be classified by points on the YZ-plane. As for the x-coordinate, it says, roughly, whether updat