轻量线性逻辑（证物图、编程notation、P-Time 正确性与完备性）
摘要
本文是对轻量线性逻辑及其直觉主义片段的系统性介绍。轻量线性逻辑具有多项式时间复杂度的剪切消除（P-Time 正确性），并编码所有 P-Time 图灵机（P-Time 完备性）。通过引入直觉主义轻量线性逻辑的证物图来证明 P-Time 正确性。 thanks to a very compact program notation, P-Time completeness is demonstrated in full details. On one side, the proof of P-Time correctness describes how the complexity of cut elimination is controlled, thanks to a suitable cut elimination strategy that exploits structural properties of the Proof nets. This allows to have a good catch on the meaning of the ``paragraph'' modality, which is a peculiarity of light logics. On the other side, the proof of P-Time completeness, together with a lot of programming examples, gives a flavor of the non trivial task of programming with resource limitations, using Intuitionistic Light Affine Logic derivations as programs.
引用
@article{arxiv.cs/0006010,
title = {Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)},
author = {Andrea Asperti and Luca Roversi},
journal= {arXiv preprint arXiv:cs/0006010},
year = {2009}
}