A Concrete Categorical Semantics of Lambda- S
Alejandro Díaz-Caro, Octavio Malherbe · Electronic Notes in Theoretical Computer Science · 2019
Lambda- S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type system of Lambda- S have a constructor S such that a type A is considered as the base of a vector space while S ( A ) is its span. A first semantics of this calculus have been given when first presented, with such an interpretation: superposed types are interpreted as vectors spaces while non-superposed types as their basis. In this paper we give a concrete categorical semantics of Lambda- S , showing that S is interpreted 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.