Coherence Spaces and Uniform Continuity

TL;DR

This paper introduces a model of classical linear logic based on coherence spaces with totality, showing that uniform spaces can be represented and that uniformly continuous functions correspond to total linear maps within this framework.

Contribution

It establishes a novel connection between coherence spaces with totality and uniform spaces, providing a new categorical model where uniform continuity is characterized by linear maps.

Findings

Uniform spaces can be represented by coherence spaces with totality.

Uniformly continuous functions correspond to total linear maps in the model.

The model applies to separable, metrizable uniform spaces like the real line.

Abstract

In this paper, we consider a model of classical linear logic based on coherence spaces endowed with a notion of totality. If we restrict ourselves to total objects, each coherence space can be regarded as a uniform space and each linear map as a uniformly continuous function. The linear exponential comonad then assigns to each uniform space X the finest uniform space !X compatible with X. By a standard realizability construction, it is possible to consider a theory of representations in our model. Each (separable, metrizable) uniform space, such as the real line, can then be represented by (a partial surjecive map from) a coherence space with totality. The following holds under certain mild conditions: a function between uniform spaces X and Y is uniformly continuous if and only if it is realized by a total linear map between the coherence spaces representing X and Y.

Equations

$$\mathbf{Tych}$$

$$\mbox{$f:\mathbb{X}\to\mathbb{Y}_{\mathsf{ut}}$ is continuous}\quad\Longleftrightarrow\quad\mbox{$f:\mathbb{X}_{\mathsf{fine}}\to\mathbb{Y}$ is uniformly continuous}\ .$$

$$\mathbf{Stab}$$

$${\mathcal{T}}_{\mathbf{X}}=\{b\in \mathbf{X}:a\subseteq b\text{mbox}forsomea\in {\mathcal{T}}_{\mathbf{X}}^{\circ }\}=({\mathcal{T}}_{\mathbf{X}}^{\circ }{)}^{\perp \perp }.$$

$$\begin{gathered} \neg (x\text{shortstack}⌢ \\ [-.3em]⌣y)⟺⟨x⟩\cap ⟨y⟩=\varnothing ;\neg (a\text{shortstack}⌢ \\ [-.3em]⌣b)⟺⟨a⟩\cap ⟨b⟩=\varnothing \end{gathered}$$

$$\mathbf{Tych}$$

$$\mathbf{X}$$

$${\wedge }_i{\mathfrak{c}}_i:=\{\{x_1,\dots ,x_n\}\in \mathbf{X}:x_i\in {\mathfrak{c}}_i(1\le i\le n)\}.$$

$$\mathfrak{B}$$

$$\hat{\kappa }(a_0)=\hat{\theta }(b_0)(a_0)=b_0⟹|\kappa -\theta (b_0)|<a_0\otimes \mathfrak{b}⟹|F(\kappa )-F(\theta (b_0))|<\mathfrak{c}.$$

$$[\rho_{{\boldsymbol{X}}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}](\kappa):=f\quad\Longleftrightarrow\quad f:S\longrightarrow T\mbox{ is realized by $\widehat{\kappa}:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$.}$$

Full text

1 Introduction

Since the inception of Scott’s domain theory in 1960’s, topology and continuity have been playing a prominent role in denotational understanding of logic and computation. On the other hand, uniformity and uniform continuity have not yet been explored so much. The purpose of this paper is to bring them into the setting of denotational semantics by relating them to another denotational model: coherence spaces and linear maps. Our principal idea is that linear maps should be uniformly continuous, not just in analysis, but also in denotational semantics. The following situation, typical for computable real functions (in the sense of [Ko91]), illustrates our idea.

Example 1

Imagine that each real number $x\in\mathbb{R}$ is presented by a rational Cauchy sequence $(x_{n})_{n\in\mathbb{N}}$ with $|x-x_{n}|\leq 2^{-n}$. Let $f:\mathbb{R}\to\mathbb{R}$ be a computable function which is uniformly continuous. Then there must be a function $\mu:\mathbb{N}\to\mathbb{N}$, called a modulus of continuity, such that an approximation of $f(x)$ with precision $2^{-m}$ can be computed from a single rational number $x_{\mu(m)}$, no matter where $x$ is located on the real line. Thus one has to access the sequence $(x_{n})$ (regarded as an oracle) only once.

On the other hand, if $f:\mathbb{R}\to\mathbb{R}$ is not uniformly continuous, it admits no uniform modulus of continuity. Hence one has to accsess $(x_{n})$ at least twice to obtain an approximation of $f(x)$, once for figuring out the location of $x$ and thus obtaining a local modulus of continuity $\mu$ around $x$, once for getting the approximate value $x_{\mu(m)}$.

Thus there is a difference in query complexity between uniformly continuous and non-uniformly continuous functions. This leads us to an inspiration that linear maps, whose query complexity is 1, should be somehow related to uniformly continuous functions. To materialize this inspiration, we work with coherence spaces with totality.

Coherence spaces, introduced by Girard [Gi87], are domains which are simply presented as undirected reflexive graphs. It was originally introduced as a denotational semantics for System F, and later led to the discovery of linear logic. One of the notable features of coherence spaces is that there are two kinds of morphisms coexisting: stable and linear maps.

Totalities, which originate in domain theory (eg. [Gi86, No90, Be93]), are often attached to coherence spaces (eg. [KN97]). Specifically, a coherence space with totality in our sense is a coherence space ${\boldsymbol{X}}$ equipped with a set $\mathcal{T}_{\boldsymbol{X}}$ of cliques called a totality, so that for any $a\in\mathcal{T}_{\boldsymbol{X}}$ there exists $\mathfrak{c}\in\mathcal{T}_{{\boldsymbol{X}}^{\perp}}$ with $a\cap\mathfrak{c}\neq\emptyset$, and vice versa. Totalities are usually employed to restrict objects and morphisms to total ones, while we use them to impose a uniform structure on ${\boldsymbol{X}}$: when restricted to “strict” ones (to be defined later), a totality $\mathcal{T}_{\boldsymbol{X}}$ can be seen as a set of ideal points of a uniform space $\mathbb{X}$, while a co-totality $\mathcal{T}_{{\boldsymbol{X}}^{\perp}}$ as the uniform sub-basis for $\mathbb{X}$. Moreover, this allows us to prove that every “total” linear map $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$ is uniformly continuous (though not vice versa).

The category of coherence spaces with totality and total linear maps forms a model of classical linear logic. In this setting, the linear exponential comonad $!$ admits an interesting interpretation: it assigns to each uniform space ${\boldsymbol{X}}$ the finest uniform space $\,!\,{\boldsymbol{X}}$ compatible with ${\boldsymbol{X}}$.

We then apply our framework to computable analysis, where people study computability over various continuous and analytic structures (such as the real numbers, metric spaces and topological spaces). An essential prerequisite for this is that each abstract space should be concretely represented. While traditional approaches employ Baire spaces [KW85, We00, BHW08] or Scott-Ershov domains [Bl97, ES99, SHT08], we here consider representations based on coherence spaces.

This program has been already launched by [MT16], where we have suitably defined admissible representations based on coherence spaces (by importing various results from the type-two theory of effectivity). The principal result there is as follows. Let $\mathbb{X}$ and $\mathbb{Y}$ be topological spaces admissibly represented by (partial surjections from) coherence spaces ${\boldsymbol{X}}$ and ${\boldsymbol{Y}}$ (eg. the real line $\mathbb{R}$ is admissibly represented by a coherence space ${\boldsymbol{R}}$ in Example 2). Then a function $f:\mathbb{X}\to\mathbb{Y}$ is sequentially continuous if and only if $f$ is realized (i.e., tracked) by a stable map $F:{\boldsymbol{X}}\longrightarrow_{st}{\boldsymbol{Y}}$.

In passing, we have also observed in [MT16] a curious phenomenon: when restricted to $\mathbb{R}$, a function $f:\mathbb{R}\to\mathbb{R}$ is uniformly continuous if and only if $f$ is realized by a linear map $F:{\boldsymbol{R}}\longrightarrow_{lin}{\boldsymbol{R}}$. Thus linearity in coherence spaces corresponds to uniform continuity of real functions. While we did not have any rationale or generalization, at that time, we now have a better understanding of uniform continuity in terms of coherence spaces. As a result, we are able to systematically generalize the above result to separable metrizable uniform spaces.

Plan of the paper.

We quickly review uniform spaces in §2.1 and coherence spaces in §2.2. We then introduce in §3.1 the notion of coherence space with totality, total and strict cliques, and study the categorical structure. In §3.2, we explore the uniformities induced by co-totalities. In §4, we give an application of our model to computable analysis. We conclude in §5 with some future work.

2 Preliminaries

2.1 Uniform Spaces

We review some concepts regarding uniform spaces. See [Is64, Wi70] for details.

A cover of a set $X$ is a family of subsets $\mathcal{U}\subseteq\mathcal{P}(X)$ such that $\bigcup\mathcal{U}=X$. Let $\mathcal{U}$ and $\mathcal{V}$ be covers of $X$. We say that $\mathcal{U}$ refines $\mathcal{V}$, written $\mathcal{U}\preceq\mathcal{V}$, if for every $U\in\mathcal{U}$ there exists $V\in\mathcal{V}$ with $U\subseteq V$. We then have the meet (greatest lower bound) of $\mathcal{U}$ and $\mathcal{V}$ defined as \{U\cap V:\mbox{U\in\mathcal{U}$and$V\in\mathcal{V}}\}, denoted by $\mathcal{U}\wedge\mathcal{V}$.

When $\mathcal{U}$ is a cover and $A$ is a subset of the set $X$, the star $\mathrm{st}(A;\mathcal{U})$ is defined as $\bigcup\{U\in\mathcal{U}:A\cap U\neq\emptyset\}$. Given any cover $\mathcal{U}$ of $X$, its star closure is defined as $\mathcal{U}^{*}:=\{\mathrm{st}(U;\mathcal{U}):U\in\mathcal{U}\}$, which is also a cover of $X$ and is refined by $\mathcal{U}$. We say that a cover $\mathcal{U}$ star-refines $\mathcal{V}$ if $\mathcal{U}^{*}\preceq\mathcal{V}$.

Definition 2.1

A family $\mu$ of covers of $X$ is called a Hausdorff uniformity if it satisfies the following:

• (U1)

If $\mathcal{U},\mathcal{V}\in\mu$, then $\mathcal{U}\wedge\mathcal{V}\in\mu$;

• (U2)

If $\mathcal{U}\in\mu$ and $\mathcal{U}\preceq\mathcal{V}$, then $\mathcal{V}\in\mu$;

• (U3)

For every $\mathcal{U}\in\mu$, there exists $\mathcal{V}\in\mu$ which star-refines $\mathcal{U}$;

• (U4)

Given any two distinct points $x,y\in X$, there exists $\mathcal{U}\in\mu$ such that no $U\in\mathcal{U}$ contains both $x$ and $y$ (the Hausdorff condition).

Throughout this paper we always assume the Hausdorff condition. A (Hausdorff) uniform space is a pair $\mathbb{X}=(X,\mu_{X})$, a set $X$ endowed with a (Hausdorff) uniformity. Given any cover $\mathcal{U}\in\mu_{X}$ and any points $x,y\in X$, we write $|x-y|<\mathcal{U}$ if $x,y\in U$ for some $U\in\mathcal{U}$. The condition (U4) can be restated as follows: if $|x-y|<\mathcal{U}$ for every $\mathcal{U}\in\mu_{X}$ then $x=y$.

Let $\mathbb{X}=(X,\mu_{X})$ and $\mathbb{Y}=(Y,\mu_{Y})$ be uniform spaces. A uniformly continuous function from $\mathbb{X}$ to $\mathbb{Y}$ is a function $f:X\to Y$ satisfying that for any $\mathcal{V}\in\mu_{Y}$ there exists $\mathcal{U}\in\mu_{X}$ with $|x-y|<\mathcal{U}\ \Longrightarrow\ |f(x)-f(y)|<\mathcal{V}$ for every $x,y\in X$. A function $f:\mathbb{X}\to\mathbb{Y}$ is called uniform quotient if it is surjective and for every function $g:\mathbb{Y}\to\mathbb{Z}$ to a uniform space $\mathbb{Z}$, $g$ is uniformly continuous iff $g\circ f:\mathbb{X}\to\mathbb{Z}$ is.

A (uniform) basis of a uniformity $\mu$ is a subfamily $\beta\subseteq\mu$ such that for every $\mathcal{U}\in\mu$ there exists $\mathcal{V}\in\beta$ with $\mathcal{V}\preceq\mathcal{U}$. A (uniform) sub-basis of a uniformity $\mu$ is a subfamily $\sigma\subseteq\mu$ such that the finite meets of members of $\sigma$ form a basis: for every $\mathcal{U}\in\mu$ there exist finitely many $\mathcal{V}_{1},\ldots,\mathcal{V}_{n}\in\sigma$ with $\mathcal{V}_{1}\wedge\cdots\wedge\mathcal{V}_{n}\preceq\mathcal{U}$. Notice that if a family of covers satisfies the conditions (U2)-(U4) (resp. (U3)-(U4)), it uniquely generates a uniformity as a basis (resp. sub-basis).

For instance, every metric space is in fact a uniform space. A uniformity on a metric space $\mathbb{X}$ is generated by a countable basis \mathcal{U}_{n}:=\{\mathcal{B}(x;2^{-n}):\mbox{x\in\mathbb{X}}\} ($n=1,2,\ldots$), where $\mathcal{B}(x;2^{-n})$ is the open ball of center $x$ and radius $2^{-n}$.

On the other hand, every uniform space $\mathbb{X}=(X,\mu_{X})$ can be equipped with a topological structure, called the uniform topology. A set $O\subseteq X$ is open with respect to the uniform topology iff for every $p\in O$ there exists $\mathcal{U}\in\mu_{X}$ such that $\mathrm{st}(\{p\},\mathcal{U})\subseteq O$. We will denote by $\tau_{\mathsf{ut}}(\mu)$ the uniform topology induced by a uniformity $\mu$. Given any uniformity $\mu$ on $X$, one can choose a basis $\beta$ consisting of open covers.

