Lens Laws Zoo
摘要
The bidirectional transformation has played beneficial roles in broad areas, database management, programming languages and model-driven development after Foster et al. revisited view updating problems introduced by Bancilhon and Spyratos. They introduced the concept of the (asymmetric) lens as a pair of a forward get and a backward put functions to synchronize source data and its view consistently. The consistency of the get and put functions is specified by several lens laws such as the (StrongGetPut), (GetPut), (PutGet) and (PutPut) laws. By combining some of these lens laws, we can represent how consistent a lens is. This chapter introduces 15 lens laws proposed in the literature, with their definitions, motivations and examples. In addition, their precise relationship will be given, such as the fact that one law implies another and that combining two laws is equivalent to combining three others. All implication relations are shown by a diagram, which is complete: every implication among lens laws is derivable by taking their transitive closure; the others have a counterexample. The results can be used to verify the law of desirable lenses quickly.