Finiteness semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
m (fixed display math)
m (link to orthogonalities)
 
(7 intermediate revisions by 2 users not shown)
Line 1: Line 1:
The category <math>\mathbf{Fin}</math> 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 <math>\mathbf{Fin}_\oc</math>.
+
The category <math>\mathbf{Fin}</math> of finiteness spaces and finitary relations was introduced by Ehrhard, refining the [[relational semantics|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 <math>\mathbf{Fin}_\oc</math>.
   
 
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 <math>\lambda</math>-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 <math>\lambda</math>-calculus and motivated the general study of a differential extension of linear logic.
 
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 <math>\lambda</math>-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 <math>\lambda</math>-calculus and motivated the general study of a differential extension of linear logic.
Line 7: Line 7:
 
== Finiteness spaces ==
 
== Finiteness spaces ==
   
The construction of finiteness spaces follows a well known pattern. It is given by the following notion of orthogonality: <math>a\mathrel \bot a'</math> iff <math>a\cap a'</math> is finite. Then one unrolls familiar definitions, as we do in the following paragraphs.
+
The construction of finiteness spaces follows a well known pattern. It is given by the following notion of orthogonality: <math>a\mathrel \bot a'</math> iff <math>a\cap a'</math> is finite. Then one unrolls [[Orthogonality relation|familiar definitions]], as we do in the following paragraphs.
   
Let <math>A</math> be a set. Denote by <math>\mathfrak P(A)</math> the powerset of <math>A</math> and by <math>\mathfrak P_f(A)</math> the set of all finite subsets of <math>A</math>. Let <math>{\mathfrak F} \subseteq \mathfrak P(A)</math> any set of subsets of <math>A</math>. We define the pre-dual of <math>{\mathfrak F}</math> in <math>A</math> as <math>{\mathfrak F}^{\bot_{A}}=\left\{a'\subseteq A;\ \forall a\in{\mathfrak F},\ a\cap a'\in\mathfrak P_f(A)\right\}</math>. In general we will omit the subscript in the pre-dual notation and just write <math>{\mathfrak F}\orth</math>. For all <math>{\mathfrak F}\subseteq\mathfrak P(A)</math>, we have the following immediate properties: <math>\mathfrak P_f(A) \subseteq {\mathfrak F}\orth</math>; <math>{\mathfrak F}\subseteq {\mathfrak F}\biorth</math>; if <math>{\mathfrak G}\subseteq{\mathfrak F}</math>, <math>{\mathfrak F}\orth\subseteq {\mathfrak G}\orth</math>. By the last two, we get <math>{\mathfrak F}\orth = {\mathfrak F}\triorth</math>. A finiteness structure on <math>A</math> is then a set <math>{\mathfrak F}</math> of subsets of <math>A</math> such that <math>{\mathfrak F}\biorth = {\mathfrak F}</math>.
+
Let <math>A</math> be a set. Denote by <math>\powerset A</math> the powerset of <math>A</math> and by <math>\finpowerset A</math> the set of all finite subsets of <math>A</math>. Let <math>{\mathfrak F} \subseteq \powerset A</math> any set of subsets of <math>A</math>. We define the pre-dual of <math>{\mathfrak F}</math> in <math>A</math> as <math>{\mathfrak F}^{\bot_{A}}=\left\{a'\subseteq A;\ \forall a\in{\mathfrak F},\ a\cap a'\in\finpowerset A\right\}</math>. In general we will omit the subscript in the pre-dual notation and just write <math>{\mathfrak F}\orth</math>. For all <math>{\mathfrak F}\subseteq\powerset A</math>, we have the following immediate properties: <math>\finpowerset A\subseteq {\mathfrak F}\orth</math>; <math>{\mathfrak F}\subseteq {\mathfrak F}\biorth</math>; if <math>{\mathfrak G}\subseteq{\mathfrak F}</math>, <math>{\mathfrak F}\orth\subseteq {\mathfrak G}\orth</math>. By the last two, we get <math>{\mathfrak F}\orth = {\mathfrak F}\triorth</math>. A finiteness structure on <math>A</math> is then a set <math>{\mathfrak F}</math> of subsets of <math>A</math> such that <math>{\mathfrak F}\biorth = {\mathfrak F}</math>.
   
 
A finiteness space is a dependant pair <math>{\mathcal A}=\left(\web{\mathcal A},\mathfrak F\left(\mathcal A\right)\right)</math> where <math>\web {\mathcal A}</math> is the underlying set (the web of <math>{\mathcal A}</math>) and <math>\mathfrak F\left(\mathcal A\right)</math> is a finiteness structure on <math>\web {\mathcal A}</math>. We then write <math>{\mathcal A}\orth</math> for the dual finiteness space: <math>\web {{\mathcal A}\orth} = \web {\mathcal A}</math> and <math>\mathfrak F\left({\mathcal A}\orth\right)=\mathfrak F\left({\mathcal A}\right)^{\bot}</math>. The elements of <math>\mathfrak F\left(\mathcal A\right)</math> are called the finitary subsets of <math>{\mathcal A}</math>.
 
A finiteness space is a dependant pair <math>{\mathcal A}=\left(\web{\mathcal A},\mathfrak F\left(\mathcal A\right)\right)</math> where <math>\web {\mathcal A}</math> is the underlying set (the web of <math>{\mathcal A}</math>) and <math>\mathfrak F\left(\mathcal A\right)</math> is a finiteness structure on <math>\web {\mathcal A}</math>. We then write <math>{\mathcal A}\orth</math> for the dual finiteness space: <math>\web {{\mathcal A}\orth} = \web {\mathcal A}</math> and <math>\mathfrak F\left({\mathcal A}\orth\right)=\mathfrak F\left({\mathcal A}\right)^{\bot}</math>. The elements of <math>\mathfrak F\left(\mathcal A\right)</math> are called the finitary subsets of <math>{\mathcal A}</math>.
   
 
===== Example. =====
 
===== Example. =====
For all set <math>A</math>, <math>(A,\mathfrak P_f(A))</math> is a finiteness space and <math>(A,\mathfrak P_f(A))\orth = (A,\mathfrak P(A))</math>. In particular, each finite set <math>A</math> is the web of exactly one finiteness space: <math>(A,\mathfrak P_f(A))=(A,\mathfrak P(A))</math>. We introduce the following two: <math>\zero = \zero\orth = \left(\emptyset, \{\emptyset\}\right)</math> and <math>\one = \one\orth = \left(\{\emptyset\}, \{\emptyset, \{\emptyset\}\}\right)</math>. We also introduce the finiteness space of natural numbers <math>{\mathcal N}</math> by: <math>|{\mathcal N}|={\mathbf N}</math> and <math>a\in\mathfrak F\left(\mathcal N\right)</math> iff <math>a</math> is finite. We write <math>\mathcal O=\{0\}\in\mathfrak F\left({\mathcal N}\right)</math>.
+
For all set <math>A</math>, <math>(A,\finpowerset A)</math> is a finiteness space and <math>(A,\finpowerset A)\orth = (A,\powerset A)</math>. In particular, each finite set <math>A</math> is the web of exactly one finiteness space: <math>(A,\finpowerset A)=(A,\powerset A)</math>. We introduce the following two: <math>\zero = \zero\orth = \left(\emptyset, \{\emptyset\}\right)</math> and <math>\one = \one\orth = \left(\{\emptyset\}, \{\emptyset, \{\emptyset\}\}\right)</math>. We also introduce the finiteness space of natural numbers <math>{\mathcal N}</math> by: <math>|{\mathcal N}|={\mathbf N}</math> and <math>a\in\mathfrak F\left(\mathcal N\right)</math> iff <math>a</math> is finite. We write <math>\mathcal O=\{0\}\in\mathfrak F\left({\mathcal N}\right)</math>.
   
 
Notice that <math>{\mathfrak F}</math> is a finiteness structure iff it is of the form <math>{\mathfrak G}\orth</math>. It follows that any finiteness structure <math>{\mathfrak F}</math> is downwards closed for inclusion, and closed under finite unions and arbitrary intersections. Notice however that <math>{\mathfrak F}</math> is not closed under directed unions in general: for all <math>k\in{\mathbf N}</math>, write <math>k{\downarrow}=\left\{j;\ j\le k\right\}\in\mathfrak F\left({\mathcal N}\right)</math>; then <math>k{\downarrow}\subseteq k'{\downarrow}</math> as soon as <math>k\le k'</math>, but <math>\bigcup_{k\ge0} k{\downarrow}={\mathbf N}\not\in\mathfrak F\left({\mathcal N}\right)</math>.
 
Notice that <math>{\mathfrak F}</math> is a finiteness structure iff it is of the form <math>{\mathfrak G}\orth</math>. It follows that any finiteness structure <math>{\mathfrak F}</math> is downwards closed for inclusion, and closed under finite unions and arbitrary intersections. Notice however that <math>{\mathfrak F}</math> is not closed under directed unions in general: for all <math>k\in{\mathbf N}</math>, write <math>k{\downarrow}=\left\{j;\ j\le k\right\}\in\mathfrak F\left({\mathcal N}\right)</math>; then <math>k{\downarrow}\subseteq k'{\downarrow}</math> as soon as <math>k\le k'</math>, but <math>\bigcup_{k\ge0} k{\downarrow}={\mathbf N}\not\in\mathfrak F\left({\mathcal N}\right)</math>.
Line 23: Line 23:
   
 
Let <math>f\subseteq A \times B</math> be a relation from <math>A</math> to <math>B</math>, we write <math>f\orth=\left\{(\beta,\alpha);\ (\alpha,\beta)\in f\right\}</math>. For all <math>a\subseteq A</math>, we set <math>f\cdot a = \left\{\beta\in B;\ \exists \alpha\in a,\ (\alpha,\beta)\in f\right\}</math>. If moreover <math>g\subseteq B \times C</math>, we define <math>g \bullet f = \left\{(\alpha,\gamma)\in A\times C;\ \exists \beta\in B,\ (\alpha,\beta)\in f\wedge(\beta,\gamma)\in g\right\}</math>. Then, setting <math>{\mathcal A}\limp{\mathcal B} = \left({\mathcal A}\otimes {\mathcal B}\orth\right)\orth</math>, <math>\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)\subseteq {\web{\mathcal A}\times\web{\mathcal B}}</math> is characterized as follows:
 
Let <math>f\subseteq A \times B</math> be a relation from <math>A</math> to <math>B</math>, we write <math>f\orth=\left\{(\beta,\alpha);\ (\alpha,\beta)\in f\right\}</math>. For all <math>a\subseteq A</math>, we set <math>f\cdot a = \left\{\beta\in B;\ \exists \alpha\in a,\ (\alpha,\beta)\in f\right\}</math>. If moreover <math>g\subseteq B \times C</math>, we define <math>g \bullet f = \left\{(\alpha,\gamma)\in A\times C;\ \exists \beta\in B,\ (\alpha,\beta)\in f\wedge(\beta,\gamma)\in g\right\}</math>. Then, setting <math>{\mathcal A}\limp{\mathcal B} = \left({\mathcal A}\otimes {\mathcal B}\orth\right)\orth</math>, <math>\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)\subseteq {\web{\mathcal A}\times\web{\mathcal B}}</math> is characterized as follows:
\begin{center}
+
\begin{tabular}{r@{\ iff\ }l}
+
<math>
<math>f\in \mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)</math> & <math>\forall a\in \mathfrak F\left({\mathcal A}\right)</math>, <math>f\cdot a \in\mathfrak F\left({\mathcal B}\right)</math> and <math>\forall b\in \mathfrak F\left({\mathcal B}\orth\right)</math>, <math>f\orth\cdot b \in\mathfrak F\left({\mathcal A}\orth\right)</math>
+
\begin{align}
  +
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)
 