It is easy to see that uniform continuity implies topological continuity: if a function $f:(X,\mu_{X})\to(Y,\mu_{Y})$ is uniformly continuous, then it is continuous as a function $f:(X,\tau_{\mathsf{ut}}(\mu_{X}))\to(Y,\tau_{\mathsf{ut}}(\mu_{Y}))$.

We say that a uniformity $\mu$ on $X$ is compatible with a topology $\tau$ if $\tau=\tau_{\mathsf{ut}}(\mu)$. A topological space $\mathbb{X}=(X,\tau)$ is said to be uniformizable if there exists a uniformity $\mu$ on $X$ compatible with $\tau$. It is known that a topological space is uniformizable if and only it is Tychonoff. For a metrizable space, the induced uniformity defined above is indeed compatible with the metric topology. In general, a uniformity is induced by a metric if and only if it has a countable basis.

Every Tychonoff (i.e. uniformizable) space $\mathbb{X}=(X,\tau)$ can be equipped with the finest uniformity $\mu_{\mathrm{fine}}$ which contains all of the uniformities compatible with $\tau$. A fine uniform space is a uniform space endowed with the finest uniformity (compatible with its uniform topology). For a Tychonoff space $\mathbb{X}=(X,\tau_{X})$ we denote by $\mathbb{X}_{\mathrm{fine}}=(X,\mu_{\mathrm{fine}})$ the fine uniform space compatible with $\tau_{X}$.

The finest uniformity can be characterized as follows. Let $\mathbf{Tych}$ be the category of Tychonoff spaces and continuous maps, and $\mathbf{Unif}$ be the category of uniform spaces and uniformly continuous maps. The fine functor $F:\mathbf{Tych}\longrightarrow\mathbf{Unif}$, which assigns to each Tychonoff space $\mathbb{X}$ the fine uniform space $\mathbb{X}_{\mathrm{fine}}$, is left adjoint to the topologizing functor $G:\mathbf{Unif}\longrightarrow\mathbf{Tych}$, which assigns to each uniform space $\mathbb{Y}$ the topological space $\mathbb{Y}_{\mathsf{ut}}$ endowed with the uniform topology:

[TABLE]

Thus, for every Tychonoff space $\mathbb{X}$ and uniform space $\mathbb{Y}$,

[TABLE]

2.2 Coherence Spaces

We here recall some basics of coherence spaces. See [Gi87, Me09] for further information.

Definition 2.2

*A coherence space {\boldsymbol{X}}=(X,\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,) consists of a set $X$ of tokens and a reflexive symmetric relation  

$\frown$

[-.3em]$\smile$

  on $X$, called coherence.*

Throughout this paper, we assume that every token set $X$ is countable. This assumption is quite reasonable in practice, since we would like to think of tokens as computational objects (see [As90] for the study on computability over coherence spaces).

A clique of ${\boldsymbol{X}}$ is a set of pairwise coherent tokens in $X$. By abuse of notation, we denote by ${\boldsymbol{X}}$ the set of all cliques of the coherence space ${\boldsymbol{X}}$. We also use the notations ${\boldsymbol{X}}_{\mathsf{fin}}$ and ${\boldsymbol{X}}_{\mathsf{max}}$ for the sets of all finite cliques and maximal cliques, respectively.

Given tokens $x,y\in X$, we write x\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,y (strict coherence) if x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,y and $x\neq y$. Notice that coherence and strict coherence are mutually definable from each other. The coherence relation  

$\frown$

[-.3em]$\smile$

  on the token set $X$ is naturally extended to ${\boldsymbol{X}}$ as: a\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,b\iff a\cup b\in{\boldsymbol{X}} ($a,b\in{\boldsymbol{X}}$). This is equivalent to say that any token in $a$ is coherent with any token in $b$.

An anti-clique of ${\boldsymbol{X}}$ is a set of pairwise incoherent tokens in X, that is, a subset $\mathfrak{a}\subseteq X$ such that \neg(x\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,y) for every $x,y\in\mathfrak{a}$. We will use the symbol  

$\smile$

[-.3em]$\frown$

  for incoherence: x\,\raisebox{-1.99997pt}{\shortstack{\smile$\\ [-.3em]$\frown}}\,y\iff\neg(x\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,y). Alternatively, an anti-clique of ${\boldsymbol{X}}$ is a clique of the dual coherence space {\boldsymbol{X}}^{\perp}:=(X,\,\raisebox{-1.99997pt}{\shortstack{\smile$\\ [-.3em]$\frown}}\,).

It is known that the set ${\boldsymbol{X}}$ of cliques ordered by inclusion $\subseteq$ is in fact a Scott domain, whose compact elements are finite cliques of ${\boldsymbol{X}}$. Thus the Scott topology on ${\boldsymbol{X}}$ is generated by $\{\langle a\rangle:a\in{\boldsymbol{X}}_{\mathsf{fin}}\}$ as a basis, where $\langle a\rangle$ is an upper set defined by \langle a\rangle:=\big{\{}b\in{\boldsymbol{X}}:a\subseteq b\big{\}}. We will denote by $\tau_{\mathrm{Sco}}$ this topology on ${\boldsymbol{X}}$.

Given a subset $\mathcal{A}\subseteq{\boldsymbol{X}}$, we also write $\tau_{\mathrm{Sco}}$ for the induced subspace topology on $\mathcal{A}$. Note that ${\boldsymbol{X}}$ is a $T_{0}$-space, and is countably-based due to the assumption that the token set $X$ is countable. Moreover, $({\boldsymbol{X}}_{\mathsf{max}},\tau_{\mathrm{Sco}})$ is Hausdorff.

Coherence spaces have a sufficiently rich structure to represent abstract spaces. Let us begin with a coherence space for the real line $\mathbb{R}$:

Example 2 (coherence space for real numbers)

Let $\mathbb{D}:=\mathbb{Z}\times\mathbb{N}$, where each pair $(m,n)\in\mathbb{D}$ is identified with a dyadic rational number $m/2^{n}$. We use the following notations for $x=(m,n)\in\mathbb{D}$: $\mathsf{den}(x):=n$; $\mathbb{D}_{n}:=\{x\in\mathbb{D}\mid\mathsf{den}(x)=n\}$ for each $n\in\mathbb{N}$; and $[x]:=[(m-1)/2^{n};(m+1)/2^{n}]$.

Hence $n=\mathsf{den}(x)$ denotes the exponent of the denominator of $x$, and $[x]$ denotes the compact interval of $\mathbb{R}$ with center $x$ and width $2^{-(n-1)}$.

Let $\mathbf{R}$ be a coherence space (\mathbb{D},\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,) defined by x\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,y iff $\mathsf{den}(x)\neq\mathsf{den}(y)$ and $[x]\cap[y]\neq\emptyset$. The latter condition immediately implies the inequality $|x-y|\leq 2^{-\mathsf{den}(x)}+2^{-\mathsf{den}(y)}$, hence each maximal clique $a\in\mathbf{R}_{\mathsf{max}}$ corresponds to a rapidly-converging Cauchy sequence $\{x_{n}:n\in\mathbb{N}\}$ such that $x_{n}\in\mathbb{D}_{n}$ for each $n\in\mathbb{N}$ and $|x_{n}-x_{m}|\leq 2^{-n}+2^{-m}$ for every $n,m\in\mathbb{N}$.

We then have a mapping $\rho_{{\boldsymbol{R}}}:\mathbf{R}_{\mathsf{max}}\to\mathbb{R}$ defined by $\rho_{{\boldsymbol{R}}}(a):=\lim_{n\to\infty}x_{n}$.

Definition 2.3** (stable and linear maps)**

Let ${\boldsymbol{X}}$ and ${\boldsymbol{Y}}$ be coherence spaces. A function $F:{\boldsymbol{X}}\to{\boldsymbol{Y}}$ is said to be stable, written $F:{\boldsymbol{X}}\longrightarrow_{st}{\boldsymbol{Y}}$, if it is Scott-continuous and a\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,b\Longrightarrow F(a\cap b)=F(a)\cap F(b) for any cliques $a,b\in{\boldsymbol{X}}$.

A function $F:{\boldsymbol{X}}\to{\boldsymbol{Y}}$ is said to be linear, written $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$, if it satisfies that $a=\sum_{i\in I}a_{i}\Longrightarrow F(a)=\sum_{i\in I}F(a_{i})$, for any clique $a\in{\boldsymbol{X}}$ and any family of cliques $\{a_{i}\}_{i\in I}\subseteq{\boldsymbol{X}}$. Here $\sum$ means the disjoint union of cliques.

It is easy to see that linearity implies stability.

There are alternative definitions. Given a function $F:{\boldsymbol{X}}\longrightarrow{\boldsymbol{Y}}$, call $(a,y)\in{\boldsymbol{X}}_{\mathsf{fin}}\times Y$ a minimal pair of $F$ if $F(a)\ni y$ and there is no proper subset $a^{\prime}\subsetneq a$ such that $F(a^{\prime})\ni y$. Denote by $\mathsf{tr}(F)$ the set of all minimal pairs, called the trace of $F$. Now, $F$ is a stable map iff it is $\subseteq$-monotone and satisfies that: if $F(a)\ni y$, there is a unique $a_{0}\subseteq a$ such that $(a_{0},y)\in\mathsf{tr}(F)$.

If $F$ is furthermore linear, preservation of disjoint unions ensures that the finite part $a_{0}$ must be a singleton. Thus $F$ is a linear map iff it is $\subseteq$-monotone and satisfies that: if $F(a)\ni y$, there is a unique $x\in a$ such that $(\{x\},y)\in\mathsf{tr}(F)$. By abuse of notation, we simply write $\mathsf{tr}(F)$ for the set $\{(x,y)|(\{x\},y)\in\mathsf{tr}(F)\}$ if $F$ is supposed to be linear.

Below are some typical constructions of coherence spaces. Let {\boldsymbol{X}}_{i}=(X_{i},\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,_{i}) be a coherence space for $i=1,2$. We define:

• •

$\mathbf{1}:=\bot=(\{\bullet\},\{(\bullet,\bullet)\})$.

• •

{\boldsymbol{X}}_{1}\otimes{\boldsymbol{X}}_{2}:=(X_{1}\times X_{2},\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,), where (z,x)\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,(w,y) holds iff both z\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,_{1}w and x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,_{2}y.

• •

{\boldsymbol{X}}_{1}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{X}}_{2}:=(X_{1}\times X_{2},\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,), where (z,x)\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,(w,y) holds iff z\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,_{1}w implies x\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,_{2}y.

• •

!\,{\boldsymbol{X}}_{1}:=(({\boldsymbol{X}}_{1})_{\mathsf{fin}},\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,), where a\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,b holds iff a\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,_{1}b.

We omit the definitions of additives ($\,\&\,$ and $\top$). It easily follows that ${\boldsymbol{X}}^{\perp}\simeq{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}\perp$.

