lambda演算中多项式时间计算的轻量类型
计算机科学中的逻辑
2016-08-31 v2
摘要
我们为lambda演算提出了一种新的类型系统，以确保良类型化的程序可在多项式时间内执行：双轻量仿射逻辑（DLAL）。DLAL具有简单的类型语言，包含线性类型箭头和直觉主义类型箭头以及一个模态算子。它对应于轻量仿射逻辑（LAL）的一个片段。我们表明，与LAL相反，DLAL在lambda项上确保了良好的性质：满足归约保型性，并且良类型化的项在任何归约策略下都满足多项式归约步数界限。我们证明了与LAL一样，DLAL能够表示所有多项式时间函数。最后，我们给出了命题DLAL的类型推断过程。
引用
@article{arxiv.cs/0402059,
title = {Light types for polynomial time computation in lambda-calculus},
author = {Patrick Baillot and Kazushige Terui},
journal= {arXiv preprint arXiv:cs/0402059},
year = {2016}
}
备注
20 pages (including 10 pages of appendix). (revised version; in particular section 5 has been modified). A short version is to appear in the proceedings of the conference LICS 2004 (IEEE Computer Society Press)