A typed, algebraic, computational lambda-calculus
Benoît Valiron · Mathematical Structures in Computer Science · 2013
Lambda-calculi with vectorial structures have been studied in various ways, but their semantics remain largely uninvestigated. The main contribution of this paper is to provide a categorical framework for the semantics of such algebraic lambda-calculi. We first develop a categorical analysis of a general simply typed lambda-calculus endowed with the structure of a module. We study the problems arising from the addition of a fixed-point combinator and show how to modify the equational theory to solve them. The categorical analysis carries nicely over to the modified language. We provide various concrete models for both the case without fixpoints and for the case with them.