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.

翻译：暂无翻译