Finiteness semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(initial import)
 
m (link to orthogonalities)
 
(11 intermediate revisions by 2 users not shown)
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 [[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>.
−
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 [[Orthogonality relation|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>\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>.
−
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,\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>.
−
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 =
 +
<math>
−
\left\{\beta\in B;\ \exists \alpha\in a,\ (\alpha,\beta)\in f\right\}$.
 +
\begin{align}
−
If moreover $g\subseteq B \times C$, we define
 +
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)
−
$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{tabular}{r@{\ iff\ }l}
  
−
$f\in \mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)$
  
−
& $\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
+
&\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)
−
$\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
+
&\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)
−
$\forall b\in \mathfrak F\left({\mathcal B}\orth\right)$, $f\orth\cdot b \in\mathfrak F\left({\mathcal A}\orth\right)$
 +
\end{align}
−
\end{tabular}
 +
</math>
−
\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}}$.
  
   
  +
=== 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=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:
   
−
+
<math>
−
\subsection*{Additives}
 +
\begin{align}
−
We now introduce the cartesian structure of $\mathbf{Fin}$.
+
\lambda_{{\mathcal A},{\mathcal B}}&=\left\{\left((1,\alpha),\alpha\right);\ \alpha\in\web{\mathcal A}\right\}
−
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*}
  
−
\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}
−
and if $f\in\mathbf{Fin}({\mathcal C},{\mathcal A})$ and $g\in\mathbf{Fin}({\mathcal C},{\mathcal B})$, pairing is given by:
 +
</math>
−
\[\left\langle f,g\right\rangle =
+
−
\left\{\left(\gamma,(1,\alpha)\right);\ (\gamma,\alpha)\in f\right\}
 +
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:
−
\cup
+
−
\left\{\left(\gamma,(2,\beta)\right);\ (\gamma,\beta)\in g\right\}
+
<math>\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}).</math>
−
\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.
 +
The unique morphism from <math>{\mathcal A}</math> to <math>\zero</math> 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>. -->
  +
  +
=== Exponentials ===
  +
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}=\finmulset a\subseteq\finmulset A</math>.
  +
If <math>\overline\alpha\in\finmulset A</math>, we denote its support by
  +
<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}}= \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\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
  +
  +
  +
<math>\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}),</math>
  +
   
−
\subsection*{Exponentials}
  
−
If $A$ is a set, we denote by $\mathfrak M_f(A)$ 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)$.
  
−
If $\overline\alpha\in\mathfrak M_f(A)$, we denote its support by
  
−
$\mathrm{Support}\left(\overline \alpha\right)\in\mathfrak P_f(A)$. For all finiteness space ${\mathcal A}$, we define
  
−
$\oc {\mathcal A}$ by: $\web{\oc
  
−
{\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 $\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 $f\in\mathbf{Fin}({\mathcal A},{\mathcal B})$, we set
  
−
\[\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(\overline\alpha_l+\overline\beta_r,\left(\overline\alpha,\overline\beta\right)\right);\
 +
−
(\overline\alpha_l,\overline\alpha)\in\oc\lambda_{{\mathcal A},{\mathcal
 +
<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>
−
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
  
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>.
  +
  +
==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.
Retrieved from "http://140.77.166.78/mediawiki/index.php?title=Finiteness_semantics&oldid=518"
Personal tools