\\
 
\\
& <math>\forall a\in \mathfrak F\left({\mathcal A}\right)</math>, <math>f\cdot a \in\mathfrak F\left({\mathcal B}\right)</math> and <math>\forall \beta\in \web{{\mathcal B}}</math>, <math>f\orth\cdot \left\{\beta\right\} \in\mathfrak F\left({\mathcal A}\orth\right)</math>
+
&\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)
 
\\
 
\\
& <math>\forall \alpha\in \web{{\mathcal A}}</math>, <math>f\cdot \left\{\alpha\right\} \in\mathfrak F\left({\mathcal B}\right)</math> and <math>\forall b\in \mathfrak F\left({\mathcal B}\orth\right)</math>, <math>f\orth\cdot b \in\mathfrak F\left({\mathcal A}\orth\right)</math>
+
&\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)
\end{tabular}
+
\end{align}
\end{center}
+
</math>
  +
 
The elements of <math>\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)</math> are called finitary relations from <math>{\mathcal A}</math> to <math>{\mathcal B}</math>. By the previous characterization, the identity relation <math>\mathsf{id}_{{\mathcal A}} = \left\{(\alpha,\alpha);\ \alpha\in\web{{\mathcal A}}\right\}</math> is finitary, and the composition of two finitary relations is also finitary. One can thus define the category <math>\mathbf{Fin}</math> of finiteness spaces and finitary relations: the objects of <math>\mathbf{Fin}</math> are all finiteness spaces, and <math>\mathbf{Fin}({\mathcal A},{\mathcal B})=\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)</math>. Equipped with the tensor product <math>\tens</math>, <math>\mathbf{Fin}</math> is symmetric monoidal, with unit <math>\one</math>; it is monoidal closed by the definition of <math>\limp</math>; it is <math>*</math>-autonomous by the obvious isomorphism between <math>{\mathcal A}\orth</math> and <math>{\mathcal A}\limp\one</math>.
 
