Finiteness semantics

From LLWiki
Revision as of 15:32, 30 September 2011 by Pierre-Marie Pédrot (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

The category \mathbf{Fin} 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 \mathbf{Fin}_\oc.

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.


Finiteness spaces

The construction of finiteness spaces follows a well known pattern. It is given by the following notion of orthogonality: a\mathrel \bot a' iff a\cap a' is finite. Then one unrolls familiar definitions, as we do in the following paragraphs.

Let A be a set. Denote by \powerset A the powerset of A and by \finpowerset A the set of all finite subsets of A. Let {\mathfrak F} \subseteq \powerset A any set of subsets of A. We define the pre-dual of {\mathfrak F} in A as {\mathfrak F}^{\bot_{A}}=\left\{a'\subseteq A;\ \forall a\in{\mathfrak F},\ a\cap a'\in\finpowerset A\right\}. In general we will omit the subscript in the pre-dual notation and just write {\mathfrak F}\orth. For all {\mathfrak F}\subseteq\powerset A, we have the following immediate properties: \finpowerset A\subseteq {\mathfrak F}\orth; {\mathfrak F}\subseteq {\mathfrak F}\biorth; if {\mathfrak G}\subseteq{\mathfrak F}, {\mathfrak F}\orth\subseteq {\mathfrak G}\orth. By the last two, we get {\mathfrak F}\orth = {\mathfrak F}\triorth. A finiteness structure on A is then a set {\mathfrak F} of subsets of A such that {\mathfrak F}\biorth = {\mathfrak F}.

A finiteness space is a dependant pair {\mathcal A}=\left(\web{\mathcal A},\mathfrak F\left(\mathcal A\right)\right) where \web {\mathcal A} is the underlying set (the web of {\mathcal A}) and \mathfrak F\left(\mathcal A\right) is a finiteness structure on \web {\mathcal A}. We then write {\mathcal A}\orth for the dual finiteness space: \web {{\mathcal A}\orth} = \web {\mathcal A} and \mathfrak F\left({\mathcal A}\orth\right)=\mathfrak F\left({\mathcal A}\right)^{\bot}. The elements of \mathfrak F\left(\mathcal A\right) are called the finitary subsets of {\mathcal A}.


For all set A, (A,\finpowerset A) is a finiteness space and (A,\finpowerset A)\orth = (A,\powerset A). In particular, each finite set A is the web of exactly one finiteness space: (A,\finpowerset A)=(A,\powerset A). We introduce the following two: \zero = \zero\orth = \left(\emptyset, \{\emptyset\}\right) and \one = \one\orth = \left(\{\emptyset\}, \{\emptyset, \{\emptyset\}\}\right). We also introduce the finiteness space of natural numbers {\mathcal N} by: |{\mathcal N}|={\mathbf N} and a\in\mathfrak F\left(\mathcal N\right) iff a is finite. We write \mathcal O=\{0\}\in\mathfrak F\left({\mathcal N}\right).

Notice that {\mathfrak F} is a finiteness structure iff it is of the form {\mathfrak G}\orth. It follows that any finiteness structure {\mathfrak F} is downwards closed for inclusion, and closed under finite unions and arbitrary intersections. Notice however that {\mathfrak F} is not closed under directed unions in general: for all k\in{\mathbf N}, write k{\downarrow}=\left\{j;\  j\le k\right\}\in\mathfrak F\left({\mathcal N}\right); then k{\downarrow}\subseteq k'{\downarrow} as soon as k\le k', but \bigcup_{k\ge0} k{\downarrow}={\mathbf N}\not\in\mathfrak F\left({\mathcal N}\right).


For all finiteness spaces {\mathcal A} and {\mathcal B}, we define {\mathcal A} \tens {\mathcal B} by \web {{\mathcal A} \tens {\mathcal B}} = \web{\mathcal A} \times \web{\mathcal B} and \mathfrak F\left({\mathcal A} \tens {\mathcal B}\right) = \left\{a\times b;\ a\in \mathfrak F\left(\mathcal A\right),\ b\in\mathfrak F\left(\mathcal B\right)\right\}\biorth. It can be shown that \mathfrak F\left({\mathcal A} \tens {\mathcal B}\right) = \left\{ c \subseteq \web{\mathcal A}\times\web{\mathcal B};\  \left.c\right|_l\in \mathfrak F\left(\mathcal A\right),\ \left.c\right|_r\in\mathfrak F\left(\mathcal B\right)\right\}, where \left.c\right|_l and \left.c\right|_r are the obvious projections.

Let f\subseteq A \times B be a relation from A to B, we write f\orth=\left\{(\beta,\alpha);\  (\alpha,\beta)\in f\right\}. For all a\subseteq A, we set f\cdot a = \left\{\beta\in B;\  \exists \alpha\in a,\ (\alpha,\beta)\in f\right\}. If moreover g\subseteq B \times C, we define g \bullet f = \left\{(\alpha,\gamma)\in A\times C;\  \exists \beta\in B,\ (\alpha,\beta)\in f\wedge(\beta,\gamma)\in g\right\}. Then, setting {\mathcal A}\limp{\mathcal B} = \left({\mathcal A}\otimes {\mathcal B}\orth\right)\orth, \mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)\subseteq {\web{\mathcal A}\times\web{\mathcal B}} is characterized as follows:

		f\in \mathfrak F\left({\mathcal A}\limp{\mathcal B}\right) &\iff \forall a\in \mathfrak F\left({\mathcal A}\right), f\cdot a \in\mathfrak F\left({\mathcal B}\right) \text{ and } \forall b\in \mathfrak F\left({\mathcal B}\orth\right), f\orth\cdot b \in\mathfrak F\left({\mathcal A}\orth\right)
		&\iff \forall a\in \mathfrak F\left({\mathcal A}\right), f\cdot a \in\mathfrak F\left({\mathcal B}\right) \text{ and } \forall \beta\in \web{{\mathcal B}}, f\orth\cdot \left\{\beta\right\} \in\mathfrak F\left({\mathcal A}\orth\right)
		&\iff \forall \alpha\in \web{{\mathcal A}}, f\cdot \left\{\alpha\right\} \in\mathfrak F\left({\mathcal B}\right) \text{ and } \forall b\in \mathfrak F\left({\mathcal B}\orth\right), f\orth\cdot b \in\mathfrak F\left({\mathcal A}\orth\right)

