通过双光仿射逻辑验证系统F项的Ptime可归约性
计算机科学中的逻辑
2007-05-23 v1
摘要
在之前的工作中，我们引入了双光仿射逻辑（DLAL）（[BaillotTerui04]）作为光线性逻辑的一种变体，适用于保证lambda演算项的复杂性属性：所有可类型化的项都可以在多项式时间内求值，并且所有Ptime函数都可以表示。在当前工作中，我们解决了在二阶DLAL中对lambda项进行类型化的问题。为此，我们给出了一个过程，该过程从系统F中类型化的项开始，找到所有可能的方式将其装饰成DLAL类型化的项。我们表明，我们的过程可以在原始Church类型化的系统F项大小的多项式时间内运行。
引用
@article{arxiv.cs/0603104,
title = {Verification of Ptime reducibility for system F terms via Dual Light Affine Logic},
author = {Vincent Atassi and Patrick Baillot and Kazushige Terui},
journal= {arXiv preprint arXiv:cs/0603104},
year = {2007}
}
备注
21 pages