一句话：提出商正则表达式与商透镜，并利用规范化定理从示例合成双向变换。
商透镜是一类双向变换，其正确性定律由指定等价关系“放宽”，可忽略数据格式中不重要的细节（如 XML 字段顺序）。本文研究如何从高层规格合成这类透镜。作者引入商正则表达式（QRE），用注解正则表达式同时刻画正则语言及其上的等价关系；进而定义 QRE 透镜，并证明关键规范化定理：每个 QRE 透镜都可转换为功能等价的透镜，仅在“边缘”规范化源和目标数据，中间映射由双射透镜完成。基于该范型，他们从一对 QRE 与输入输出示例合成 QRE 透镜，复用已有普通双射透镜合成算法。该方法已在双向编程语言 Boomerang 中实现，并在 Optician 基准的真实数据格式间合成 QRE 透镜进行评估。
Quotient lenses are bidirectional transformations whose correctness laws are “loosened” by specified equivalence relations, allowing inessential details in concrete data formats to be suppressed. For example, a programmer could use a quotient lens to define a transformation that ignores the order of fields in XML data, so that two XML files with the same fields but in different orders would be considered the same, allowing a single, simple program to handle them both. Building on a recently published algorithm for synthesizing plain bijective lenses from high-level specifications, we show how to synthesize bijective quotient lenses in three steps. First, we introduce quotient regular expressions (QREs), annotated regular expressions that conveniently mark inessential aspects of string data formats; each QRE specifies, simulteneously, a regular language and an equivalence relation on it. Second, we introduce QRE lenses , i.e., lenses mapping between QREs. Our key technical result is a proof that every QRE lens can be transformed into a functionally equivalent lens that canonizes source and target data just at the “edges” and that uses a bijective lens to map between the respective canonical elements; no internal canonization occurs in a lens in this normal form. Third, we leverage this normalization theorem to synthesize QRE lenses from a pair of QREs and example input-output pairs, reusing earlier work on synthesizing plain bijective lenses. We have implemented QREs and QRE lens synthesis as an extension to the bidirectional programming language Boomerang. We evaluate the effectiveness of our approach by synthesizing QRE lenses between various real-world data formats in the Optician benchmark suite.
@article{paperbot289,
title = {Synthesizing quotient lenses},
author = {Solomon Maina and Anders Miltner and Kathleen Fisher and Benjamin C. Pierce and David Walker and Steve Zdancewic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236775}
}