What is a model for a semanticatty linear λ-calculus?

摘要

This article is about a categorical approach modelling a simple term calculus, named Sℓλ-calculus. This is the core calculus underlying the programming language SℓPCF conceived in order to program only linear functions between coherence spaces. We introduce the notion of Sℓλ-category, which is able to describe a large class of sound models of Sℓλ-calculus. An Sℓλ-category extends in a natural way Benton, Bierman, Hyland and de Paiva's Linear Category by requirements useful to interpret all the programming constructs of the Sℓλ-calculus. In particular, a key role is played by a !-coalgebra p:N→!N used to interpret the numeral constants of the Sℓλ-calculus. We will define two interpretations of Sℓλ-calculus types and terms into objects and morphisms of Sℓλ-categories: the first one is a generalization of the translation given in [23] but lacks completeness; the second one uses the !-coalgebra p:N→!N and the comonadic properties of ! to recover completeness. Finally, we show that this notion is general enough to capture interesting models in the category of sets and relations, in Scott Domains and in coherence spaces.