Church => Scott = Ptime：资源敏感可实现性的一个应用
计算机科学中的逻辑
2010-05-05 v1
摘要
我们引入了一种线性逻辑的变体，具有二阶量词和类型不动点，两者都限制在纯线性公式上。二进制词的 Church 编码由标准非线性类型 'Church' 定型，而 Scott 编码（词的纯线性表示）则由线性类型 'Scott' 定型。我们给出了多项式时间函数的刻画，该刻画源自 (Leivant and Marion 93)：一个函数是多项式时间可计算的，当且仅当它可以由类型 Church => Scott 的项表示。为了证明可靠性，我们采用了 Hofmann 和 Dal Lago 开发的资源敏感可实现性技术。
引用
@article{arxiv.1005.0524,
title = {Church => Scott = Ptime: an application of resource sensitive realizability},
author = {Aloïs Brunel and Kazushige Terui},
journal= {arXiv preprint arXiv:1005.0524},
year = {2010}
}