一句话：为线性/非线性 lambda 演算的 string diagram 语言建立富化语义模型，并扩展一般递归与证明可靠性/充分性。
Benton 的线性/非线性（LNL）模型可可靠地解释 LNL 项演算与 LNL 逻辑。本文研究如何用这类模型解释 Rios 和 Selinger 为 string diagram 提出的 LNL lambda 演算，该语言主要面向量子计算。作者证明每个 LNL 模型都可诱导一个典范的富化（enrichment），并可靠地解释该演算；这种抽象处理还给出比已有工作更简单的具体模型。文章进一步把语言扩展到带一般递归的情形并证明可靠性，最后对无 diagram 片段给出 adequacy 结果，该片段对应带递归的 Benton-Wadler adjoint calculus 的修改版本。
Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus for string diagrams, introduced by Rios and Selinger (with primary application in quantum computing). Our abstract treatment of this language leads to simpler concrete models compared to those presented so far. We also extend the language with general recursion and prove soundness. Finally, we present an adequacy result for the diagram-free fragment of the language which corresponds to a modified version of Benton and Wadler's adjoint calculus with recursion.
DOI 原文 ·
@inproceedings{paperbot4379,
title = {Enriching a Linear/Non-linear Lambda Calculus},
author = {Bert Lindenhovius and Michael Mislove and Vladimir Zamdzhiev},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209196}
}