The elements of <math>\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)</math> are called finitary relations from <math>{\mathcal A}</math> to <math>{\mathcal B}</math>. By the previous characterization, the identity relation <math>\mathsf{id}_{{\mathcal A}} = \left\{(\alpha,\alpha);\ \alpha\in\web{{\mathcal A}}\right\}</math> is finitary, and the composition of two finitary relations is also finitary. One can thus define the category <math>\mathbf{Fin}</math> of finiteness spaces and finitary relations: the objects of <math>\mathbf{Fin}</math> are all finiteness spaces, and <math>\mathbf{Fin}({\mathcal A},{\mathcal B})=\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)</math>. Equipped with the tensor product <math>\tens</math>, <math>\mathbf{Fin}</math> is symmetric monoidal, with unit <math>\one</math>; it is monoidal closed by the definition of <math>\limp</math>; it is <math>*</math>-autonomous by the obvious isomorphism between <math>{\mathcal A}\orth</math> and <math>{\mathcal A}\limp\one</math>.
 
<!-- By contrast with the purely relational model, it is not compact closed: -->
 
<!-- By contrast with the purely relational model, it is not compact closed: -->
Line 39: Line 39:
 
===== Example. =====
 
===== Example. =====
 
Setting <math>\mathcal{S}=\left\{(k,k+1);\ k\in{\mathbf N}\right\}</math> and <math>\mathcal{P}=\left\{(k+1,k);\ k\in{\mathbf N}\right\}</math>, we have <math>\mathcal{S},\mathcal{P}\in\mathbf{Fin}({\mathcal N},{\mathcal N})</math> and <math>\mathcal{P}\bullet\mathcal{S}=\mathsf{id}_{{\mathcal N}}</math>.
 
