Normal Forms and Cut-Free Proofs as Natural Transformations
Normal Forms and Cut-Free Proofs as Natural Transformations
复制标题
作为自然变换的范式和免割证明
DOI：
10.1007/978-1-4612-2822-6_8
复制
发表时间：
1992
影响因子：
0.8
通讯作者：
P. Scott
中科院分区：
文献类型：
--
作者：
J. Girard;A. Scedrov;P. Scott
我们可以保证简单的函数程序必须满足哪些方程，而不考虑它们明显的定义方程？同样地，在λ项之间必须有什么非平凡的标识，被认为是编码适当的自然演绎证明？我们证明了通常的句法保证了范畴论中的某些自然性方程是必然可证明的。同时，我们的分类方法解决了切消的等价意义和无切证明的不对称解释。这一观点与Reynolds关于参数性的关系解释（[27],[2]）以及Kelly-Lambek-Mac Lane-Mints在范畴论中研究相干性问题的方法有关。
What equations can we guarantee that simple functional programs must satisfy, irrespective of their obvious defining equations? Equivalently, what non-trivial identifications must hold between lambda terms, thought-of as encoding appropriate natural deduction proofs ? We show that the usual syntax guarantees that certain naturality equations from category theory are necessarily provable. At the same time, our categorical approach addresses an equational meaning of cut-elimination and asymmetrical interpretations of cut-free proofs. This viewpoint is connected to Reynolds’ relational interpretation of parametricity ([27], [2]), and to the Kelly-Lambek-Mac Lane-Mints approach to coherence problems in category theory.