We give an adequate, concrete, categorical-based model for Lambda-S, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables, and to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S have a superposition constructor S such that a type A is considered as the base of a vector space while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

翻译：我们为Lambda-S给出了一个充分且具体的、基于范畴论的模型。Lambda-S是一种类型化的线性代数λ演算，并扩展了测量操作。Lambda-S是对一阶λ演算的扩展，统一了量子λ演算中两种非克隆方法：禁止变量重复，以及将所有λ项视为代数线性函数。Lambda-S的类型系统包含一个叠加构造子S，使得类型A被视为向量空间的基，而SA是其张成空间。我们的模型将S视为集合范畴与复数域上向量空间范畴之间伴随关系中的两个函子的复合。右伴随是一个遗忘函子U，它在语言中是隐式的，并在计算推理中发挥核心作用。