Setting <math>\mathcal{S}=\left\{(k,k+1);\ k\in{\mathbf N}\right\}</math> and <math>\mathcal{P}=\left\{(k+1,k);\ k\in{\mathbf N}\right\}</math>, we have <math>\mathcal{S},\mathcal{P}\in\mathbf{Fin}({\mathcal N},{\mathcal N})</math> and <math>\mathcal{P}\bullet\mathcal{S}=\mathsf{id}_{{\mathcal N}}</math>.
 
 
   
 
=== Additives ===
 
=== Additives ===
We now introduce the cartesian structure of <math>\mathbf{Fin}</math>. We define <math>{\mathcal A} \oplus {\mathcal B}</math> by <math>\web {{\mathcal A} \oplus {\mathcal B}} = \web{\mathcal A} \uplus \web{\mathcal B}</math> and <math>\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\}</math> where <math>\uplus</math> denotes the disjoint union of sets: <math>x\uplus y=(\{1\}\times x)\cup(\{2\}\times y)</math>. We have <math>\left({\mathcal A}\oplus {\mathcal B}\right)\orth = {\mathcal A}\orth\oplus{\mathcal B}\orth</math>. The category <math>\mathbf{Fin}</math> is both cartesian and co-cartesian, with <math>\oplus</math> being the product and co-product, and <math>\zero</math> the initial and terminal object. Projections are given by:
+
We now introduce the cartesian structure of <math>\mathbf{Fin}</math>. We define <math>{\mathcal A} \oplus {\mathcal B}</math> by <math>\web {{\mathcal A} \oplus {\mathcal B}} = \web{\mathcal A} \uplus \web{\mathcal B}</math> and <math>\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\}</math> where <math>\uplus</math> denotes the disjoint union of sets: <math>x\uplus y=(\{1\}\times x)\cup(\{2\}\times y)</math>. We have <math>\left({\mathcal A}\oplus {\mathcal B}\right)\orth = {\mathcal A}\orth\oplus{\mathcal B}\orth</math>.<ref>The fact that the additive connectors are identified, i.e. that we obtain a biproduct, is to be related with the enrichment of <math>\mathbf{Fin}</math> over the monoid structure of set union: see {{BibEntry|bibtype=journal|author=Marcello P. Fiore|title=Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic|journal=TLCA 2007}} This identification can also be shown to be a [[isomorphism]] of LL with sums of proofs.</ref>
\begin{eqnarray*}
+
The category <math>\mathbf{Fin}</math> is both cartesian and co-cartesian, with <math>\oplus</math> being the product and co-product, and <math>\zero</math> 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\}
+
  +