A notable feature of coherence spaces is that they have two closed structures: the category $\mathbf{Stab}$ of coherence spaces and stable maps is cartesian closed; while the category $\mathbf{Lin}$ of coherence spaces and linear maps equipped with $(\mathbf{1},\otimes,\mathbin{-\mkern-3.0mu\circ},\bot)$ is *-autonomous. Moreover, the co-Kleisli category of the linear exponential comonad $!$ on $\mathbf{Lin}$ is isomorphic to $\mathbf{Stab}$ in such a way that a stable map $F:{\boldsymbol{X}}\longrightarrow_{st}{\boldsymbol{Y}}$ can be identified with a linear map $G:\,!\,{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$ so that $\mathsf{tr}(F)=\mathsf{tr}(G)\subseteq{\boldsymbol{X}}_{\mathsf{fin}}\times Y$. This leads to a linear-non-linear adjunction:

[TABLE]

The purpose of this paper is to establish a connection between the two adjunctions (1) and (2), which will be done in §3.2.

We do not describe the categorical structures in detail, but let us just mention the following. Given any linear map $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$, we have $\mathsf{tr}(F)\in{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}$. Conversely, given any clique $\kappa\in{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}$, the induced linear map $\widehat{\kappa}:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$ is defined by \widehat{\kappa}(a):=\{y\in Y:\mbox{(x,y)\in\kappa$for some$x\in a}\}.

3 Uniform Structures on Coherence Spaces

In this section, we introduce a notion of (co-)totality on coherence spaces and observe that co-totality induces a uniform structure on the set of total cliques.

3.1 Coherence Spaces with Totality

Let ${\boldsymbol{X}}$ be a coherence space. For any clique $a\in{\boldsymbol{X}}$ and any anti-clique $\mathfrak{c}\in{\boldsymbol{X}}^{\perp}$, $a\cap\mathfrak{c}$ is either empty or a singleton. If the latter is the case, we write $a\perp\mathfrak{c}$.

For any subset $\mathcal{A}\subseteq{\boldsymbol{X}}$, we write $\mathcal{A}^{\perp}$ for the set \{\mathfrak{c}\in{\boldsymbol{X}}^{\perp}:\mbox{\forall a\in\mathcal{A}$.$a\perp\mathfrak{c}}\} of anti-cliques of ${\boldsymbol{X}}$. One can immediately observe the following: (i) $\mathcal{A}\subseteq\mathcal{A}^{\perp\perp}\subseteq{\boldsymbol{X}}$; (ii) $\mathcal{B}\subseteq\mathcal{A}$ implies $\mathcal{A}^{\perp}\subseteq\mathcal{B}^{\perp}$; and (iii) $\mathcal{A}^{\perp}=\mathcal{A}^{\perp\perp\perp}$. As a consequence, $\mathcal{A}=\mathcal{A}^{\perp\perp}$ iff $\mathcal{A}=\mathcal{B}^{\perp}$ for some $\mathcal{B}\subseteq{\boldsymbol{X}}^{\perp}$.

Definition 3.1** (coherence spaces with totality)**

A coherence space with totality is a coherence space ${\boldsymbol{X}}$ endowed with a set $\mathcal{T}_{\boldsymbol{X}}\subseteq{\boldsymbol{X}}$ such that $\mathcal{T}_{\boldsymbol{X}}=\mathcal{T}_{\boldsymbol{X}}^{\perp\perp}$, called a totality. Cliques in $\mathcal{T}_{{\boldsymbol{X}}}$ are said to be total.

It is clear that a totality $\mathcal{T}_{\boldsymbol{X}}$ is upward-closed with respect to $\subseteq$, and is closed under compatible intersections: $a,b\in\mathcal{T}_{\boldsymbol{X}}$ with a\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,b implies $a\cap b\in\mathcal{T}_{\boldsymbol{X}}$. As a consequence, every total clique $a\in\mathcal{T}_{\boldsymbol{X}}$ is associated with a unique minimal total clique $a^{\circ}:=\bigcap\{b\in\mathcal{T}_{\boldsymbol{X}}:b\subseteq a\}\in\mathcal{T}_{\boldsymbol{X}}$. Such a total clique is called strict (or material in the sense of ludics). We write $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ for the set of strict total cliques of ${\boldsymbol{X}}$. We have

[TABLE]

Thus defining a totality is essentially equivalent to defining a strict totality. Notice that $a\in\mathcal{T}_{\boldsymbol{X}}$ iff for every $\mathfrak{c}\in\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$, $a\perp\mathfrak{c}$. In particular, $a\in\mathcal{T}_{\boldsymbol{X}}^{\circ}$ iff for every $\mathfrak{c}\in(\mathcal{T}_{\boldsymbol{X}}^{\perp})^{\circ}$ there exists $x\in a$ such that $x\in\mathfrak{c}$ and dually, for every $x\in a$ there exists $\mathfrak{c}\in(\mathcal{T}_{{\boldsymbol{X}}}^{\perp})^{\circ}$ such that $x\in\mathfrak{c}$.

Our use of totality is inspired by Kristiansen and Normann [KN97], although they use a set of anti-cliques of $!{\boldsymbol{X}}$ as totality and they do not consider strictness and bi-orthogonality. Similar constructions are abundant in the literature, eg., totality spaces by Loader [Loa94] and finiteness spaces by Ehrhard [Ehr05].

Example 3

Consider the coherence space {\boldsymbol{R}}=(\mathbb{D},\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,) for real numbers defined in Example 2. Then $\mathcal{T}_{\boldsymbol{R}}:={\boldsymbol{R}}_{\mathsf{max}}$ is a totality on ${\boldsymbol{R}}$: it is easy to see that $\mathcal{T}_{{\boldsymbol{R}}}^{\perp}=\{\mathcal{D}_{n}:n\in\mathbb{N}\}$, hence $\mathcal{T}_{{\boldsymbol{R}}}^{\perp\perp}={\boldsymbol{R}}_{\mathsf{max}}=\mathcal{T}_{\boldsymbol{R}}$. Moreover, $\mathcal{T}_{{\boldsymbol{R}}}^{\circ}={\boldsymbol{R}}_{\mathsf{max}}$ since $a^{\circ}\subseteq a$ and $a^{\circ}\in{\boldsymbol{R}}_{\mathsf{max}}$ imply $a^{\circ}=a$.

Example 4

The idea of Example 2 can be generalized to a more general class. Let $\mathbb{X}=(X,\mu)$ be a uniform space with a countable basis $\beta=\{\mathcal{U}_{n}\}_{n\in\mathbb{N}}$ consisting of countable covers. A metrization theorem states that such a uniform space must be separable metrizable (see [Ke75] for instance).

Let {\boldsymbol{B}}_{\mathbb{X}}=(B,\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,) be a coherence space defined as $B=\coprod_{n\in\mathbb{N}}\mathcal{U}_{n}$ and (n,U)\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,(m,V) iff $n\neq m$ and $U\cap V\neq\emptyset$, where $\coprod_{n\in\mathbb{N}}\mathcal{U}_{n}$ means the coproduct \{(n,U):\mbox{n\in\mathbb{N}$,$U\in\mathcal{U}_{n}}\}. Each $a\in({\boldsymbol{B}}_{\mathbb{X}})_{\mathsf{max}}$ corresponds to a sequence of members of uniform covers: $a=\{U_{n}\}_{n\in\mathbb{N}}$ such that $U_{n}\in\mathcal{U}_{n}$ for each $n\in\mathbb{N}$ and $U_{n}\cap U_{m}\neq\emptyset$ for every $n,m\in\mathbb{N}$. By the Hausdorff property, it indicates at most one point in $\mathbb{X}$.

The separable metrizable space $\mathbb{X}$ is represented by a partial map $\delta_{\mathbb{X}}:\subseteq{\boldsymbol{B}}_{\mathbb{X}}\to\mathbb{X}$ defined by $\delta_{\mathbb{X}}(a):=p\quad\Longleftrightarrow\quad p\in\bigcap_{n\in\mathbb{N}}U_{n}$, for every $p\in\mathbb{X}$ and $a=\{U_{n}:n\in\mathbb{N}\}\in({\boldsymbol{B}}_{\mathbb{X}})_{\mathsf{max}}$. Let us define a totality by $\mathcal{T}_{{\boldsymbol{B}}_{\mathbb{X}}}:=\mathsf{dom}(\delta_{\mathbb{X}})^{\perp\perp}$.

Notice that we do not have $\mathsf{dom}(\delta_{\mathbb{X}})=\mathsf{dom}(\delta_{\mathbb{X}})^{\perp\perp}$ in general, even though $\{\mathcal{U}_{n}:n\in\mathbb{N}\}\subseteq\mathcal{T}_{{\boldsymbol{B}}_{\mathbb{X}}}^{\perp}$, since $\mathsf{dom}(\delta_{\mathbb{X}})^{\perp\perp}=({\boldsymbol{B}}_{\mathbb{X}})_{\mathsf{max}}$. To make $\mathsf{dom}(\delta_{\mathbb{X}})$ itself a totality, we have to assume that $\mathbb{X}$ is complete (every Cauchy sequence must be converging).

All constructions of coherence spaces are extended with totality in a rather canonical way. Let {\boldsymbol{X}}=(X,\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,_{\boldsymbol{X}}) and {\boldsymbol{Y}}=(Y,\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,_{\boldsymbol{Y}}) be coherence spaces, and $\mathcal{T}_{\boldsymbol{X}}\subseteq{\boldsymbol{X}}$ and $\mathcal{T}_{\boldsymbol{Y}}\subseteq{\boldsymbol{Y}}$ be totalities of ${\boldsymbol{X}}$ and ${\boldsymbol{Y}}$, respectively. Define:

• •

$\mathcal{T}_{{\boldsymbol{X}}^{\perp}}:=\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$; $\mathcal{T}_{\mathbf{1}}:=\mathbf{1}_{\mathsf{max}}$.

• •

$\mathcal{T}_{{\boldsymbol{X}}\otimes{\boldsymbol{Y}}}:=(\mathcal{T}_{{\boldsymbol{X}}}\otimes\mathcal{T}_{{\boldsymbol{Y}}})^{\perp\perp}$, where $a\otimes b:=\{(x,y):x\in a,y\in b\}$ for $a\in{\boldsymbol{X}}$ and $b\in{\boldsymbol{Y}}$, and $\mathcal{T}_{{\boldsymbol{X}}}\otimes\mathcal{T}_{{\boldsymbol{Y}}}$ is pointwise defined.

• •

\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}:=\{\kappa\in({\boldsymbol{X}}_{1}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{X}}_{2}):\mbox{\widehat{\kappa}[\mathcal{T}{\boldsymbol{X}}]\subseteq\mathcal{T}{\boldsymbol{Y}}}.

• •

$\mathcal{T}_{\,!\,{\boldsymbol{X}}}:=(\,!\,\mathcal{T}_{{\boldsymbol{X}}})^{\perp\perp}$, where $\,!\,a:=\{a_{0}\in{\boldsymbol{X}}:a_{0}\subseteq_{\mathsf{fin}}a\}$ for $a\in{\boldsymbol{X}}$, and $!\,\mathcal{T}_{{\boldsymbol{X}}}$ is pointwise defined.

The connectives $\otimes$ and $!$ admit “internal completeness” in the following sense.

Proposition 1

$(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp\perp\circ}=\mathcal{T}_{{\boldsymbol{X}}}^{\circ}\otimes\mathcal{T}_{{\boldsymbol{Y}}}^{\circ}$* holds whenever totalities $\mathcal{T}_{{\boldsymbol{X}}}$, $\mathcal{T}_{{\boldsymbol{Y}}}$, $\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$ and $\mathcal{T}_{{\boldsymbol{Y}}}^{\perp}$ are all nonempty. $(\,!\,\mathcal{T}_{{\boldsymbol{Z}}})^{\perp\perp\circ}=\,!\,(\mathcal{T}_{{\boldsymbol{Z}}}^{\circ})$ holds for an arbitrary totality $\mathcal{T}_{{\boldsymbol{Z}}}$.*

A proof is given in Appendix.

Let us now turn to the morphisms.

Definition 3.2

A linear map $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$ is called total if $\mathsf{tr}(F)\in\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}$, or equivalently if $F$ preserves totality: $F[\mathcal{T}_{\boldsymbol{X}}]\subseteq\mathcal{T}_{\boldsymbol{Y}}$.

A stable map $F:{\boldsymbol{X}}\longrightarrow_{st}{\boldsymbol{Y}}$ is total if so is the corresponding linear map $G:\,!\,{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$ given in §2.2.

Denote by $\mathbf{Lin}_{\mathsf{Tot}}$ the category of coherence spaces with totality and total linear maps. It turns out to be a model of classical linear logic (CLL):

Theorem 3.3

The category $\mathbf{Lin}_{\mathsf{Tot}}$ is a model of classical linear logic (i.e., a $\ast$-autonomous category with finite (co)products and a linear exponential (co)monad).

This is due to Theorem 5.14 in [HS03]. In fact, our construction of $\mathbf{Lin}_{\mathsf{Tot}}$ is essentially following the idea of tight orthogonality category $\mathbf{T}(\mathbf{Lin})$ induced by the orthogonality relation $\perp$, which can be shown to be a symmetric stable orthogonality in $\mathbf{Lin}$.

The category $\mathbf{Stab}_{\mathsf{Tot}}$ of coherence spaces with totality and total stable maps, is trivially the co-Kleisli category of the linear exponential comonad $\,!\,$ and hence is cartesian closed.

3.2 Uniformities induced by co-Totality

We shall next show that each coherence space with totality can be equipped with a uniform structure. Our claim can be summarized as follows. Given a coherence space ${\boldsymbol{X}}$ with totality $\mathcal{T}_{\boldsymbol{X}}$, the set of strict total cliques $\mathcal{T}_{\boldsymbol{X}}^{\circ}$ is endowed with both a topology and a uniformity:

the totality $\mathcal{T}_{\boldsymbol{X}}^{\circ}$ is a set of points endowed with a Hausdorff topology $\tau_{\mathrm{Sco}}$ ,

while

the co-totality $(\mathcal{T}_{\boldsymbol{X}}^{\perp})^{\circ}$ is a uniform sub-basis.

Moreover, the co-totality $(\mathcal{T}_{\,!\,{\boldsymbol{X}}}^{\perp})^{\circ}$ on $\,!\,{\boldsymbol{X}}$ is a uniform basis, which induces the finest uniformity on $\mathcal{T}_{\boldsymbol{X}}^{\circ}$.

Recall that each finite clique $a\in{\boldsymbol{X}}_{\mathsf{fin}}$ generates the upper set $\langle a\rangle:=\{b\in{\boldsymbol{X}}:b\supseteq a\}$ in such a way that incoherence corresponds to disjointness:

[TABLE]

for every $x,y\in X$ and $a,b\in{\boldsymbol{X}}_{\mathsf{fin}}$, where $\langle x\rangle$ stands for $\langle\{x\}\rangle$ by abuse of notation. Let us write $\langle x\rangle^{\circ}:=\langle x\rangle\cap\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ and $\langle a\rangle^{\circ}:=\langle a\rangle\cap\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$.

We call each $\mathfrak{c}\in(\mathcal{T}_{{\boldsymbol{X}}}^{\perp})^{\circ}$ a uni-cover of $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$. It can be seen as a disjoint cover $\{\langle x\rangle^{\circ}:x\in\mathfrak{c}\}$ of $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$, since $\mathfrak{c}$ being total precisely means that every $a\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ is contained in $\langle x\rangle^{\circ}$ for some $x\in\mathfrak{c}$. Thus $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}=\sum_{x\in\mathfrak{c}}\langle x\rangle^{\circ}$. Moreover, $\mathfrak{c}$ being strict means that $\langle x\rangle^{\circ}$ is nonempty for every $x\in\mathfrak{c}$. That is, restricting $\mathfrak{c}\in\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$ to $\mathfrak{c}^{\circ}\in(\mathcal{T}_{{\boldsymbol{X}}}^{\perp})^{\circ}$ amounts to removing all empty $\langle x\rangle^{\circ}$ from the disjoint cover $\{\langle x\rangle^{\circ}:x\in\mathfrak{c}\}$.

On the other hand, each $\mathfrak{C}\in(\mathcal{T}_{!{\boldsymbol{X}}}^{\perp})^{\circ}$ is called an unbounded-cover of $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$. It is also identified with a disjoint cover $\{\langle a\rangle^{\circ}:a\in\mathfrak{C}\}$ of $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$, consisting of nonempty upper sets, so that $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}=\sum_{a\in\mathfrak{C}}\langle a\rangle^{\circ}$.

