论文标题
融合的逻辑
Logic of fusion
论文作者
论文摘要
这项工作的起点是观察到的，咖喱 - 霍华德同构，将类型和命题，程序和证明，组成和剪切相关，扩展到程序融合和剪切消除的对应关系。这个简单的想法暗示了对通用和变革性编程的一些基本方法的逻辑解释。在本文中，我们对构建融合的一般形式（也称为森林砍伐）提供了逻辑分析，在电感和嵌套的诱导性数据类型上。该分析是基于本文中引入的属性转化的新型逻辑解释。
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.