<math>
  +
\begin{align}
  +
\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}) \\
 
\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\}
+
\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})
 
\in\mathbf{Fin}({\mathcal A}\oplus{\mathcal B},{\mathcal B})
\end{eqnarray*}
+
\end{align}
  +
</math>
  +
 
and if <math>f\in\mathbf{Fin}({\mathcal C},{\mathcal A})</math> and <math>g\in\mathbf{Fin}({\mathcal C},{\mathcal B})</math>, pairing is given by:
 
and if <math>f\in\mathbf{Fin}({\mathcal C},{\mathcal A})</math> and <math>g\in\mathbf{Fin}({\mathcal C},{\mathcal B})</math>, pairing is given by:
   
Line 64: Line 62:
   
 
=== Exponentials ===
 
=== Exponentials ===
If <math>A</math> is a set, we denote by <math>\mathfrak M_f(A)</math> the set of all finite multisets of
+
If <math>A</math> is a set, we denote by <math>\finmulset A</math> the set of all finite multisets of
elements of <math>A</math>, and if <math>a\subseteq A</math>, we write <math>a^{\oc}=\mathfrak M_f(a)\subseteq\mathfrak M_f(A)</math>.
+
elements of <math>A</math>, and if <math>a\subseteq A</math>, we write <math>a^{\oc}=\finmulset a\subseteq\finmulset A</math>.
If <math>\overline\alpha\in\mathfrak M_f(A)</math>, we denote its support by
+
If <math>\overline\alpha\in\finmulset A</math>, we denote its support by
<math>\mathrm{Support}\left(\overline \alpha\right)\in\mathfrak P_f(A)</math>. For all finiteness space <math>{\mathcal A}</math>, we define
+
<math>\mathrm{Support}\left(\overline \alpha\right)\in\finpowerset A</math>. For all finiteness space <math>{\mathcal A}</math>, we define
<math>\oc {\mathcal A}</math> by: <math>\web{\oc {\mathcal A}}= \mathfrak M_f\left(\web{{\mathcal A}}\right)</math> and <math>\mathfrak F\left(\oc{\mathcal A}\right)=\left\{a^{\oc};\ a\in\mathfrak F\left({\mathcal A}\right)\right\}\biorth</math>.
+
<math>\oc {\mathcal A}</math> by: <math>\web{\oc {\mathcal A}}= \finmulset{\web{{\mathcal A}}}</math> and <math>\mathfrak F\left(\oc{\mathcal A}\right)=\left\{a^{\oc};\ a\in\mathfrak F\left({\mathcal A}\right)\right\}\biorth</math>.
It can be shown that <math>\mathfrak F\left(\oc{\mathcal A}\right) = \left\{\overline a\subseteq\mathfrak M_f\left(\web{{\mathcal A}}\right);\ \bigcup_{\overline\alpha\in \overline a}\mathrm{Support}\left(\overline \alpha\right)\in\mathfrak F\left(\mathcal A\right)\right\}</math>.
+
It can be shown that <math>\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\}</math>.
 
Then, for all <math>f\in\mathbf{Fin}({\mathcal A},{\mathcal B})</math>, we set
 
Then, for all <math>f\in\mathbf{Fin}({\mathcal A},{\mathcal B})</math>, we set
   
Line 93: Line 91:
 
More generally, we have
 
More generally, we have
 
<math>\oc\left({\mathcal A}_1\oplus\cdots\oplus{\mathcal A}_n\right)\cong\oc{\mathcal A}_1\tens\cdots\tens\oc{\mathcal A}_n</math>.
 
<math>\oc\left({\mathcal A}_1\oplus\cdots\oplus{\mathcal A}_n\right)\cong\oc{\mathcal A}_1\tens\cdots\tens\oc{\mathcal A}_n</math>.
  +
  +
==References==
  +
<references />

Latest revision as of 15:32, 30 September 2011

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.

Contents

[edit] 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}.

[edit] Example.

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).


[edit] Multiplicatives

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:


\begin{align}
		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)
\end{align}

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.

[edit] Example.

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}}.

[edit] Additives

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:


\begin{align}
\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}) 
\end{align}

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.

[edit] Example.

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.


[edit] Exponentials

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.

[edit] Example.

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.

[edit] References

  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