Finiteness semantics - Revision history

Pierre-Marie Pédrot: link to orthogonalities

2011-09-30T14:32:46Z

link to orthogonalities

Lionel Vaux: fixed reference

2009-10-12T09:29:25Z

fixed reference

Lionel Vaux: /* Additives */ mention the more general fact that additives are identified in a Mon-enriched model

2009-10-12T09:20:26Z

‎Additives: mention the more general fact that additives are identified in a Mon-enriched model

Lionel Vaux: link to relational semantics

2009-07-06T14:59:38Z

link to relational semantics

Lionel Vaux: Use \powerset, \finpowerset and \finmulset notations

2009-07-06T14:57:33Z

Use \powerset, \finpowerset and \finmulset notations

Olivier Laurent: /* Additives */ formatting

2009-05-25T21:48:57Z

‎Additives: formatting

Olivier Laurent: /* Multiplicatives */ formatting

2009-05-25T21:43:03Z

‎Multiplicatives: formatting

Lionel Vaux: /* Finiteness spaces */ link to closure operators

2009-05-22T18:30:47Z

‎Finiteness spaces: link to closure operators

Lionel Vaux: fixed display math

2009-05-22T18:01:25Z

fixed display math

Lionel Vaux: support for \[ and \]

2009-05-22T17:56:50Z

support for \[ and \]

@@ Line 7: / Line 7: @@
 == 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 [[Phase_semantics#Closure_operators|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>\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>.

@@ Line 43: / Line 43: @@
 === 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>.<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=inproceedings|author=Fiore, Marcello P.|title=Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic|booktitle=TLCA|year=2007|pages=163-177|ee={http://dx.doi.org/10.1007/978-3-540-73228-0_13}|editor={Simona Ronchi Della Rocca}|title={Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings}|publisher={Springer}|series={Lecture Notes in Computer Science}|volume={4583}|isbn={978-3-540-73227-3}}}.</ref>
+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>
 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:
@@ Line 98: / Line 98: @@
 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>.

@@ Line 43: / Line 43: @@
 === 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=inproceedings|author=Fiore, Marcello P.|title=Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic|booktitle=TLCA|year=2007|pages=163-177|ee={http://dx.doi.org/10.1007/978-3-540-73228-0_13}|editor={Simona Ronchi Della Rocca}|title={Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings}|publisher={Springer}|series={Lecture Notes in Computer Science}|volume={4583}|isbn={978-3-540-73227-3}}}.</ref>
 <math>

← Older revision		Revision as of 14:59, 6 July 2009
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 9: / Line 9: @@
 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 [[Phase_semantics#Closure_operators|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>.
 ===== 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>.
@@ Line 68: / Line 68: @@
 === 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

@@ Line 44: / Line 44: @@
 === 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:
 \begin{eqnarray*}
-\lambda_{{\mathcal A},{\mathcal B}}&=&\left\{\left((1,\alpha),\alpha\right);\ \alpha\in\web{\mathcal A}\right\}
+<math>
 \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})
-\end{eqnarray*}
+\end{align}
 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 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:
 \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}
 		\\
-		& <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>.
 <!--  By contrast with the purely relational model, it is not compact closed:  -->
@@ Line 39: / Line 39: @@
 ===== 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>.
 === Additives ===

← Older revision		Revision as of 18:01, 22 May 2009
Line 88:		Line 88:


−	<math>\left\{	+	<math>\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}).</math>
−	\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}).</math>

@@ Line 9: / Line 9: @@
 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.
-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>\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>.
 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>.
@@ Line 16: / Line 16: @@
 	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>.
-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 50: / Line 50: @@
 \in\mathbf{Fin}({\mathcal A}\oplus{\mathcal B},{\mathcal B})
 \end{eqnarray*}
-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: \[\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}).\]
+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:
 The unique morphism from <math>{\mathcal A}</math> to <math>\zero</math> is the empty relation.  The co-cartesian structure is obtained symmetrically.
@@ Line 67: / Line 67: @@
 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>.
 Then, for all <math>f\in\mathbf{Fin}({\mathcal A},{\mathcal B})</math>, 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
@@ Line 78: / Line 78: @@
 <math>\left\{([],\emptyset)\right\}\in\mathbf{Fin}(\oc\zero,\one)</math>
 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}).\]
+A}\tens\oc{\mathcal B}).</math>
 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>.