Finiteness semantics
From LLWiki
(Difference between revisions)
Lionel Vaux (Talk | contribs) (initial import) |
Lionel Vaux (Talk | contribs) (fixed math and sectionning) |
||
| Line 1: | Line 1: | ||
| − | The category $\mathbf{Fin}$ of finiteness spaces and finitary relations was introduced |
+ | 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>. |
| − | 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 |
+ | 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. |
| − | 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 $\lambda$-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 |
||
| − | $\lambda$-calculus and motivated the general study of a |
||
| − | differential extension of linear logic. |
||
| − | It is worth noticing that finiteness spaces can accomodate typed |
+ | It is worth noticing that finiteness spaces can accomodate typed <math>\lambda</math>-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. |
| − | $\lambda$-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. |
||
| − | \section*{Finiteness spaces} |
+ | == Finiteness spaces == |
| − | The construction of finiteness spaces follows a well known pattern. It is |
+ | 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. |
| − | 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 $\mathfrak P(A)$ the powerset of $A$ and by $\mathfrak P_f(A)$ |
+ | 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>. |
| − | the set of all finite subsets of $A$. Let ${\mathfrak f} \subseteq \mathfrak P(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\mathfrak P_f(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\mathfrak P(A)$, we have |
||
| − | the following immediate properties: $\mathfrak P_f(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 |
+ | 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>. |
| − | ${\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}$. |
||
===== Example. ===== |
===== Example. ===== |
||
| − | \label{ex:fs} |
+ | 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 $A$, $(A,\mathfrak P_f(A))$ is a finiteness space |
||
| − | and $(A,\mathfrak P_f(A))\orth = (A,\mathfrak P(A))$. |
||
| − | In particular, each finite set $A$ is the web of exactly one |
||
| − | finiteness space: $(A,\mathfrak P_f(A))=(A,\mathfrak P(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 |
+ | 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>. |
| − | ${\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)$. |
||
| − | \subsection*{Multiplicatives} |
+ | === Multiplicatives === |
| − | For all finiteness spaces ${\mathcal A}$ and ${\mathcal B}$, |
+ | For all finiteness spaces <math>{\mathcal A}</math> and <math>{\mathcal B}</math>, we define <math>{\mathcal A} \tens {\mathcal B}</math> by <math>\web {{\mathcal A} \tens {\mathcal B}} = \web{\mathcal A} \times \web{\mathcal B}</math> and <math>\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</math>. It can be shown that <math>\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\}</math>, where <math>\left.c\right|_l</math> and <math>\left.c\right|_r</math> are the obvious projections. |
| − | 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$, |
+ | 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: |
| − | 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{center} |
\begin{center} |
||
\begin{tabular}{r@{\ iff\ }l} |
\begin{tabular}{r@{\ iff\ }l} |
||
| − | $f\in \mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)$ |
+ | <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> |
| − | & $\forall a\in \mathfrak F\left({\mathcal A}\right)$, $f\cdot a \in\mathfrak F\left({\mathcal B}\right)$ and |
||
| − | $\forall b\in \mathfrak F\left({\mathcal B}\orth\right)$, $f\orth\cdot b \in\mathfrak F\left({\mathcal A}\orth\right)$ |
||
\\ |
\\ |
||
| − | & $\forall a\in \mathfrak F\left({\mathcal A}\right)$, $f\cdot a \in\mathfrak F\left({\mathcal B}\right)$ and |
+ | & <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> |
| − | $\forall \beta\in \web{{\mathcal B}}$, $f\orth\cdot \left\{\beta\right\} \in\mathfrak F\left({\mathcal A}\orth\right)$ |
||
\\ |
\\ |
||
| − | & $\forall \alpha\in \web{{\mathcal A}}$, $f\cdot \left\{\alpha\right\} \in\mathfrak F\left({\mathcal B}\right)$ and |
+ | & <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> |
| − | $\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{tabular} |
||
\end{center} |
\end{center} |
||
| − | The elements of $\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)$ are called finitary relations from |
+ | 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>. |
| − | ${\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$. |
||
<!-- By contrast with the purely relational model, it is not compact closed: --> |
<!-- By contrast with the purely relational model, it is not compact closed: --> |
||
| − | <!-- in general, ${\mathcal A}\limp {\mathcal B}\not\cong{\mathcal A}\orth\tens {\mathcal B}$ (consider ${\mathcal A}$ and --> |
+ | <!-- in general, <math>{\mathcal A}\limp {\mathcal B}\not\cong{\mathcal A}\orth\tens {\mathcal B}</math> (consider <math>{\mathcal A}</math> and --> |
| − | <!-- ${\mathcal B}$ such that $\mathfrak F\left({\mathcal A}\right)=\powerset{\web{{\mathcal A}}}$ and $\web{{\mathcal B}}$ is finite). --> |
+ | <!-- <math>{\mathcal B}</math> such that <math>\mathfrak F\left({\mathcal A}\right)=\powerset{\web{{\mathcal A}}}</math> and <math>\web{{\mathcal B}}</math> is finite). --> |
===== Example. ===== |
===== Example. ===== |
||
| − | Setting $\mathcal{S}=\left\{(k,k+1);\ k\in{\\mathbf N}\right\}$ |
+ | 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>. |
| − | 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}}$. |
||
| − | \subsection*{Additives} |
+ | === Additives === |
| − | We now introduce the cartesian structure of $\mathbf{Fin}$. |
+ | 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 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$. 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{eqnarray*} |
\begin{eqnarray*} |
||
\lambda_{{\mathcal A},{\mathcal B}}&=&\left\{\left((1,\alpha),\alpha\right);\ \alpha\in\web{\mathcal A}\right\} |
\lambda_{{\mathcal A},{\mathcal B}}&=&\left\{\left((1,\alpha),\alpha\right);\ \alpha\in\web{\mathcal A}\right\} |
||
| Line 50: | Line 50: | ||
\in\mathbf{Fin}({\mathcal A}\oplus{\mathcal B},{\mathcal B}) |
\in\mathbf{Fin}({\mathcal A}\oplus{\mathcal B},{\mathcal B}) |
||
\end{eqnarray*} |
\end{eqnarray*} |
||
| − | and if $f\in\mathbf{Fin}({\mathcal C},{\mathcal A})$ and $g\in\mathbf{Fin}({\mathcal C},{\mathcal B})$, 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: \[\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}).\] |
| − | \[\left\langle f,g\right\rangle = |
+ | The unique morphism from <math>{\mathcal A}</math> to <math>\zero</math> is the empty relation. The co-cartesian structure is obtained symmetrically. |
| − | \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. |
||
===== Example. ===== |
===== Example. ===== |
||
| − | Write ${\mathcal O}\orth=\left\{(0,\emptyset)\right\}\in\mathbf{Fin}({\mathcal N},\one)$. |
+ | Write <math>{\mathcal O}\orth=\left\{(0,\emptyset)\right\}\in\mathbf{Fin}({\mathcal N},\one)</math>. Then <math>\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)</math> |
| − | 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. |
is an isomorphism. |
||
| − | <!-- the inverse of which we denote by $\mathcal{P}$. --> |
+ | <!-- the inverse of which we denote by <math>\mathcal{P}</math>. --> |
| − | <!-- Hence $\one\oplus{\mathcal N}\cong {\mathcal N}$. --> |
+ | <!-- Hence <math>\one\oplus{\mathcal N}\cong {\mathcal N}</math>. --> |
| − | \subsection*{Exponentials} |
+ | === Exponentials === |
| − | If $A$ is a set, we denote by $\mathfrak M_f(A)$ the set of all finite multisets of |
+ | If <math>A</math> is a set, we denote by <math>\mathfrak M_f(A)</math> the set of all finite multisets of |
| − | elements of $A$, and if $a\subseteq A$, we write $a^{\oc}=\mathfrak M_f(a)\subseteq\mathfrak M_f(A)$. |
+ | 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>. |
| − | If $\overline\alpha\in\mathfrak M_f(A)$, we denote its support by |
+ | If <math>\overline\alpha\in\mathfrak M_f(A)</math>, we denote its support by |
| − | $\mathrm{Support}\left(\overline \alpha\right)\in\mathfrak P_f(A)$. For all finiteness space ${\mathcal A}$, we define |
+ | <math>\mathrm{Support}\left(\overline \alpha\right)\in\mathfrak P_f(A)</math>. For all finiteness space <math>{\mathcal A}</math>, we define |
| − | $\oc {\mathcal A}$ by: $\web{\oc |
+ | <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>. |
| − | {\mathcal A}}= \mathfrak M_f\left(\web{{\mathcal A}}\right)$ 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 <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 $\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\}$. |
+ | Then, for all <math>f\in\mathbf{Fin}({\mathcal A},{\mathcal B})</math>, we set |
| − | 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}),\] |
| − | \[\oc f =\left\{\left(\left[\alpha_1,\dotsc,\alpha_n\right],\left[\beta_1,\dotsc,\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. |
which defines a functor. |
||
Natural transformations |
Natural transformations |
||
| − | $\mathsf{der}_{{\mathcal A}}=\left\{([\alpha],\alpha);\ \alpha\in |
+ | <math>\mathsf{der}_{{\mathcal A}}=\left\{([\alpha],\alpha);\ \alpha\in \web{{\mathcal A}}\right\}\in\mathbf{Fin}(\oc{\mathcal A},{\mathcal A})</math> and |
| − | \web{{\mathcal A}}\right\}\in\mathbf{Fin}(\oc{\mathcal A},{\mathcal A})$ and |
+ | <math>\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\}</math> make this functor a comonad. |
| − | $\mathsf{digg}_{{\mathcal A}}=\left\{\left(\sum_{i=1}^n\overline\alpha_i,\left[\overline\alpha_1,\dotsc,\overline\alpha_n\right]\right);\ |
||
| − | \forall i,\ \overline\alpha_i\in\web{\oc {\mathcal A}}\right\}$ make this functor a comonad. |
||
===== Example. ===== |
===== Example. ===== |
||
We have isomorphisms |
We have isomorphisms |
||
| − | <!-- $\left\{(n[\emptyset],n);\ n\in{\mathbf N}\right\}\in\mathbf{Fin}(\oc\one,{\mathcal N}\orth)$, --> |
+ | <!-- <math>\left\{(n[\emptyset],n);\ n\in{\mathbf N}\right\}\in\mathbf{Fin}(\oc\one,{\mathcal N}\orth)</math>, --> |
| − | $\left\{([],\emptyset)\right\}\in\mathbf{Fin}(\oc\zero,\one)$ |
+ | <math>\left\{([],\emptyset)\right\}\in\mathbf{Fin}(\oc\zero,\one)</math> |
and |
and |
||
\[\left\{ |
\[\left\{ |
||
| Line 85: | Line 85: | ||
A}\tens\oc{\mathcal B}).\] |
A}\tens\oc{\mathcal B}).\] |
||
More generally, we have |
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$. |
+ | <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>. |
Revision as of 18:52, 22 May 2009
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.
Contents |
Finiteness spaces
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 .
Example.
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 Failed to parse (syntax error): k\in{\\mathbf N}
, write 
; then 
as soon as 
, but Failed to parse (syntax error): \bigcup_{k\ge0} k{\downarrow}={\\mathbf N}\not\in\mathfrak F\left({\mathcal N}\right)
.
Multiplicatives
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:
\begin{center}
\begin{tabular}{r@{\ iff\ }l}
& 
, 
and 
, 
\\
& , and 
, 
\\
& 
, 
and ,
\end{tabular}
\end{center}
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 
.
Example.
Setting Failed to parse (syntax error): \mathcal{S}=\left\{(k,k+1);\ k\in{\\mathbf N}\right\}
and, we have
and
.
Additives
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:
\begin{eqnarray*}
\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{eqnarray*}
and if 
and 
, 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 to is the empty relation. The co-cartesian structure is obtained symmetrically.
Example.
Write 
. Then 
is an isomorphism.
Exponentials
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
\[\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})](/mediawiki/images/math/3/4/a/34a5940f73335627eb8d19f1f3e3371e.png)
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\}](/mediawiki/images/math/a/8/0/a80ae2d100f55cc252774621422d0bcc.png)
make this functor a comonad.
Example.
We have isomorphisms
![\left\{([],\emptyset)\right\}\in\mathbf{Fin}(\oc\zero,\one)](/mediawiki/images/math/1/9/e/19eeee98d64e829cd46b47bc879a348e.png)
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
.
