SHF: Small: Algebraic Foundations for Collaborative Data Sharing

数据复制需要复杂的工具，如同步器和版本控制系统，以便在对复制的数据结构进行更改时保持或恢复一致性。 不幸的是，这一领域蓬勃发展的活动并没有完全与其理论基础的进步相匹配，导致系统复杂，难以理解，并且容易出现令人惊讶的行为。 该项目旨在开发一个异构版本控制系统的数学基础和原型实现，能够管理多个副本的并发更新的传播和集成，其中每个副本可能以不同的方式表示，并且可能包含不与其他副本共享的信息。过去在这些领域的工作已经产生了重大的现实影响：Unison文件同步器现在是研究社区内外的大型用户社区的基本工具集的一部分，而Redhat的Augeas工具直接基于实验性双向语言Boomerang，正在成为系统配置管理的流行工具。 更好的数学基础将提高未来系统的功能性和鲁棒性--例如，用于软件模型转换的工业工具。该项目的主要技术线索是（1）对称透镜的代数理论，一种传播双向更新的机制，（2）为现代分布式版本控制系统提供坚实基础的新补丁理论，以及（3）体现这两组思想的系统的原型实现。

Data replication demands complex tools such as SYNCHRONIZERS and VERSION CONTROL SYSTEMS to maintain or restore consistency when changes are made to replicated data structures. Unfortunately, the burgeoning activity in this area has not been fully matched by advances in its theoretical underpinnings, resulting in systems that are complex, hard to understand, and prone to surprising behaviors. The project aims to develop mathematical foundations and a prototype implementation of a HETEROGENEOUS VERSION CONTROL SYSTEM, able to manage propagation and integration of concurrent updates to multiple replicas, where each replica may be represented differently and may include information that is not shared with the others.Past work in these areas has had significant real-world impacts: the Unison file synchronizer is now part of the basic toolset of a large community of users, both within and outside the research community, and Redhat's Augeas tool, based directly on the experimental bidirectional language Boomerang, is becoming a popular tool for system configuration management. Better mathematical foundations will improve the functionality and robustness of future systems---for example, industrial tools for software model transformation.The project's primary technical threads are (1) the algebraic theory of SYMMETRIC LENSES, a mechanism for propagating bidirectional updates, (2) a new THEORY OF PATCHES providing a solid foundation to modern distributed version control systems, and (3) a prototype implementation of a system embodying both sets of ideas.