轻量逻辑与最优归约：完备性与复杂度
计算机科学中的逻辑
2007-05-23 v1 编程语言
摘要
初等与轻量仿射逻辑（分别为 EAL 和 LAL）中 lambda-项的类型化出于两个不同的原因被研究：一方面，使用 LAL（分别为 EAL）证明网的类型项求值具有有保证的多项式（分别为初等）界限；另一方面，这些项也可以使用 Lamping 算法的抽象版本通过最优归约进行求值。第一种归约是全局的，而第二种是局部且异步的。我们证明了对于 LAL（分别为 EAL）类型化的项，Lamping 抽象算法同样具有多项式（分别为初等）界限。我们还通过使用简单的交互几何模型（语境语义），证明了其可靠性及完备性（针对带有类型不动点的 EAL 和 LAL）。
引用
@article{arxiv.0704.2448,
title = {Light Logics and Optimal Reduction: Completeness and Complexity},
author = {Patrick Baillot and Paolo Coppola and Ugo Dal Lago},
journal= {arXiv preprint arXiv:0704.2448},
year = {2007}
}
评论
21 pages