The elements of \mathfrak F\left({\mathcal A}\limp{\mathcal B}\right) are called finitary relations from {\mathcal A} to {\mathcal B}. By the previous characterization, the identity relation \mathsf{id}_{{\mathcal A}} = \left\{(\alpha,\alpha);\  \alpha\in\web{{\mathcal A}}\right\} is finitary, and the composition of two finitary relations is also finitary. One can thus define the category \mathbf{Fin} of finiteness spaces and finitary relations: the objects of \mathbf{Fin} are all finiteness spaces, and \mathbf{Fin}({\mathcal A},{\mathcal B})=\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right). Equipped with the tensor product \tens, \mathbf{Fin} is symmetric monoidal, with unit \one; it is monoidal closed by the definition of \limp; it is * -autonomous by the obvious isomorphism between {\mathcal A}\orth and {\mathcal A}\limp\one.


Setting \mathcal{S}=\left\{(k,k+1);\  k\in{\mathbf N}\right\} and \mathcal{P}=\left\{(k+1,k);\  k\in{\mathbf N}\right\}, we have \mathcal{S},\mathcal{P}\in\mathbf{Fin}({\mathcal N},{\mathcal N}) and \mathcal{P}\bullet\mathcal{S}=\mathsf{id}_{{\mathcal N}}.


We now introduce the cartesian structure of \mathbf{Fin}. We define {\mathcal A} \oplus {\mathcal B} by \web {{\mathcal A} \oplus {\mathcal B}} = \web{\mathcal A} \uplus \web{\mathcal B} and \mathfrak F\left({\mathcal A} \oplus {\mathcal B}\right) = \left\{ a\uplus b;\  a\in \mathfrak F\left(\mathcal A\right),\ b\in\mathfrak F\left(\mathcal B\right)\right\} where \uplus denotes the disjoint union of sets: x\uplus y=(\{1\}\times x)\cup(\{2\}\times y). We have \left({\mathcal A}\oplus {\mathcal B}\right)\orth = {\mathcal A}\orth\oplus{\mathcal B}\orth.[1] The category \mathbf{Fin} is both cartesian and co-cartesian, with \oplus being the product and co-product, and \zero the initial and terminal object. Projections are given by:

\lambda_{{\mathcal A},{\mathcal B}}&=\left\{\left((1,\alpha),\alpha\right);\ \alpha\in\web{\mathcal A}\right\}
\in\mathbf{Fin}({\mathcal A}\oplus{\mathcal B},{\mathcal A}) \\
\rho_{{\mathcal A},{\mathcal B}}&=\left\{\left((2,\beta),\beta\right);\ \beta\in\web{\mathcal B}\right\}
\in\mathbf{Fin}({\mathcal A}\oplus{\mathcal B},{\mathcal B}) 

