The category of finiteness spaces and finitary relations was introduced by Ehrhard, refining the purely relational model of linear logic. A finiteness space is a set equipped with a finiteness structure, i.e. a particular set of subsets which are said to be finitary; and the model is such that the usual relational denotation of a proof in linear logic is always a finitary subset of its conclusion. By the usual co-Kleisli construction, this also provides a model of the simply typed lambda-calculus: the cartesian closed category .
The main property of finiteness spaces is that the intersection of two finitary subsets of dual types is always finite. This feature allows to reformulate Girard's quantitative semantics in a standard algebraic setting, where morphisms interpreting typed λ-terms are analytic functions between the topological vector spaces generated by vectors with finitary supports. This provided the semantical foundations of Ehrhard-Regnier's differential λ-calculus and motivated the general study of a differential extension of linear logic.
It is worth noticing that finiteness spaces can accomodate typed λ-calculi only: for instance, the relational semantics of fixpoint combinators is never finitary. The whole point of the finiteness construction is actually to reject infinite computations. Indeed, from a logical point of view, computation is cut elimination: the finiteness structure ensures the intermediate sets involved in the relational interpretation of a cut are all finite. In that sense, the finitary semantics is intrinsically typed.
The construction of finiteness spaces follows a well known pattern. It is given by the following notion of orthogonality: iff is finite. Then one unrolls familiar definitions, as we do in the following paragraphs.
Let A be a set. Denote by the powerset of A and by the set of all finite subsets of A. Let any set of subsets of A. We define the pre-dual of in A as . In general we will omit the subscript in the pre-dual notation and just write . For all , we have the following immediate properties: ; ; if , . By the last two, we get . A finiteness structure on A is then a set of subsets of A such that .
A finiteness space is a dependant pair where is the underlying set (the web of ) and is a finiteness structure on . We then write for the dual finiteness space: and . The elements of are called the finitary subsets of .
For all set A, is a finiteness space and . In particular, each finite set A is the web of exactly one finiteness space: . We introduce the following two: and . We also introduce the finiteness space of natural numbers by: and iff a is finite. We write .
Notice that is a finiteness structure iff it is of the form . It follows that any finiteness structure is downwards closed for inclusion, and closed under finite unions and arbitrary intersections. Notice however that is not closed under directed unions in general: for all , write ; then as soon as , but .
For all finiteness spaces and , we define by and . It can be shown that , where and are the obvious projections.
Let be a relation from A to B, we write . For all , we set . If moreover , we define . Then, setting , is characterized as follows:
The elements of are called finitary relations from to . By the previous characterization, the identity relation is finitary, and the composition of two finitary relations is also finitary. One can thus define the category of finiteness spaces and finitary relations: the objects of are all finiteness spaces, and . Equipped with the tensor product , is symmetric monoidal, with unit ; it is monoidal closed by the definition of ; it is * -autonomous by the obvious isomorphism between and .
Setting and , we have and .
We now introduce the cartesian structure of . We define by and where denotes the disjoint union of sets: . We have . The category is both cartesian and co-cartesian, with being the product and co-product, and the initial and terminal object. Projections are given by:
and if and , pairing is given by:
The unique morphism from to is the empty relation. The co-cartesian structure is obtained symmetrically.
Write . Then is an isomorphism.
If A is a set, we denote by the set of all finite multisets of elements of A, and if , we write . If , we denote its support by . For all finiteness space , we define by: and . It can be shown that . Then, for all , we set
which defines a functor. Natural transformations and make this functor a comonad.
We have isomorphisms and
More generally, we have .
- ↑ The fact that the additive connectors are identified, i.e. that we obtain a biproduct, is to be related with the enrichment of over the monoid structure of set union: see Marcello P. Fiore. Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic. TLCA 2007. This identification can also be shown to be a isomorphism of LL with sums of proofs.