AI 中文总结
从代数角度研究线性λ演算模型，证明其与Curry的λ代数线性类似物和半封闭操作代数等价，给出λ代数线性变体的有限等式表示，并建立Scott表示定理的线性类似物。
AI 中文摘要
我们从代数角度研究线性λ演算的模型概念。以线性λ项的操作代数为出发点，其代数提供了自然候选。证明该模型概念等同于另外两种结构：Curry的λ代数的线性类似物和半封闭操作代数。这三种方法的等价统一了关于线性λ演算模型应为何物的三个互补答案。还给出了使用线性组合子的λ代数线性变体的有限等式表示。最后，利用与半封闭操作代数的等价性，通过表明每个模型在预层的自然幺半闭范畴中作为自反对象出现，建立了Scott表示定理的线性类似物。
英文摘要
We investigate the notion of model of the linear $λ$-calculus from an algebraic perspective. Our starting point is the operad of linear $λ$-terms, whose algebras provide a natural candidate. We prove that this notion of model is equivalent to two other structures: a linear analogue of Curry's $λ$-algebras, and semiclosed operads, a class of operads equipped with an internal abstraction operation. The equivalence between these three approaches unifies three complementary answers to the question of what should be regarded as a model of the linear $λ$-calculus. As a second contribution, we give a finite equational presentation for the linear variant of $λ$-algebras using the linear combinators $\mathbf{B}$, $\mathbf{C}$, and $\mathbf{I}$. Finally, exploiting the equivalence with semiclosed operads, we establish a linear analogue of Scott's representation theorem by showing that every model arises as a reflexive object in a natural monoidal closed category of presheaves.
