What is a Model of the Linear Lambda Calculus?

Abstract

We investigate the notion of model of the linear $\lambda$-calculus from an algebraic perspective. Our starting point is the operad of linear $\lambda$-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 $\lambda$-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 $\lambda$-calculus. As a second contribution, we give a finite equational presentation for the linear variant of $\lambda$-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.