融合的逻辑
Logic of fusion
AI总结：
论文利用 Curry-Howard 同构将程序融合对应于切消除，并借助超自然变换重新解释参数化性，从而逻辑分析各类归纳与共归纳数据类型上的 build 融合。
摘要：
本工作的出发点是观察到，将类型与命题、程序与证明、复合与切分联系起来的 Curry-Howard 同构，可以扩展为程序融合与切消除之间的对应。这一简单思想为泛型编程和变换式编程的一些基本方法提供了逻辑解释。在本文中，我们对归纳和共归纳数据类型（包括正则或嵌套类型）上的 build 融合（也称为消森林化）的一般形式进行了逻辑分析。该分析基于本文引入的、以超自然变换对参数化性所作的一种新颖逻辑解释。
英文摘要：
The starting point of this work is the observation that the Curry-Howard isomorphism, relating types and propositions, programs and proofs, composition and cut, extends to the correspondence of program fusion and cut elimination. This simple idea suggests logical interpretations of some of the basic methods of generic and transformational programming. In the present paper, we provide a logical analysis of the general form of build fusion, also known as deforestation, over the inductive and the coinductive datatypes, regular or nested. The analysis is based on a novel logical interpretation of parametricity in terms of the paranatural transformations, introduced in the paper.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