and if f\in\mathbf{Fin}({\mathcal C},{\mathcal A}) and g\in\mathbf{Fin}({\mathcal C},{\mathcal B}), pairing is given by:

\left\langle f,g\right\rangle = \left\{\left(\gamma,(1,\alpha)\right);\ (\gamma,\alpha)\in f\right\} \cup \left\{\left(\gamma,(2,\beta)\right);\ (\gamma,\beta)\in g\right\} \in\mathbf{Fin}({\mathcal C},{\mathcal A}\oplus{\mathcal B}).

The unique morphism from {\mathcal A} to \zero is the empty relation. The co-cartesian structure is obtained symmetrically.


Write {\mathcal O}\orth=\left\{(0,\emptyset)\right\}\in\mathbf{Fin}({\mathcal N},\one). Then \left\langle{{\mathcal O}\orth},{\mathcal{P}}\right\rangle =\{ (0,(1,\emptyset)) \}\cup \{ (k+1,(2,k)) ;\  k\in{\mathbf N} \} \in\mathbf{Fin}\left({\mathcal N},\one\oplus{\mathcal N}\right) is an isomorphism.


If A is a set, we denote by \finmulset A the set of all finite multisets of elements of A, and if a\subseteq A, we write a^{\oc}=\finmulset a\subseteq\finmulset A. If \overline\alpha\in\finmulset A, we denote its support by \mathrm{Support}\left(\overline \alpha\right)\in\finpowerset A. For all finiteness space {\mathcal A}, we define \oc {\mathcal A} by: \web{\oc {\mathcal A}}= \finmulset{\web{{\mathcal A}}} and \mathfrak F\left(\oc{\mathcal A}\right)=\left\{a^{\oc};\  a\in\mathfrak F\left({\mathcal A}\right)\right\}\biorth. It can be shown that \mathfrak F\left(\oc{\mathcal A}\right) = \left\{\overline a\subseteq\finmulset{\web{{\mathcal A}}};\ \bigcup_{\overline\alpha\in \overline a}\mathrm{Support}\left(\overline \alpha\right)\in\mathfrak F\left(\mathcal A\right)\right\}. Then, for all f\in\mathbf{Fin}({\mathcal A},{\mathcal B}), we set

\oc f =\left\{\left(\left[\alpha_1,\ldots,\alpha_n\right],\left[\beta_1,\ldots,\beta_n\right]\right);\  \forall i,\ (\alpha_i,\beta_i)\in f\right\} \in \mathbf{Fin}(\oc {\mathcal A}, \oc {\mathcal B}),

which defines a functor. Natural transformations \mathsf{der}_{{\mathcal A}}=\left\{([\alpha],\alpha);\  \alpha\in \web{{\mathcal A}}\right\}\in\mathbf{Fin}(\oc{\mathcal A},{\mathcal A}) and \mathsf{digg}_{{\mathcal A}}=\left\{\left(\sum_{i=1}^n\overline\alpha_i,\left[\overline\alpha_1,\ldots,\overline\alpha_n\right]\right);\ \forall i,\ \overline\alpha_i\in\web{\oc {\mathcal A}}\right\} make this functor a comonad.


We have isomorphisms \left\{([],\emptyset)\right\}\in\mathbf{Fin}(\oc\zero,\one) and

\left\{ \left(\overline\alpha_l+\overline\beta_r,\left(\overline\alpha,\overline\beta\right)\right);\ (\overline\alpha_l,\overline\alpha)\in\oc\lambda_{{\mathcal A},{\mathcal B}}\wedge(\overline\beta_r,\overline\beta)\in\oc\rho_{{\mathcal A},{\mathcal B}}\right\} \in\mathbf{Fin}(\oc({\mathcal A}\oplus{\mathcal B}),\oc{\mathcal A}\tens\oc{\mathcal B}).

More generally, we have \oc\left({\mathcal A}_1\oplus\cdots\oplus{\mathcal A}_n\right)\cong\oc{\mathcal A}_1\tens\cdots\tens\oc{\mathcal A}_n.


  1. The fact that the additive connectors are identified, i.e. that we obtain a biproduct, is to be related with the enrichment of \mathbf{Fin} 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.
Personal tools