2026/07/22 by Arturo De Faveri
#cs.LO
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 B, C, and 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.