从证明生成集合转换
Generating collection transformations from proofs
摘要：
嵌套关系由原子类型通过乘积和集合类型构建而成，形成了丰富的数据模型。在过去的几十年中，嵌套的关系演算，NRC，已经成为一种标准的语言，用于定义嵌套集合的转换。NRC是一种强类型的函数式语言，它允许使用元组和投影、单元组形成器和映射操作来构建转换，该映射操作将元组上的转换提升到集合上的转换。在这项工作中，我们描述了一种替代的声明性方法来描述逻辑中的转换。一个具有不同输入和输出的公式给出了一个隐式定义，如果我们可以证明对于每个输入只有一个输出满足它。我们的主要结果表明，我们可以从公式提供隐式定义的证明中合成变换，其中证明是在一个直觉主义演算中，该演算捕获了嵌套集合的自然推理风格。我们的多项式时间合成过程是基于克雷格的插值引理的模拟，从一个可证明的包含项之间表示嵌套集合，并生成一个NRC表达式，它们之间的插值。我们进一步表明，实现隐式定义的NRC表达式，可以找到一个经典的功能证明时，不只是当有一个直观的。也就是说，只要公式隐式定义了一个转换，就有一个NRC表达式来实现它。
英文摘要：
Nested relations, built up from atomic types via product and set types, form a rich data model. Over the last decades the nested relational calculus, NRC, has emerged as a standard language for defining transformations on nested collections. NRC is a strongly-typed functional language which allows building up transformations using tupling and projections, a singleton-former, and a map operation that lifts transformations on tuples to transformations on sets. In this work we describe an alternative declarative method of describing transformations in logic. A formula with distinguished inputs and outputs gives an implicit definition if one can prove that for each input there is only one output that satisfies it. Our main result shows that one can synthesize transformations from proofs that a formula provides an implicit definition, where the proof is in an intuitionistic calculus that captures a natural style of reasoning about nested collections. Our polynomial time synthesis procedure is based on an analog of Craig's interpolation lemma, starting with a provable containment between terms representing nested collections and generating an NRC expression that interpolates between them. We further show that NRC expressions that implement an implicit definition can be found when there is a classical proof of functionality, not just when there is an intuitionistic one. That is, whenever a formula implicitly defines a transformation, there is an NRC expression that implements it.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