To emphasize the uniformity aspect, we will use the notations $\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}:=(\mathcal{T}_{{\boldsymbol{X}}}^{\perp})^{\circ}$ and $\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}:=(\mathcal{T}_{\,!\,{\boldsymbol{X}}}^{\perp})^{\circ}$. Each uni-cover can be considered as an unbounded-cover consisting of singletons: $\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}\subseteq\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}$ by $\mathfrak{c}\in\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}\mapsto\{\{x\}:x\in\mathfrak{c}\}\in\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}$.

The families $\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}$ and $\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}$ indeed generate uniformities on $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$:

Proposition 2

$(\mathcal{T}_{\boldsymbol{X}}^{\circ},\beta_{{\boldsymbol{X}}}^{\mathrm{ub}})$* satisfies axioms (U1), (U3) and (U4), while $(\mathcal{T}_{\boldsymbol{X}}^{\circ},\sigma_{{\boldsymbol{X}}}^{\mathrm{b}})$ satisfies (U3) and (U4) in Definition 2.1.*

Proof

(U1) Given $\mathfrak{A},\mathfrak{B}\in\beta^{\mathrm{ub}}_{\boldsymbol{X}}$, let \mathfrak{A}\wedge\mathfrak{B}:=\{a\cup b\ :\ \mbox{a\in\mathfrak{A}$,$b\in\mathfrak{B}$and$a,\raisebox{-1.99997pt}{\shortstack{$\frown$\ [-.3em]$\smile$}},b}\}^{\circ}. It is indeed the meet of $\mathfrak{A}$ and $\mathfrak{B}$, and belongs to $\beta^{\mathrm{ub}}_{\boldsymbol{X}}=(!\mathcal{T}_{\boldsymbol{X}}^{\circ\bot})^{\circ}$. In fact, given $!c\in!\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$, there are $a\in\mathfrak{A}$ and $b\in\mathfrak{B}$ such that $a\in!c$ and $b\in!c$. Hence $a\cup b\in!c\cap(\mathfrak{A}\wedge\mathfrak{B})$.

(U3) In general, we have $\mathrm{st}(U,{\mathfrak{C}})=\bigcup\{V\in\mathfrak{C}:U\cap V\neq\emptyset\}=U$ for any disjoint cover ${\mathfrak{C}}$ of $\mathcal{T}_{\boldsymbol{X}}^{\circ}$ and $U\in\mathfrak{C}$. Hence each $\mathfrak{A}\in\beta^{\mathrm{ub}}_{\boldsymbol{X}}$, which is disjoint, star-refines itself.

(U4) Assume that $a,b\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ with $a\neq b$. Then there are $x\in a\backslash b$ and $\mathfrak{c}\in\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}=(\mathcal{T}_{{\boldsymbol{X}}}^{\perp})^{\circ}$ such that $x\in\mathfrak{c}$ by strictness of $a$. As $a\in\langle x\rangle^{\circ}$, $b\not\in\langle x\rangle^{\circ}$ and $\mathfrak{c}$ is a disjoint cover, this witnesses the Hausdorff property for $\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}$ (so for $\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}$ too).

Consequently, $\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}$, as basis, generates a uniformity $\mu_{{\boldsymbol{X}}}^{\mathrm{ub}}$, called the unbounded uniformity, while $\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}$, as sub-basis, generates another uniformity $\mu_{{\boldsymbol{X}}}^{\mathrm{b}}\subseteq\mu_{{\boldsymbol{X}}}^{\mathrm{ub}}$, called the bounded uniformity. The index ${\boldsymbol{X}}$ will be often dropped if it is obvious from the context.

As one may have noticed, the uniformities satisfy axiom (U3) for a rather trivial reason. Nevertheless, viewing coherence spaces with totality as uniform spaces will be essential to establish our main theorem (Theorem 4.8).

Unlike $\beta^{\mathrm{ub}}_{\boldsymbol{X}}$, the set $\sigma^{\mathrm{b}}_{\boldsymbol{X}}$ is not closed under finite meets. To make it closed, we have to extend it to another set $\beta^{\mathrm{b}}_{\boldsymbol{X}}\subseteq\beta^{\mathrm{ub}}_{\boldsymbol{X}}$ which consists of all finite meets of uni-covers: $\mathfrak{c}_{1}\wedge\cdots\wedge\mathfrak{c}_{m}:=\{\{x_{1},\dots,x_{m}\}\in{\boldsymbol{X}}:x_{i}\in\mathfrak{c}_{i}\ (1\leq i\leq m)\}^{\circ}$. Notice that $\mathfrak{c}_{1}\wedge\cdots\wedge\mathfrak{c}_{m}$ consists of cliques of size at most $m$. That is why $\mu_{{\boldsymbol{X}}}^{\mathrm{b}}$ is called bounded.

Although $\mu_{{\boldsymbol{X}}}^{\mathrm{b}}$ and $\mu_{{\boldsymbol{X}}}^{\mathrm{ub}}$ are different as uniformities, they do induce the same uniform topology.

Proposition 3

The (un)bounded uniformity on $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ is compatible with the Scott topology restricted to $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$. That is, $\tau_{\mathsf{ut}}(\mu^{\mathrm{b}})=\tau_{\mathsf{ut}}(\mu^{\mathrm{ub}})=\tau_{\mathrm{Sco}}$.

Proof

By definition a set $U\subseteq\mathcal{T}_{\boldsymbol{X}}^{\circ}$ is open with respect to $\tau_{\mathsf{ut}}(\mu^{\mathrm{ub}})$ iff for every $a\in U$ there exists $\mathfrak{A}\in\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}$ such that $\mathrm{st}(\{a\};\mathfrak{A})\subseteq U$ (see §2.1). Due to disjointness of $\mathfrak{A}$, however, $\mathrm{st}(\{a\};\mathfrak{A})$ just amounts to $\langle a_{0}\rangle^{\circ}$, where $a_{0}$ is the unique clique in $\mathfrak{A}$ such that $a\in\langle a_{0}\rangle^{\circ}$. Moreover, any $a_{0}\in{\boldsymbol{X}}_{\mathsf{fin}}$ with $\langle a_{0}\rangle^{\circ}\neq\emptyset$ is contained in some $\mathfrak{A}\in\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}$ by Lemma 12 in §0.A.2. All together, $U$ is open iff for every $a\in U$ there exists $a_{0}\in{\boldsymbol{X}}_{\mathsf{fin}}$ such that $a\in\langle a_{0}\rangle^{\circ}$ iff $U$ is open with respect to $\tau_{\mathrm{Sco}}$.

The same reasoning works for $\tau_{\mathsf{ut}}(\mu^{\mathrm{b}})$ too.

The unbounded uniformity $\mu^{\mathrm{ub}}$ is hence compatible with, and finer than the bounded uniformity $\mu^{\mathrm{b}}$. We can furthermore show that it is the finest uniformity on $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$. The omitted proofs are found in §0.A.2.

Theorem 3.4

$(\mathcal{T}_{{\boldsymbol{X}}}^{\circ},\mu^{\mathrm{ub}}_{\boldsymbol{X}})$* is a fine uniform space.*

Due to the internal completeness (Proposition 1), we have a bijection $\mathcal{T}_{{\boldsymbol{X}}}^{\circ}\simeq\mathcal{T}_{\,!\,{\boldsymbol{X}}}^{\circ}$ defined by $a\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}\leftrightarrow\,!\,a\in\mathcal{T}_{\,!\,{\boldsymbol{X}}}^{\circ}$. Notice also that $\beta^{\mathrm{ub}}_{{\boldsymbol{X}}}=(\mathcal{T}_{!{\boldsymbol{X}}}^{\perp})^{\circ}=\sigma^{\mathrm{b}}_{!{\boldsymbol{X}}}$ and fine uniformity is preserved under uniform homeomorphisms. These facts together allow us to prove:

Corollary 1

There is a uniform homeomorphism $(\mathcal{T}_{{\boldsymbol{X}}}^{\circ},\mu_{{\boldsymbol{X}}}^{\mathrm{ub}})\simeq(\mathcal{T}_{\,!\,{\boldsymbol{X}}}^{\circ},\mu_{\,!\,{\boldsymbol{X}}}^{\mathrm{b}})$. As a consequence, $(\mathcal{T}_{\,!\,{\boldsymbol{X}}}^{\circ},\mu^{\mathrm{b}}_{\,!\,{\boldsymbol{X}}})$ is a fine uniform space.

We are now ready to establish uniform continuity of linear maps.

Theorem 3.5

A total linear map $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$ is strongly uniformly continuous: for any $\mathfrak{b}\in\sigma_{{\boldsymbol{Y}}}^{\mathrm{b}}$ there exists $\mathfrak{a}\in\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}$ such that $|a-b|<\mathfrak{a}\ \Rightarrow\ |F(a)-F(b)|<\mathfrak{b}$ for every $a,b\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$. As a consequence:

• (i)

Every total linear map $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$ is uniformly continuous w.r.t. the bounded uniformities.

• (ii)

Every total stable map $F:{\boldsymbol{X}}\longrightarrow_{st}{\boldsymbol{Y}}$ is topologically continuous w.r.t. the uniform topologies.

Proof

Note that the transpose $F^{\bot}:{\boldsymbol{Y}}^{\bot}\longrightarrow_{lin}{\boldsymbol{X}}^{\bot}$, defined by $x\in F^{\bot}(\{y\})\Leftrightarrow F(\{x\})\ni y$ for every $x\in X$ and $y\in Y$, is also total linear since $\mathbf{Lin}_{\mathsf{Tot}}$ is *-autonomous. By linearity, any $x\in\mathfrak{a}$ is uniquely associated with $y\in\mathfrak{b}$ such that $x\in F^{\bot}(\{y\})$ (i.e., $F(\{x\})\ni y$). From this, one can immediately observe that $a,b\in\langle x\rangle^{\circ}$ with $x\in\mathfrak{a}$ implies $F(a),F(b)\in\langle y\rangle^{\circ}$ with $y\in\mathfrak{b}$.

We thus obtain a functor $J:\mathbf{Lin}_{\mathsf{Tot}}\to\mathbf{Unif}$ which sends a coherence space with totality $({\boldsymbol{X}},\mathcal{T}_{\boldsymbol{X}})$ to the uniform space $(\mathcal{T}_{\boldsymbol{X}}^{\circ},\mu^{\mathrm{b}})$ and a total linear map to the corresponding uniformly continuous map which is shown in the above theorem. There is also a functor $I:\mathbf{Stab}_{\mathsf{Tot}}\to\mathbf{Tych}$ sending $({\boldsymbol{X}},\mathcal{T}_{\boldsymbol{X}})$ to the Tychonoff space $(\mathcal{T}_{\boldsymbol{X}}^{\circ},\tau_{\mathrm{Sco}})$ and a total stable map to the corresponding continuous map. We now have the following diagram, in which the two squares commute (up to natural isomorphisms):

[TABLE]

In addition, the pair of functors $\langle I,J\rangle$ preserves an adjunction: it is a pseudo-map of adjunctions in the sense of Jacobs [Ja99] (see Appendix in §0.A.3).

This combines (1) and (2), as we have planned.

4 Coherent Representations

In this section, we exhibit a representation model based on coherence spaces and show that there exist good representations based on which linear maps well express uniformly continuous functions.

4.1 Representations as a Realizability Model

We represent abstract spaces, largely following the mainstreams of computable analysis: Baire-space representations in type-two theory of effectivity (TTE) [KW85, We00, BHW08], and domain representations [Bl97, ES99, SHT08]. In both theories, computations are tracked by continuous maps over their base spaces (the Baire space $\mathbb{B}=\mathbb{N}^{\omega}$ for TTE or Scott domains for domain representations). Similarly we assign “coherent” representations to topological spaces, and track computations by stable maps, just as in Examples 2 and 4.

Let us formally give a definition:

Definition 4.1

Let $S$ be an arbitrary set. A tuple $({\boldsymbol{X}},\rho,S)$ is called a representation of $S$ if ${\boldsymbol{X}}$ is a coherence space and $\rho:\subseteq{\boldsymbol{X}}\to S$ is a partial surjective function. Below, we write ${\boldsymbol{X}}\stackrel{{\scriptstyle\rho}}{{\longrightarrow}}S$, or simply $\rho$ for $({\boldsymbol{X}},\rho,S)$.

Representations enable us to express abstract functions as stable maps:

Definition 4.2** (stable realizability)**

Let ${\boldsymbol{X}}\stackrel{{\scriptstyle\rho_{\boldsymbol{X}}}}{{\longrightarrow}}S$ and ${\boldsymbol{Y}}\stackrel{{\scriptstyle\rho_{\boldsymbol{Y}}}}{{\longrightarrow}}T$ be representations. A function $f:S\to T$ is stably realizable with respect to $\rho_{\boldsymbol{X}}$ and $\rho_{\boldsymbol{Y}}$ if it is tracked by a stable map $F:{\boldsymbol{X}}\longrightarrow_{st}{\boldsymbol{Y}}$. That is, $F$ makes the following diagram commute:

[TABLE]

We denote by $\mathbf{StabRep}$ the category of coherent representations and stably realizable functions.

With the help of Longley’s theory of applicative morphisms [Lon94], one can compare $\mathbf{StabRep}$ with other models of representations. By simply mimicking Bauer’s approach [Ba00, Ba02], we obtain an applicative retraction between coherent representations and TTE-representations. As a consequence, we can embed TTE into the theory of coherent representations:

Theorem 4.3

Let $\mathbf{TTERep}$ be a category which embodies TTE: the category of TTE-representations and continuously realizable functions. Then $\mathbf{TTERep}$ is equivalent to a full coreflexive subcategory of $\mathbf{StabRep}$.

For details on the realizability theory, we refer to [Lon94]. We also refer to the Ph.D thesis of Bauer [Ba00], in which the relationship between the theory of (TTE and domain) representations and realizability theory is deeply studied.

