一句话：为带最小/最大不动点的线性逻辑 μLL 的非良基与循环证明建立范畴语义，并证明翻译保持解释。
本文研究带最小和最大不动点的线性逻辑 μLL 中非良基证明与循环证明的指称不变量，提出一套范畴语义。作者依次为三类对象给出语义：(i) 任意非良基预证明，无论是否有效；(ii) 有效预证明，利用范畴模型上的正交性构造刻画有效性；(iii) 循环强有效预证明，同时利用有效性和正则性归纳定义解释。随后分析从有穷证明到非良基证明、以及从（强有效）循环证明到有穷证明的翻译，证明这两个方向的翻译都保持语义解释。
This paper investigates the denotational invariants of non-wellfounded and circular proofs of linear logic with least and greatest fixed points, μLL, by providing a categorical semantics. More precisely the paper successively introduces semantics for (i) non-wellfounded pre-proofs, be they valid or not, (ii) valid pre-proofs exploiting their validity condition by considering an orthogonality construction on the given categorical model and finally (iii) circular strongly valid pre-proofs, exploiting both validity and regularity in order to define inductively the interpretation. Then the paper investigates the semantical content of the translation from finitary proofs to non-wellfounded proofs and, conversely, from (strongly valid) circular proofs to finitary proofs, showing that both translations preserve the interpretation.
@inproceedings{paperbot8655,
title = {On the denotation of circular and non-wellfounded proofs in linear logic with fixed points},
author = {Thomas Ehrhard and Farzad Jafarrahmani and Alexis Saurin},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00014}
}