Multiple Model Synchronization with Multiary Delta Lenses with Amendment and K-Putput
Zinovy Diskin, Harald K\"onig, Mark Lawford

TL;DR
This paper introduces multiary delta lenses with amendments for synchronizing multiple models, extending the binary lens framework to handle more complex scenarios with reflective updates and composition properties.
Contribution
It proposes a novel multiary delta lens framework with amendments, addressing the less-studied multi-model synchronization problem and establishing composition results.
Findings
Defined multiary delta lenses with amendments
Proved composition theorems for these lenses
Enhanced understanding of multi-model synchronization mechanisms
Abstract
Multiple (more than 2) model synchronization is ubiquitous and important for model driven engineering, but its theoretical underpinning gained much less attention than the binary case. Specifically, the latter was extensively studied by the bx community in the framework of algebraic models for update propagation called lenses. Now we make a step to restore the balance and propose a notion of multiary delta lens. Besides multiarity, our lenses feature {\em reflective} updates, when consistency restoration requires some amendment of the update that violated consistency. We emphasize the importance of various ways of lens composition for practical applications of the framework, and prove several composition results.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Formal Methods in Verification · Logic, programming, and type systems