In [MT16], we have defined a full subcategory $\mathbf{SpStabRep}$ of $\mathbf{StabRep}$ which is equivalent to $\mathbf{TTERep}$, and introduced a concept of admissibility of representations in $\mathbf{SpStabRep}$. The main result of [MT16] is as follows:

Theorem 4.4 ([MT16])

Let $\mathbb{X}$ and $\mathbb{Y}$ be topological spaces represented by admissible representations ${\boldsymbol{X}}\stackrel{{\scriptstyle\rho_{\boldsymbol{X}}}}{{\longrightarrow}}\mathbb{X}$ and ${\boldsymbol{Y}}\stackrel{{\scriptstyle\rho_{\boldsymbol{Y}}}}{{\longrightarrow}}\mathbb{Y}$ in $\mathbf{SpStabRep}$. A function $f:\mathbb{X}\longrightarrow\mathbb{Y}$ is stably realizable if and only if it is sequentially continuous, that is, it preserves the limit of any convergent sequence: $x_{n}\rightarrow x\ \Rightarrow\ f(x_{n})\rightarrow f(x)$.

For instance, the coherent representation ${\boldsymbol{R}}\stackrel{{\scriptstyle\rho_{\boldsymbol{R}}}}{{\longrightarrow}}\mathbb{R}$ defined in Example 2 belongs to $\mathbf{SpStabRep}$ and is admissible. Consequently, a function $f:\mathbb{R}\to\mathbb{R}$ is stably realizable w.r.t. $\rho_{\boldsymbol{R}}$ iff it is continuous. This equivalence can be generalized to any countably-based $T_{0}$-space (and more generally, any qcb-space in the sense of [Si03]) as shown in [We00, Sc02].

Notice that given any topological space $\mathbb{X}$, its admissible representations are “interchangeable”: if ${\boldsymbol{X}}_{0}\stackrel{{\scriptstyle\rho_{0}}}{{\longrightarrow}}\mathbb{X}$ and ${\boldsymbol{X}}_{1}\stackrel{{\scriptstyle\rho_{1}}}{{\longrightarrow}}\mathbb{X}$ are adimissible, then the identity map $\mathsf{id}:\mathbb{X}\longrightarrow\mathbb{X}$ is realized by stable maps $F:{\boldsymbol{X}}_{0}\longrightarrow_{st}{\boldsymbol{X}}_{1}$ and $G:{\boldsymbol{X}}_{1}\longrightarrow_{st}{\boldsymbol{X}}_{0}$ which reduce each representation to another one.

4.2 Linear Realizability for Separable Metrizable Spaces

On the other hand, we have found in [MT16] a linear variant of the above equivalence between stable realizability and continuity: a function $f:\mathbb{R}\to\mathbb{R}$ is linearly realizable iff it is uniformly continuous. We below try to generalize this correspondence to a class of separable metrizable spaces, based on standard representations defined in Example 4.

Definition 4.5** (linear realizability)**

Let ${\boldsymbol{X}}\stackrel{{\scriptstyle\rho_{\boldsymbol{X}}}}{{\longrightarrow}}S$ and ${\boldsymbol{Y}}\stackrel{{\scriptstyle\rho_{\boldsymbol{Y}}}}{{\longrightarrow}}T$ be representations. A function $f:S\to T$ is linearly realizable with respect to $\rho_{\boldsymbol{X}}$ and $\rho_{\boldsymbol{Y}}$ if it is tracked by a linear map $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$. That is, $F$ makes the diagram (4) commute.

We denote by $\mathbf{LinRep}$ the category of coherent representations and linearly realizable functions.

Given suitable totalities, a linear map $F$ which tracks $f$ turns out to be uniformly continuous. First recall that for any set $\mathcal{A}\subseteq{\boldsymbol{X}}$ of a coherence space ${\boldsymbol{X}}$, the set $\mathcal{A}^{\perp\perp}$ is a totality on ${\boldsymbol{X}}$, hence is endowed with a bounded uniformity (observed in §3). Here is an extension lemma for the double negation totalities:

Lemma 1

Let $\mathcal{A}\subseteq{\boldsymbol{X}}$ and $\mathcal{B}\subseteq{\boldsymbol{Y}}$ be arbitrary (non-empty) sets of cliques. If $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$ satisfies $F[\mathcal{A}]\subseteq\mathcal{B}$ then $F$ is indeed total: $F[\mathcal{A}^{\perp\perp}]\subseteq\mathcal{B}^{\perp\perp}$.

Given any coherent representation ${\boldsymbol{X}}\stackrel{{\scriptstyle\delta_{\boldsymbol{X}}}}{{\longrightarrow}}S$, let us endow ${\boldsymbol{X}}$ with a totality $\mathcal{T}_{\boldsymbol{X}}:=\mathsf{dom}(\delta_{\boldsymbol{X}})^{\perp\perp}$. From the above lemma, we obtain that $f:S\to T$ is linearly realizable if and only if it is tracked by a total linear map $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{Y}}$. So one can say that a linearly realizable function is in fact a “totally linearly realizable” function. Recall that $\mathsf{dom}(\rho_{{\boldsymbol{R}}})^{\perp\perp}=\mathsf{dom}(\rho_{{\boldsymbol{R}}})^{\perp\perp\circ}={\boldsymbol{R}}_{\mathsf{max}}$ and $\mathsf{dom}(\delta_{\mathbb{X}})^{\perp\perp}=\mathsf{dom}(\delta_{\mathbb{X}})^{\perp\perp\circ}=({\boldsymbol{B}}_{\mathbb{X}})_{\mathsf{max}}$.

Theorem 4.6

$\mathbf{LinRep}$* is a linear category (i.e., a symmetric monoidal closed category with a linear exponential comonad).*

Proof Sketch.    Recall that a linear combinatory algebra (LCA) [AHS02] is a linear variant of well-known partial combinatory algebras (PCA). It is shown in Theorem 2.1 of [AL05] that the PER category $\mathbf{PER}(\mathbb{A})$ over an LCA $\mathbb{A}$ is a linear category.

We can naturally define an LCA $\mathbb{C}oh$ such that $\mathbf{LinRep}\simeq\mathbf{PER}(\mathbb{C}oh)$. Indeed, coherence spaces have linear type structures and there also exists a universal type, from which we obtain an untyped LCA $\mathbb{C}oh$ by a linear variant of the Lietz-Streicher theorem [LS02].

Consequently, the category $\mathbf{LinRep}\simeq\mathbf{PER}(\mathbb{C}oh)$ is a linear category.   From the categorical structure of $\mathbf{PER}(\mathbb{C}oh)$, one can naturally construct various coherent representations, which are explicitly given in §0.A.7. We leave to future work to relate the co-Kleisli category $\mathbf{LinRep}_{\,!\,}$ and $\mathbf{StabRep}$.

Then one can see that a standard representation ${\boldsymbol{B}}_{\mathbb{X}}\stackrel{{\scriptstyle\delta_{\mathbb{X}}}}{{\longrightarrow}}\mathbb{X}$ of a separable metrizable space $\mathbb{X}$ is topologically “good” for linear realizability, like admissible representations for stable realizability. It is shown in §0.A.5 that a standard representation of $\mathbb{X}$ does not depend on the chocie of a uniform basis, up to linear isomorphisms. Moreover, we can show that:

Theorem 4.7

Let $\mathbb{X}$ and $\mathbb{Y}$ be separable metrizable spaces with standard representations ${\boldsymbol{B}}_{\mathbb{X}}\stackrel{{\scriptstyle\delta_{\mathbb{X}}}}{{\longrightarrow}}\mathbb{X}$ and ${\boldsymbol{B}}_{\mathbb{Y}}\stackrel{{\scriptstyle\delta_{\mathbb{Y}}}}{{\longrightarrow}}\mathbb{Y}$. Then every uniformly continuous function $f:\mathbb{X}\to\mathbb{Y}$ is linearly realizable.

See §0.A.5 for a proof.

For the other direction, we need a kind of connectedness in addition so that uni-covers of the coherence space exactly generates the uniformity on the represented space. A uniform space $\mathbb{X}=(X,\mu_{X})$ is chain-connected (or sometimes called uniformly connected) if for any two points $p,q\in X$ and every uniform cover $\mathcal{U}\in\mu_{X}$, there exist finitely many $U_{1},\ldots U_{n}\in\mathcal{U}$ such that $p\in U_{1}$, $U_{i}\cap U_{i+1}\neq\emptyset$ for every $i<n$, and $U_{n}\ni q$.

Theorem 4.8

Let $\mathbb{X}$ and $\mathbb{Y}$ be separable metrizable spaces represented by the standard representations. Provided that $\mathbb{X}$ is chain-connected, a function $f:\mathbb{X}\to\mathbb{Y}$ is linearly realizable iff it is uniformly continuous.

Proof

The “if”-direction is due to Theorem 4.7. We shall show the “only-if” direction. As noted above, if $f$ is linearly realizable, there exists a total linear map $F:{\boldsymbol{B}}_{\mathbb{X}}\longrightarrow_{lin}{\boldsymbol{B}}_{\mathbb{Y}}$ which tracks $f$, hence $F$ is uniformly continuous w.r.t. the bounded uniformities by Theorem 3.5. Any standard representation $\delta_{\mathbb{Y}}$ is also uniformly continuous as a partial map $\delta_{\mathbb{Y}}:\subseteq{\boldsymbol{B}}_{\mathbb{Y}}\to\mathbb{Y}$, so is the composition $\delta_{\mathbb{Y}}\circ F:\mathsf{dom}(\delta_{\mathbb{X}})\to\mathbb{Y}$. Since $\delta_{\mathbb{X}}$ is a uniform quotient by Lemma 15 in §0.A.6, uniform continuity of $f\circ\delta_{\mathbb{X}}=\delta_{\mathbb{Y}}\circ F$ implies that of $f$.

This result substantially and systematically generalizes the already mentioned result in [MT16]: a function $f:\mathbb{R}\to\mathbb{R}$ is linearly realizable w.r.t. $\rho_{\boldsymbol{R}}$ iff it is uniformly continuous.

5 Related and Future Work

Type theory.

In this paper, we have proposed coherence spaces with totality as an extension of ordinary coherence spaces, following the idea of Kristiansen and Normann. Originally in the domain theory, domains with totality, are introduced by Berger [Be93] to interpret Martin-Löf type theory (i.e., intuitionistic type theory), using “total” domain elements. Since our model of coherence spaces with totality is a linear version of this model, one can expect that it could model intuitionistic linear type theory.

Our theory also includes a natural representation of (separable, metrizable) uniform spaces and uniformly continuous maps between them. Hence it might lead to a denotational model of real functional programming languages (e.g., [Es96, ES14]) extended with other uniform spaces, where one can deal with uniformly continuous functions based on linear types.

Realizability theory.

In the traditional setting, giving representations roughly amounts to constructing modest sets over a partial combinatory algebra (PCA) in the theory of realizability. Our model of coherent representations and stable realizability is in fact considered as a modest set model over a PCA $\mathbb{C}oh$, constructed from the universal coherence space ${\boldsymbol{U}}$ in $\mathbf{Stab}$, to which one can embed any coherence spaces by linear (hence stable) maps. A modest set model turns out to be a model of intuitionistic logic [Lon94, Ba00]. Bauer then gave an attractive paradigm [Ba05]:

*Computable mathematics is a realizability interpretation

of constructive mathematics.*

On the other hand, less is known about the relationship between computable mathematics and linear realizability theory over a linear combinatory algebra (LCA) [AL00], which is a linear analogue of PCA, and for which we can build a PER model of intuitionitstic linear logic. Since the above universal coherence space ${\boldsymbol{U}}$ in fact resides in $\mathbf{Lin}$, it is in principle possible to develop such a theory based on our framework. We believe that exploring this direction, already mentioned in [Ba00], will be an interesting avenue for future work.

Acknowledgement

The author is greatful to Naohiko Hoshino and Kazushige Terui (RIMS) for useful comments.

Appendix 0.A Miscellaneous Proofs

0.A.1 Construction of Totalities

Lemma 2

The functional totality is well-defined: $\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}=\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}^{\perp\perp}$.

Proof

Notice that $({\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}})^{\perp}={\boldsymbol{X}}\otimes{\boldsymbol{Y}}^{\perp}$ and $\widehat{\kappa}(a)\perp\mathfrak{c}$ iff $\kappa\perp a\otimes\mathfrak{c}$ for any $\kappa\in{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}$, $a\in{\boldsymbol{X}}$ and $\mathfrak{c}\in{\boldsymbol{Y}}^{\bot}$. It follows that $\kappa\in\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}$ iff $\widehat{\kappa}(a)\perp\mathfrak{c}$ for any $a\in{\boldsymbol{X}}$ and $\mathfrak{c}\in\mathcal{T}_{\boldsymbol{Y}}^{\bot}$ iff $\kappa\in(\mathcal{T}_{{\boldsymbol{X}}}\otimes\mathcal{T}^{\perp}_{{\boldsymbol{Y}}})^{\perp}$.

The following lemmas prove the internal completeness of $\otimes$ and $\,!\,$ (Proposition 1).

Lemma 3

Given $\mathfrak{a}\in\mathcal{T}_{\boldsymbol{X}}^{\perp}$ and $\mathfrak{b}\in\mathcal{T}_{\boldsymbol{Y}}^{\perp}$, let $\mathfrak{a}\bullet\mathfrak{b}:=\{(x,y):x\in\mathfrak{a},\ y\in\mathfrak{b}\}$. Then $\mathfrak{a}\bullet\mathfrak{b}\in(\mathcal{T}_{{\boldsymbol{X}}}\otimes\mathcal{T}_{{\boldsymbol{Y}}})^{\perp}$.

Proof

