Confluence in Lens Synthesis

A lens is a program that can be executed both forwards and backwards, from input to output and from output back to input again. Domain-specific languages for defining lenses have been developed to help users synchronize text files, and construct different “views” of databases, among other applications. Recent research has shown how string lenses can be synthesized from their types, which are pairs of regular expressions. However, guaranteeing that we can synthesize all possible lenses is quite tricky on these languages, due in large part to the many equivalences on regular expressions. The proof that all string lenses are synthesizeable involves proving a confluence-like property, parameterized by a an additional binary relation R. We call this property Rconfluence. In this model, standard confluence is the specific case where R is equality. In this paper, we show how existing techniques for demonstrating confluence do not work in the domain of R-confluence, and find that if the rewrite system is =-confluent and satisfies a commutativity property with R, then the system is R-confluent.