软 lambda 演算：一种用于多项式时间计算的语言
计算机科学中的逻辑
2007-05-23 v1 计算复杂性
摘要
软线性逻辑（[Lafont02]）是线性逻辑的一个子系统，它刻画了 PTIME 类。我们引入软 lambda 演算，作为可在此逻辑的直觉主义和仿射变体中进行类型指派的演算。我们证明了该演算的（无类型）项可在多项式时间内归约。随后，我们用递归类型扩展了 Soft 逻辑的类型系统。这使我们能够考虑用于表示列表的非标准类型。利用这些数据类型，我们以插入排序算法为例考察了软 lambda 演算的具体表达能力。
引用
@article{arxiv.cs/0312015,
title = {Soft lambda-calculus: a language for polynomial time computation},
author = {Patrick Baillot and Virgile Mogbil},
journal= {arXiv preprint arXiv:cs/0312015},
year = {2007}
}
备注
20 pages