First of all, $\mathfrak{a}\bullet\mathfrak{b}$ is an anti-clique of ${\boldsymbol{X}}\otimes{\boldsymbol{Y}}$. Indeed, given $(x,y),(x^{\prime},y^{\prime})\in\mathfrak{a}\bullet\mathfrak{b}$ with $(x,y)\neq(x^{\prime},y^{\prime})$, either $x\neq x^{\prime}$ or $y\neq y^{\prime}$. Assume that $x\neq x^{\prime}$. We then have \neg(x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,x^{\prime}), so \neg((x,y)\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,(x^{\prime},y^{\prime})).

Now given $c\in\mathcal{T}_{\boldsymbol{X}}$ and $d\in\mathcal{T}_{\boldsymbol{Y}}$, we have $c\perp\mathfrak{a}$ and $d\perp\mathfrak{b}$, from which we conclude $c\otimes d\perp\mathfrak{a}\bullet\mathfrak{b}$.

Lemma 4

$\mathcal{T}_{{\boldsymbol{X}}}^{\circ}\otimes\mathcal{T}_{{\boldsymbol{Y}}}^{\circ}\subseteq(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp\perp\circ}$.

Proof

Let $a\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ and $b\in\mathcal{T}_{{\boldsymbol{Y}}}^{\circ}$. It is clear that $a\otimes b\in(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp\perp}$. Too see strictness, let $(x,y)\in a\otimes b$. Then there are $\mathfrak{c}\in\mathcal{T}_{\boldsymbol{X}}^{\perp}$ and $\mathfrak{d}\in\mathcal{T}_{\boldsymbol{Y}}^{\perp}$ such that $x\in\mathfrak{c}$ and $y\in\mathfrak{d}$. Hence $(x,y)\in\mathfrak{c}\bullet\mathfrak{d}$ and $\mathfrak{c}\bullet\mathfrak{d}\in(\mathcal{T}_{{\boldsymbol{X}}}\otimes\mathcal{T}_{{\boldsymbol{Y}}})^{\perp}$ by Lemma 3.

Lemma 5

Assume that $\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$ and $\mathcal{T}_{{\boldsymbol{Y}}}^{\perp}$ are not empty. Given $c\in(\mathcal{T}_{{\boldsymbol{X}}}\otimes\mathcal{T}_{{\boldsymbol{Y}}})^{\perp\perp}$, let $c^{1}:=\{x:(x,y)\in c\mbox{ for some }y\}$ and $c^{2}:=\{y:(x,y)\in c\mbox{ for some }x\}$. Then $c^{1}\in\mathcal{T}_{\boldsymbol{X}}$ and $c^{2}\in\mathcal{T}_{\boldsymbol{Y}}$.

Proof

Let $\mathfrak{a}\in\mathcal{T}_{\boldsymbol{X}}^{\perp}$. Since we suppose that $\mathcal{T}_{\boldsymbol{Y}}\neq\emptyset$ there is $\mathfrak{b}\in\mathcal{T}_{\boldsymbol{Y}}^{\perp}$ and $\mathfrak{a}\bullet\mathfrak{b}\in(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp}$ by Lemma 3. Hence $c\perp\mathfrak{a}\bullet\mathfrak{b}$ and we conclude that $c^{1}\perp\mathfrak{a}$.

Lemma 6

Assume that $\mathcal{T}_{{\boldsymbol{X}}}$ and $\mathcal{T}_{{\boldsymbol{Y}}}$ are not empty. Given $\mathfrak{c}\in(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp}$, let $\mathfrak{c}^{1}:=\{x:(x,y)\in\mathfrak{c}\mbox{ for some }y\}$ and $\mathfrak{c}^{2}:=\{y:(x,y)\in\mathfrak{c}\mbox{ for some }x\}$. Then $\mathfrak{c}^{1}\in\mathcal{T}_{\boldsymbol{X}}^{\perp}$ and $\mathfrak{c}^{2}\in\mathcal{T}_{\boldsymbol{Y}}^{\perp}$.

Proof

Similarly.

Lemma 7

Assume that $\mathcal{T}_{{\boldsymbol{X}}}$, $\mathcal{T}_{{\boldsymbol{Y}}}$, $\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$ and $\mathcal{T}_{{\boldsymbol{Y}}}^{\perp}$ are all nonempty. Then $(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp\perp\circ}\subseteq\mathcal{T}_{{\boldsymbol{X}}}^{\circ}\otimes\mathcal{T}_{{\boldsymbol{Y}}}^{\circ}$.

Proof

Let $c\in(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp\perp\circ}$. We prove that $c^{1}\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ (and $c^{2}\in\mathcal{T}_{{\boldsymbol{Y}}}^{\circ}$). Since $c\subseteq c^{1}\otimes c^{2}$ and $c^{1}\otimes c^{2}$ is strict in $(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp\perp}$ by Lemma 4, we will be able to conclude that $c=c^{1}\otimes c^{2}\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}\otimes\mathcal{T}_{{\boldsymbol{Y}}}^{\circ}$ by strictness of $c$.

Totality of $c^{1}$ is due to Lemma 5. To show strictness, let $x\in c^{1}$, so that $(x,y)\in c$ for some $y$. Since $c$ is strict, there is $\mathfrak{d}\in(\mathcal{T}_{\boldsymbol{X}}\otimes\mathcal{T}_{\boldsymbol{Y}})^{\perp}$ such that $(x,y)\in\mathfrak{d}$. We then have $x\in\mathfrak{d}^{1}$ and $\mathfrak{d}^{1}\in\mathcal{T}_{\boldsymbol{X}}^{\perp}$ by Lemma 6.

We have established the internal completeness of $\otimes$. Let us next proceed to connective $!$.

Lemma 8

Given $\mathfrak{c}_{1},\dots,\mathfrak{c}_{n}\in\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$, let

[TABLE]

Then $\wedge_{i}\mathfrak{c}_{i}\in(!\mathcal{T}_{{\boldsymbol{X}}})^{\perp}$. In particular, $\wedge\!\mathfrak{c}:=\{\{x\}\in{\boldsymbol{X}}:x\in\mathfrak{c}\}\in(!\mathcal{T}_{{\boldsymbol{X}}})^{\perp}$.

Proof

Each $\wedge_{i}\mathfrak{c}_{i}$ consists of finite cliques of ${\boldsymbol{X}}$, namely tokens of $!{\boldsymbol{X}}$, which are pairwise incoherent in $!{\boldsymbol{X}}$. Indeed, given distinct $\{x_{1},\dots,x_{n}\},\{y_{1},\dots,y_{n}\}$, there is $i$ such that $x_{i}\neq y_{i}$ and $x_{i},y_{i}\in\mathfrak{c}_{i}$. We have \neg(x_{i}\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,y_{i}), so that \neg(\{x_{1},\dots,x_{n}\}\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,\{y_{1},\dots,y_{n}\}). Hence $\wedge_{i}\mathfrak{c}_{i}\in(!{\boldsymbol{X}})^{\perp}$.

To see totality, suppose that $a\in\mathcal{T}_{\boldsymbol{X}}$ so that $!a\in!\mathcal{T}_{\boldsymbol{X}}$. We then have $x_{i}\in a\cap\mathfrak{c}_{i}$ for each $1\leq i\leq n$, hence the clique $\{x_{1},\dots,x_{n}\}\subseteq a$ belongs to $\wedge_{i}\mathfrak{c}_{i}$. This proves $!a\perp\wedge_{i}\mathfrak{c}_{i}$.

Lemma 9

$\,!\,\mathcal{T}_{{\boldsymbol{X}}}^{\circ}\subseteq(\,!\,\mathcal{T}_{{\boldsymbol{X}}})^{\perp\perp\circ}$.

Proof

It is easy to see that every $!a\in\,!\,\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ belongs to $(\,!\,\mathcal{T}_{{\boldsymbol{X}}})^{\perp\perp}$. For strictness, let $a_{0}=\{x_{1},\dots,x_{n}\}\in!a$. Since $a\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$, there are $\mathfrak{c}_{i}\in\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$ such that $x_{i}\in\mathfrak{c}_{i}$ for each $1\leq i\leq n$. Applying the previous lemma, we obtain $\wedge_{i}\mathfrak{c}_{i}\in(\,!\,\mathcal{T}_{{\boldsymbol{X}}})^{\perp}$, which contains $a_{0}$.

Lemma 10

Given $\alpha\in(!\mathcal{T}_{\boldsymbol{X}})^{\perp\perp}$, let $\alpha^{1}:=\{x:\{x\}\in\alpha\cap(\wedge\!\mathfrak{c})\mbox{ for some }\mathfrak{c}\in\mathcal{T}_{\boldsymbol{X}}^{\perp}\}$. Then $\alpha^{1}\in\mathcal{T}_{\boldsymbol{X}}^{\circ}$.

Proof

Given $\mathfrak{c}\in\mathcal{T}_{\boldsymbol{X}}^{\perp}$, we have $\wedge\!\mathfrak{c}\in(!\mathcal{T}_{\boldsymbol{X}})^{\perp}$ by Lemma 8. Hence $\{x\}\in\alpha\cap(\wedge\!\mathfrak{c})$ for some $x$, so $x\in\alpha^{1}\cap\mathfrak{c}$. Strictness of $\alpha^{1}$ is obvious.

Lemma 11

$(\,!\,\mathcal{T}_{{\boldsymbol{X}}})^{\perp\perp\circ}\subseteq\,!\,(\mathcal{T}_{{\boldsymbol{X}}}^{\circ})$.

Proof

Let $\alpha\in(!\mathcal{T}_{\boldsymbol{X}})^{\perp\perp\circ}$. We prove that $!\alpha^{1}\subseteq\alpha$. Since $!\alpha^{1}\in(!\mathcal{T}_{\boldsymbol{X}})^{\perp\perp\circ}$ by combining Lemmas 9 and 10, we will be able to conclude $\alpha=!\alpha^{1}\in!\mathcal{T}_{\boldsymbol{X}}^{\circ}$ by strictness of $\alpha$.

Let $a_{0}\in!\alpha^{1}$. As in the proof of Lemma 9, we obtain $\mathfrak{c}_{i}\in\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$ ($1\leq i\leq n$) such that $a_{0}\in\wedge_{i}\mathfrak{c}_{i}\in(\,!\,\mathcal{T}_{{\boldsymbol{X}}})^{\perp}$. Meanwhile, we have some $a_{1}\in\alpha\cap\wedge_{i}\mathfrak{c}_{i}$ since $\alpha\in(!\mathcal{T}_{\boldsymbol{X}})^{\perp\perp\circ}$. If $a_{0}\neq a_{1}$, there would be $x,y\in\mathfrak{c}_{i}$ such that $x\in a_{0}$, $y\in a_{1}$ and $x\neq y$. We would have \neg(x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,y) since they belong to an anti-clique $\mathfrak{c}_{i}$, while x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,y since they belong to a clique $\bigcup\alpha$, that is a contradiction. We therefore conclude that $a_{0}=a_{1}\in\alpha$.

This completes the proof of Proposition 1.

0.A.2 The proof of Theorem 3.4

Let us begin with an important lemma:

Lemma 12

For every $a\in{\boldsymbol{X}}_{\mathsf{fin}}$ with $\langle a\rangle^{\circ}\neq\emptyset$, there exist finitely many uni-covers $\mathfrak{c}_{1},\ldots,\mathfrak{c}_{m}\in\sigma^{\mathrm{b}}_{\boldsymbol{X}}$ such that $a\in\mathfrak{c}_{1}\wedge\cdots\wedge\mathfrak{c}_{m}$, hence $a$ is contained in the unbounded cover $\mathfrak{c}_{1}\wedge\cdots\wedge\mathfrak{c}_{m}\in\beta_{{\boldsymbol{X}}}^{\mathrm{ub}}$.

Proof

Let $a=\{x_{1},\ldots,x_{m}\}$. By assumption, there exists $b\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ with $b\supseteq a$. By strictness of $b$, each $x_{i}$ is contained in some $\mathfrak{c}_{i}\in\mathcal{T}_{{\boldsymbol{X}}}^{\perp}$, which we may assume is strict. Hence we have $a\in\mathfrak{c}_{1}\wedge\cdots\wedge\mathfrak{c}_{m}$.

The next lemma is used to cut down and divide the set $\mathcal{T}_{\boldsymbol{X}}^{\circ}$.

Lemma 13

For any $n\in\mathbb{N}$ and $a_{0},\ldots,a_{n}\in{\boldsymbol{X}}_{\mathsf{fin}}$, there exists $\mathfrak{B}\in(!{\boldsymbol{X}})^{\perp}$ such that $\sum_{b\in\mathfrak{B}}\langle b\rangle^{\circ}=\langle a_{n}\rangle^{\circ}\,\setminus\,\bigcup_{i=0}^{n-1}\langle a_{i}\rangle^{\circ}$.

Proof

Without loss of generality, one can assume that $\langle a_{i}\rangle^{\circ}\neq\emptyset$ for all $i=1,\ldots,n$. By Lemma 12, each $a_{i}$ belongs to some unbounded-cover $\mathfrak{A}_{i}\in\beta^{\mathrm{ub}}$. Define

[TABLE]

We then have $c\in\langle b\rangle^{\circ}$ for some $b=b_{0}\cup\dots\cup b_{n-1}\cup a_{n}\in\mathfrak{B}$ iff $c\in\langle b_{0}\rangle^{\circ}\cap\dots\cap\langle b_{n-1}\rangle^{\circ}\cap\langle a_{n}\rangle^{\circ}$ iff $c\not\in\langle a_{0}\rangle^{\circ},\dots,c\not\in\langle a_{n-1}\rangle^{\circ}$ (by disjointness) and $c\in\langle a_{n}\rangle^{\circ}$.

Now we go on the proof of Theorem 3.4: $(\mathcal{T}_{{\boldsymbol{X}}}^{\circ},\mu^{\mathrm{ub}}_{\boldsymbol{X}})$ is a fine uniform space.

Proof

