完成其一，余下699待续：抑或组合式脱糖变换的综合

现实系统中使用的编程或脚本语言很少从一开始就以形式语义为设计出发点。因此，为这些系统开发有坚实基础的分析工具，首先需要逆向工程出形式语义。这可能需要数月乃至数年的努力。我们能否（至少部分地）自动化这一过程？尽管这一目标令人向往，但如 Krishnamurthi 等人 [2019] 所发现的，从实现中自动逆向工程出语义规则极具挑战性。在本文中，我们指出由于状态空间爆炸，方法随语言规模扩展非常困难，因此提出增量式地学习语义。我们给出了 Krishnamurthi 等人脱糖学习框架的形式化，以厘清增量学习算法可行所必需的假设。我们表明，这一重构使我们能够扩展搜索空间并表达 Krishnamurthi 等人描述为具有挑战性的规则，同时仍保持可行性。我们将枚举综合作为基线算法进行评估，并证明，借助我们对问题的重构，在大多数情况下可与预期规则完全一致地，为 Krishnamurthi 等人提出的示例源语言与核心语言学习到正确的脱糖规则。此外，在用户引导下，我们的系统能够综合出用于脱糖列表推导式以及 try/catch/finally 结构的规则。