Let $\mathcal{U}$ be an open cover of $\mathcal{T}_{\boldsymbol{X}}^{\circ}$. Since an open set in $\mathcal{T}_{\boldsymbol{X}}^{\circ}$ is a countable union of upper sets $\langle a\rangle^{\circ}$, we can assume that $\mathcal{U}$ is of the form $\{\langle a_{n}\rangle^{\circ}:n\in\mathbb{N}\}$. Our goal is to show that there exists $\mathfrak{B}\in\mathcal{T}_{!{\boldsymbol{X}}}^{\perp}$ which refines $\mathcal{U}$: for any $b\in\mathfrak{B}$ there exists $n\in\mathbb{N}$ with $\langle b\rangle\subseteq\langle a_{n}\rangle$. It will follow that $\mathfrak{B}^{\circ}$ belongs to $\mu^{\mathrm{ub}}$ and so does $\mathcal{U}$ by axiom (U2).

Let us denote $\mathcal{D}_{n}:=\langle a_{n}\rangle^{\circ}\,\setminus\,\bigcup_{i=0}^{n-1}\langle a_{i}\rangle^{\circ}$ so that $\mathcal{T}_{\boldsymbol{X}}^{\circ}=\sum_{n}\mathcal{D}_{n}$. For each $n\in\mathbb{N}$, apply Lemma 13 to $a_{0},\ldots,a_{n}$ to find $\mathfrak{B}_{n}\in(!\,{\boldsymbol{X}})^{\perp}$ such that $\sum_{b\in\mathfrak{B}_{n}}\langle b\rangle^{\circ}=\mathcal{D}_{n}$.

Now it is easy to see that $\mathcal{B}:=\bigcup_{n}\mathcal{B}_{n}$ also belongs to $(!\,{\boldsymbol{X}})^{\perp}$ and moreover $\mathcal{B}\in\mathcal{T}_{!{\boldsymbol{X}}}^{\perp}$, since $\{\langle b\rangle^{\circ}:b\in\mathfrak{B}\}$ covers $\mathcal{T}_{\boldsymbol{X}}^{\circ}=\sum_{n}\mathcal{D}_{n}$. Finally, any $b\in\mathcal{B}_{n}\subseteq\mathcal{B}$ satisfies $\langle b\rangle\subseteq\mathcal{D}_{n}\subseteq\langle a_{n}\rangle$.

0.A.3 Existence of a pseudo-Map of Adjunctions

The pair of functors $\langle I,J\rangle$ in the diagram (3) is a psudo-map of adjunctions. That is, $\langle I,J\rangle$ preserves the counit-unit pair (up to isomorphisms): $J\eta_{\mathrm{coh}}=(\eta_{\mathrm{unif}})_{J}:J\Rightarrow JLK\simeq GFJ$ and $I\epsilon_{\mathrm{coh}}=(\epsilon_{\mathrm{unif}})_{I}:IKL\simeq FGI\Rightarrow I$, where $\langle\epsilon_{\mathrm{coh}},\eta_{\mathrm{coh}}\rangle$ and $\langle\epsilon_{\mathrm{unif}},\eta_{\mathrm{unif}}\rangle$ are the counit-unit pairs of the adjunctions $F\dashv G$ and $K\dashv L$, respectively.

Proof

Let ${\boldsymbol{X}}\in\mathbf{Stab}_{\mathsf{STot}}$ be a coherence space with totality. Since $(\eta_{\mathrm{coh}})_{\boldsymbol{X}}(a):=\,!\,a$ for every $a\in{\boldsymbol{X}}$, $(I\eta_{\mathrm{coh}})_{\boldsymbol{X}}:(\mathcal{T}_{{\boldsymbol{X}}}^{\circ},\tau_{\mathrm{Sco}})\to(\mathcal{T}_{\,!\,{\boldsymbol{X}}}^{\circ},\tau_{\mathrm{Sco}})$ gives the bijection $a\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}\mapsto\,!\,a\in\mathcal{T}_{\,!\,{\boldsymbol{X}}}^{\circ}$ given in Proposition 1. On the other hand, $(\eta_{\mathrm{unif}})_{I{\boldsymbol{X}}}:(\mathcal{T}_{{\boldsymbol{X}}}^{\circ},\tau_{\mathrm{Sco}})\to(\mathcal{T}_{{\boldsymbol{X}}}^{\circ},\tau_{\mathrm{Sco}})$ is the identity, therefore, $I\eta_{\mathrm{coh}}=(\eta_{\mathrm{unif}})_{I}$ up to isomorphisms.

Let ${\boldsymbol{Y}}\in\mathbf{Lin}_{\mathsf{STot}}$ be a coherence space with totality. Recall that $(\epsilon_{\mathrm{coh}})_{\boldsymbol{Y}}:\,!\,{\boldsymbol{Y}}\longrightarrow_{lin}{\boldsymbol{Y}}$ is the dereliction so that $(\epsilon_{\mathrm{coh}})_{\boldsymbol{Y}}(\,!\,a):=a$ for every $a\in{\boldsymbol{Y}}$. Hence $(J\epsilon_{\mathrm{coh}})_{\boldsymbol{Y}}:(\mathcal{T}_{\,!\,{\boldsymbol{Y}}}^{\circ},\mu_{\,!\,{\boldsymbol{Y}}}^{\mathrm{b}})\to(\mathcal{T}_{{\boldsymbol{Y}}}^{\circ},\mu_{{\boldsymbol{Y}}}^{\mathrm{b}})$ also gives the uniform homeomorphism in Proposition 1. Similarly, $(\epsilon_{\mathrm{unif}})_{J{\boldsymbol{Y}}}:(\mathcal{T}_{\boldsymbol{Y}}^{\circ},\mu_{\mathrm{fine}})\to(\mathcal{T}_{\boldsymbol{Y}}^{\circ},\mu_{{\boldsymbol{Y}}}^{\mathrm{b}})$ is the identity, therefore, we obtain $J\epsilon_{\mathrm{coh}}=(\epsilon_{\mathrm{unif}})_{J}$ up to isomorphisms.

0.A.4 Uniform Structure on a Linear Function Space

We shall exhibit an explicit structure of uniformity on a function space induced by co-totality given in §3.

Proposition 4

Every total linear map $F:({\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}})\longrightarrow_{lin}{\boldsymbol{Z}}$ is uniformly continuous at single points: for every $\mathfrak{c}\in\sigma_{{\boldsymbol{Z}}}^{\mathrm{b}}$, there exist $a\in\mathcal{T}_{\boldsymbol{X}}^{\circ}$ and a total linear map $G:{\boldsymbol{Y}}\longrightarrow_{lin}{\boldsymbol{Z}}$ such that $|F(\kappa)-G(\widehat{\kappa}(a_{0}))|<\mathfrak{c}$ for every $\kappa\in\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}^{\circ}$.

Proof

By Theorem 3.5, there exists $\mathfrak{f}\in\sigma^{\mathrm{b}}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}$ such that $|\kappa-\kappa^{\prime}|<\mathfrak{f}\ \Rightarrow\ |F(\kappa)-F(\kappa^{\prime})|<\mathfrak{c}$ for all $\kappa,\kappa^{\prime}\in\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}^{\circ}$. Notice that $({\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}})^{\perp}={\boldsymbol{X}}\otimes{\boldsymbol{Y}}^{\perp}$. Hence $\sigma^{\mathrm{b}}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}=\mathcal{T}_{\boldsymbol{X}}^{\circ}\otimes(\mathcal{T}_{\boldsymbol{Y}}^{\perp})^{\circ}$ by Proposition 1, so $\mathfrak{f}=a_{0}\otimes\mathfrak{b}$ for some $a_{0}\in\mathcal{T}_{\boldsymbol{X}}^{\circ}$ and $\mathfrak{b}\in\sigma^{\mathrm{b}}_{\boldsymbol{Y}}$. We now have $|\kappa-\kappa^{\prime}|<a_{0}\otimes\mathfrak{b}\Rightarrow|F(\kappa)-F(\kappa^{\prime})|<\mathfrak{c}$.

Let $\mathfrak{c}\in\mathcal{T}_{{\boldsymbol{X}}}^{\circ}$ be an arbitrary uni-cover, and define $\theta\in{\boldsymbol{Y}}\longrightarrow_{lin}({\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}})$ as \mathsf{tr}(\theta):=\{(y,(x,y)):\mbox{x\in\mathfrak{c}$,$y\in Y}\}. It is easy to see that $\theta$ is strictly total and satisfies that $\widehat{\theta}(b)(a):=b$ for all $a\in\mathcal{T}_{\boldsymbol{X}}$ and $b\in\mathcal{T}_{\boldsymbol{Y}}$.

Then $G:=F\circ\theta:{\boldsymbol{Y}}\longrightarrow_{lin}{\boldsymbol{Z}}$ is a total linear map satisfying our requirement: By letting $b_{0}:=\widehat{\kappa}(a_{0})$,

[TABLE]

What is interesting here is that the uniform structures on the constructed spaces are determined by purely logical rules: for instance $({\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}})^{\perp}={\boldsymbol{X}}\otimes{\boldsymbol{Y}}^{\perp}$.

0.A.5 The proof of Theorem 4.7

To prove the theorem, we first observe that a standard representation $\delta_{\mathbb{X}}$ satisfies a kind of universality.

A coherent representation ${\boldsymbol{X}}\stackrel{{\scriptstyle\gamma}}{{\longrightarrow}}\mathbb{Y}$ is said to be linearish if (i) x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,y implies $\gamma[\langle x\rangle]\cap\gamma[\langle y\rangle]\neq\emptyset$ for every $x,y\in X$; and (ii) for every uniform cover $\mathcal{U}\in\mu_{\mathbb{Y}}$ there exists $\mathfrak{c}\in\sigma^{\mathrm{b}}_{\boldsymbol{X}}$ such that $|a-b|<\mathfrak{c}\Rightarrow|\gamma(a)-\gamma(b)|<\mathcal{U}$ for all $a,b\in\mathsf{dom}(\gamma)$, which is an analogue of strong uniform continuity in Theorem 3.5.

A standard representation ${\boldsymbol{B}}_{\mathbb{X}}\stackrel{{\scriptstyle\delta_{\mathbb{X}}}}{{\longrightarrow}}\mathbb{X}$ is indeed linearish. Let $\beta=\{\mathcal{U}_{n}\}$ be a countable basis of a uniform space $\mathbb{X}=(X,\mu_{X})$ and $\delta_{\mathbb{X}}$ is a standard representation induced from $\beta$. (i) By definition, (n,U)\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,(m,V) implies $U\cap V\neq\emptyset$, hence $\delta_{\mathbb{X}}[(n,U)]=U$, $\delta_{\mathbb{X}}[(m,V)]=V$ and $\delta_{\mathbb{X}}[(n,U)]\cap\delta_{\mathbb{X}}[(m,V)]\neq\emptyset$. (ii) For every uniform cover $\mathcal{U}\in\mu_{X}$, there exists $n\in\mathbb{N}$ such that $\mathcal{U}_{n}$ refines $\mathcal{U}$. Since $\mathfrak{c}:=\{(n,U):U\in\mathcal{U}_{n}\}$ is a uni-partition of $\mathcal{T}_{{\boldsymbol{B}}_{\mathbb{X}}}$, we have $|a-b|<\mathfrak{c}\Rightarrow|\delta_{\mathbb{X}}(a)-\delta_{\mathbb{X}}(b)|<\mathcal{U}_{n}<\mathcal{U}$.

The following lemma indicates that $\delta_{\mathbb{X}}$ is a representative example of linearish representations.

Lemma 14

For any subspace $\mathbb{X}_{0}\subseteq\mathbb{X}$ and any linearish representation ${\boldsymbol{X}}\stackrel{{\scriptstyle\gamma}}{{\longrightarrow}}\mathbb{X}_{0}$, there exists a linear map $F:{\boldsymbol{X}}\longrightarrow_{lin}{\boldsymbol{B}}_{\mathbb{X}}$ with $\delta_{\mathbb{X}}\circ F=\gamma$.

In particular, it immediately follows that standard representations of $\mathbb{X}$ are all isomorphic by letting $\mathbb{X}_{0}:=\mathbb{X}$, hence they do not depend on the choice of uniform basis $\beta$.

Proof

Let $\{\mathcal{U}_{n}:n\in\mathbb{N}\}$ be a countable basis on $\mathbb{X}$. Since $\gamma$ is linearish, we can take a sequence of uni-covers $\{\mathfrak{c}_{n}:n\in\mathbb{N}\}\subseteq\sigma^{\mathrm{b}}_{\boldsymbol{X}}$ such that $|a-b|<\mathfrak{c}_{n}\Rightarrow|\gamma(a)-\gamma(b)|<\mathcal{U}_{n}$ for each $n\in\mathbb{N}$. Let $\psi:\subseteq X\times\mathbb{N}\to B$ be a partial function so that $\psi(x,n):=U$ is defined for each $n\in\mathbb{N}$ and $x\in\mathfrak{a}_{n}$, and then $U\in\mathcal{U}_{n}$ and $\gamma[\langle x\rangle]\subseteq U$. We define a linear map $F:X\longrightarrow_{lin}{\boldsymbol{B}}_{\mathbb{X}}$ as F(a):=\{\psi(x,n):\mbox{n\in\mathbb{N}$and$x\in a}\}. Let us now verify that $F$ is the desired map in 4 steps.

(i) $F(a)\in{\boldsymbol{B}}_{\mathbb{X}}$ for every $a\in{\boldsymbol{X}}$. Let $(n,U),(m,V)\in F(a)$ with $(n,U)\neq(m,V)$. This means that there exist $x\in\mathfrak{a}_{n}$, and $w\in\mathfrak{a}_{m}$ such that $\psi(x,n)=U$, $\psi(w,m)=V$ and $x,w\in a$ (so x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,w). If $n=m$ then $x=w$ since x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,w but $x,w\in\mathfrak{a}_{n}$. Hence $U=\psi(x,n)=\psi(z,m)=V$, contradicting the assumption, so $n\neq m$.

We also have $U\cap V\neq\emptyset$, since x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,w implies $\gamma[\langle x\rangle]\cap\gamma[\langle w\rangle]\neq\emptyset$, $\gamma[\langle x\rangle]\subseteq U$ and $\gamma[\langle w\rangle]\subseteq V$. Therefore, (n,U)\,\raisebox{0.0pt}{\shortstack{\frown\\ [-.3em]$$}}\,(m,V).

(ii) $F$ is a linear map. It is sufficient to verify the condition that $F(a)\ni y$ implies the unique existence of $x\in X$ such that $F(\{x\})\ni y$. Let $y=(n,U)\in B$. By definition, it is immediate that there is a unique $x\in a\cap\mathfrak{a}_{n}$ such that $\psi(x,n)=U$.

(iii) $F(a)\in({\boldsymbol{B}}_{\mathbb{X}})_{\mathsf{max}}$ for every $a\in\mathsf{dom}(\gamma)$. Let $x_{n}\in a\cap\mathfrak{a}_{n}$ for each $n\in\mathbb{N}$. It suffices to show that for every $n\in\mathbb{N}$ there is $(n,U)\in F(a)$ for some $U\in\mathcal{U}_{n}$. By definition, $\psi(x_{n},n):=U$ is defined so that $(n,U)\in F(a)$.

(iv) $\delta_{\mathbb{X}}\circ F(a)=\gamma(a)$ for every $a\in\mathsf{dom}(\gamma)$. Suppose that $(n,U_{n})\in F(a)$, namely there is $x\in a$ such that $\psi(x,n)=U_{n}$. By definition, we have $\gamma(a)\in\gamma[\langle x\rangle]\subseteq U_{n}$. Since it holds for every token of $F(a)$, we have $\gamma(a)\in\bigcap_{(n,U_{n})\in F(a)}U_{n}$. Therefore, $F(a)\in\mathsf{dom}(\delta_{\mathbb{X}})$ and $\delta_{\mathbb{X}}\circ F(a)=\gamma(a)$.

We are now ready to prove Theorem 4.7. Let $\mathbb{Y}_{0}:=f[\mathbb{X}]$ and $\gamma:=f\circ\delta_{\mathbb{X}}$. Then $\gamma$ is linearish: (i) If x\,\raisebox{-1.99997pt}{\shortstack{\frown$\\ [-.3em]$\smile}}\,y then $\delta_{\mathbb{X}}[\langle x\rangle]\cap\delta_{\mathbb{X}}[\langle y\rangle]\neq\emptyset$ hence $\gamma[\langle x\rangle]\cap\gamma[\langle y\rangle]\neq\emptyset$. (ii) For every (subspace) uniform cover $\mathcal{V}\in\mu_{\mathbb{Y}_{0}}$, there exists $\mathcal{U}\in\mu_{\mathbb{X}}$ such that $|p-q|<\mathcal{U}\ \Rightarrow\ |f(p)-f(q)|<\mathcal{V}$, and we also have $\mathfrak{c}\in\sigma^{\mathrm{b}}_{\boldsymbol{X}}$ such that $|a-b|<\mathfrak{c}\ \Rightarrow\ |\delta_{\mathbb{X}}(a)-\delta_{\mathbb{X}}(b)|<\mathcal{U}$, since $\delta_{\mathbb{X}}$ is linearish.

Applying Lemma 14 to ${\boldsymbol{B}}_{\mathbb{X}}\stackrel{{\scriptstyle\delta_{\mathbb{X}}}}{{\longrightarrow}}\mathbb{X}\stackrel{{\scriptstyle f}}{{\longrightarrow}}{\mathbb{Y}_{0}}$, we obtain a (total) linear map $F:{\boldsymbol{B}}_{\mathbb{X}}\longrightarrow_{lin}{\boldsymbol{B}}_{\mathbb{Y}}$ such that $\delta_{\mathbb{Y}}\circ F=f\circ\delta_{\mathbb{X}}$. This concludes Theorem 4.7.

0.A.6 The Lemma for Theorem 4.8

Lemma 15

If $\mathbb{X}$ is chain-connected, the standard representation $\delta_{\mathbb{X}}$ is a uniform quotient. That is, $\{\delta_{\mathbb{X}}[\mathfrak{c}]:\mathfrak{c}\in\sigma_{{\boldsymbol{X}}}^{\mathrm{b}}\}$ is a uniform basis of $\mathbb{X}$, where $\delta_{\mathbb{X}}[\mathfrak{c}]$ is a cover of $\mathbb{X}$ defined by $\{\delta_{\mathbb{X}}[\langle x\rangle]:x\in\mathfrak{c}\}$.

Proof

We need to check that the surjection ${\boldsymbol{B}}_{\mathbb{X}}\stackrel{{\scriptstyle\delta_{\mathbb{X}}}}{{\longrightarrow}}\mathbb{X}$ induces the uniformity on $\mathbb{X}$: namely, $\{\delta_{\mathbb{X}}[\mathfrak{c}]:\mathfrak{c}\in\sigma^{\mathrm{b}}_{{\boldsymbol{B}}_{\mathbb{X}}}\}$ forms a uniform basis of $\mathbb{X}$, where $\delta_{\mathbb{X}}[\mathfrak{c}]$ is a cover of $\mathbb{X}$ defined by $\delta_{\mathbb{X}}[\mathfrak{c}]:=\{\delta_{\mathbb{X}}[\langle x\rangle]:x\in\mathfrak{c}\}$.

Let $\{\mathcal{U}_{n}:n\in\mathbb{N}\}$ be a countable basis of $\mathbb{X}$. All we have to show is that each uni-cover $\mathfrak{c}\in\sigma^{\mathrm{b}}_{{\boldsymbol{B}}_{\mathbb{X}}}$ is of the form $\mathfrak{c}=\{(n,U):U\in\mathcal{U}_{n}\}$ for some $n\in\mathbb{N}$. Then $\delta_{\mathbb{X}}[\mathfrak{c}]=\mathcal{U}_{n}$, hence they generate the uniformity on $\mathbb{X}$.

Let $\mathfrak{c}\in\sigma^{\mathrm{b}}_{{\boldsymbol{B}}_{\mathbb{X}}}$ be a uni-cover of $\mathsf{dom}(\delta_{\mathbb{X}})$. Since $\mathfrak{c}\neq\emptyset$, one can fix a token $(n,U_{n})\in\mathfrak{c}$.

Indeed $\mathfrak{c}=\{(n,U):U\in\mathcal{U}_{n}\}$. By chain-connectedness of $\mathbb{X}$, we have $U_{n}^{\prime}\neq U_{n}\in\mathcal{U}_{n}$ such that $U_{n}\cap U_{n}^{\prime}\neq\emptyset$. Given arbitrary $p\in U_{n}\cap U_{n}^{\prime}$, we can take $\{U_{m}:m\neq n\}$ such that $p\in U_{m}\in\mathcal{U}_{m}$ for each $m\neq n\in\mathbb{N}$. Let $a:=\{(m,U_{m}):m\neq n\}\cup\{(n,U_{n})\}$ and $a^{\prime}:=\{(m,U_{m}):m\neq n\}\cup\{(n,U^{\prime}_{n})\}$. Both $p\in\bigcap_{m\neq n}U_{m}\cap U_{n}$ and $p\in\bigcap_{m\neq n}U_{m}\cap U^{\prime}_{n}$ hold, hence $a,a^{\prime}\in\mathsf{dom}(\delta_{\mathbb{X}})$. Since $\mathfrak{c}$ is a uni-cover of $\mathsf{dom}(\delta_{\mathbb{X}})$, both $a\perp\mathfrak{c}$ and $a^{\prime}\perp\mathfrak{c}$ hold, therefore, $(n,U_{n}^{\prime})\in\mathfrak{c}$ (otherwise, if $(m,U_{m})\in a^{\prime}\cap\mathfrak{c}$, then $a\cap\mathfrak{c}$ contains both $(n,U_{n})$ and $(m,U_{m})$, which contradicts that $a\cap\mathfrak{c}$ must be a singleton.

Repeating this argument, we obtain $(n,U)\in\mathfrak{c}$ for all $U\in\mathcal{U}_{n}$.

0.A.7 Some Constructions of Coherent Representations

Typical constructions of coherent representations are naturally given as follows. Given ${\boldsymbol{X}}\stackrel{{\scriptstyle\rho_{\boldsymbol{X}}}}{{\longrightarrow}}S$ and ${\boldsymbol{Y}}\stackrel{{\scriptstyle\rho_{\boldsymbol{Y}}}}{{\longrightarrow}}T$, define:

• •

${\boldsymbol{X}}\otimes{\boldsymbol{Y}}\stackrel{{\scriptstyle[\rho_{\boldsymbol{X}}\otimes\rho_{\boldsymbol{Y}}]}}{{\longrightarrow}}S\times T$ is defined as $\mathsf{dom}([\rho_{{\boldsymbol{X}}}\otimes\rho_{{\boldsymbol{Y}}}]):=\mathsf{dom}(\rho_{\boldsymbol{X}})\otimes\mathsf{dom}(\rho_{\boldsymbol{Y}})$ and $[\rho_{{\boldsymbol{X}}}\otimes\rho_{{\boldsymbol{Y}}}](a\otimes b):=(\rho_{\boldsymbol{X}}(a),\rho_{\boldsymbol{Y}}(b))$, where $\mathsf{dom}(\ )$ means the domains of representations (as partial maps).

• •

${\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}\stackrel{{\scriptstyle[\rho_{{\boldsymbol{X}}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}]}}{{\longrightarrow}}\mathcal{LR}(\rho_{\boldsymbol{X}},\rho_{\boldsymbol{Y}})$ is defined as follows. Define $[\rho_{{\boldsymbol{X}}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}]:\subseteq{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}\longrightarrow T^{S}$ by

[TABLE]

$\mathcal{LR}(\rho_{\boldsymbol{X}},\rho_{\boldsymbol{Y}})\subseteq\mathbb{Y}^{\mathbb{X}}$ is the range of $[\rho_{{\boldsymbol{X}}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}]$, which consists of linearly realizable functions.

• •

$\,!\,{\boldsymbol{X}}\stackrel{{\scriptstyle[\,!\,\rho_{\boldsymbol{X}}]}}{{\longrightarrow}}S$ is defined as $\mathsf{dom}([\,!\,\rho_{{\boldsymbol{X}}}]):=\,!\,\mathsf{dom}(\rho_{\boldsymbol{X}})$ and $[\,!\,\rho_{{\boldsymbol{X}}}](\,!\,a):=\rho_{\boldsymbol{X}}(a)$ for every $a\in\mathsf{dom}(\rho_{\boldsymbol{X}})$.

Unfortunately, the total extension lemma (Lemma 1) is no longer available for these constructions. For instance, we do not have $\mathsf{dom}([\rho_{{\boldsymbol{X}}}\otimes\rho_{{\boldsymbol{Y}}}])^{\perp\perp}=\mathcal{T}_{{\boldsymbol{X}}\otimes{\boldsymbol{Y}}}$ in general, where $\mathcal{T}_{{\boldsymbol{X}}\otimes{\boldsymbol{Y}}}$ is the tensor of the totalities $\mathcal{T}_{\boldsymbol{X}}$ and $\mathcal{T}_{\boldsymbol{Y}}$ which are the double negations of $\mathsf{dom}(\rho_{\boldsymbol{X}})$ and $\mathsf{dom}(\rho_{\boldsymbol{Y}})$ respectively.

To avoid this, we consider the following condition. A coherent representation ${\boldsymbol{X}}\stackrel{{\scriptstyle\rho_{\boldsymbol{X}}}}{{\longrightarrow}}S$ is said to be classical if $\mathsf{dom}(\rho_{\boldsymbol{X}})=\mathsf{dom}(\rho_{\boldsymbol{X}})^{\perp\perp\circ}$ (i.e. the domain is a totality on ${\boldsymbol{X}}$ and consists of strict total cliques). As noted in Example 4, a complete space $\mathbb{X}$ has a classical standard representation $\delta_{\mathbb{X}}$.

Then it is easy to see that if $\rho_{\boldsymbol{X}}$ and $\rho_{\boldsymbol{Y}}$ are classical, so are $[\rho_{\boldsymbol{X}}\otimes\rho_{\boldsymbol{Y}}]$ and $[\,!\,\rho_{\boldsymbol{X}}]$, due to the internal completeness (Proposition 1). Although $[\rho_{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}]$ is not classical, one can naturally restrict it as follows. Since $[\rho_{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}](\kappa)=[\rho_{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}](\kappa^{\circ})$ for every $\kappa\in\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}$, the strict restriction $[\rho_{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}]^{\circ}:\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}^{\circ}\to\mathcal{LR}(\rho_{\boldsymbol{X}},\rho_{\boldsymbol{Y}})$ is well-defined.

These representations are indeed compatible with the uniformities induced by totalities: $\mathsf{dom}([\rho_{\boldsymbol{X}}\otimes\rho_{\boldsymbol{Y}}])^{\perp\perp}=\mathcal{T}_{{\boldsymbol{X}}\otimes{\boldsymbol{Y}}}$, $\mathsf{dom}([\rho_{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}\rho_{\boldsymbol{Y}}]^{\circ})^{\perp\perp}=\mathcal{T}_{{\boldsymbol{X}}\mathbin{-\mkern-3.0mu\circ}{\boldsymbol{Y}}}$ and $\mathsf{dom}([\,!\,\rho_{\boldsymbol{X}}])^{\perp\perp}=\mathcal{T}_{\,!\,{\boldsymbol{X}}}$, where $\mathcal{T}_{\boldsymbol{X}}:=\mathsf{dom}(\rho_{\boldsymbol{X}})$ and $\mathcal{T}_{\boldsymbol{Y}}:=\mathsf{dom}(\rho_{\boldsymbol{Y}})$.