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
01
Uniform spaces can be represented by coherence spaces with totality.
02
Uniformly continuous functions correspond to total linear maps in the model.
03
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.
Equations22
Tych
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}\ .
\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}\ .
[\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}}$.}
[\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}}$.}
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
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 R, 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.
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βR is presented by a
rational Cauchy sequence (xnβ)nβNβ with β£xβxnββ£β€2βn.
Let f:RβR be a computable function
which is uniformly continuous.
Then there must be a function ΞΌ:Nβ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ΞΌ(m)β,
no matter where x is located on the real line.
Thus one has to access the sequence (xnβ) (regarded as an oracle)
only once.
On the other hand,
if f:RβR is not uniformly continuous,
it admits no uniform modulus of continuity. Hence one has to accsess
(xnβ) 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 ΞΌ around x,
once for getting the approximate value xΞΌ(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.
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 X
the finest uniform space !X compatible with 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 X and Y be topological spaces
admissibly represented by (partial surjections from)
coherence spaces X and Y (eg.Β the real line R is admissibly represented by a
coherence space R in Example 2).
Then a function f:XβY is sequentially continuous if and only if
f is realized (i.e., tracked) by a stable map
F:XβΆstβY.
In passing, we have also observed in [MT16] a curious phenomenon:
when restricted to R,
a function f:RβR is uniformly continuous if and only if
f is realized by a linear map F:RβΆlinβ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 UβP(X)
such that βU=X.
Let U and V be covers of X.
We say that UrefinesV,
written Uβͺ―V,
if for every UβU there exists VβV with UβV.
We then have the meet (greatest lower bound) of U and V defined as
\{U\cap V:\mbox{U\in\mathcal{U}andV\in\mathcal{V}}\},
denoted by Uβ§V.
A family ΞΌ of covers of X is called a Hausdorff uniformity if
it satisfies the following:
(U1)
If U,VβΞΌ, then Uβ§VβΞΌ;
(U2)
If UβΞΌ and Uβͺ―V, then VβΞΌ;
(U3)
For every UβΞΌ, there exists VβΞΌ which star-refines U;
(U4)
Given any two distinct points x,yβX, there exists UβΞΌ such that
no Uβ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 X=(X,ΞΌXβ), a set X endowed with a (Hausdorff) uniformity.
Given any cover UβΞΌXβ and any points x,yβX,
we write β£xβyβ£<U if x,yβU for some UβU.
The condition (U4) can be restated as follows:
if β£xβyβ£<U for every UβΞΌXβ then x=y.
Let X=(X,ΞΌXβ) and Y=(Y,ΞΌYβ) be uniform spaces.
A uniformly continuous function from X to Y
is a function f:XβY satisfying that
for any VβΞΌYβ there exists UβΞΌXβ with
β£xβyβ£<UΒ βΉΒ β£f(x)βf(y)β£<V
for every x,yβX.
A function f:XβY is called uniform quotient if
it is surjective and
for every function g:YβZ to a uniform space Z,
g is uniformly continuous iff gβf:XβZ is.
A (uniform) basis of a uniformity ΞΌ is a subfamily Ξ²βΞΌ
such that for every UβΞΌ there exists VβΞ² with Vβͺ―U.
A (uniform) sub-basis of a uniformity ΞΌ is a subfamily ΟβΞΌ
such that the finite meets of members of Ο form a basis:
for every UβΞΌ there exist finitely many V1β,β¦,VnββΟ
with V1ββ§β―β§Vnββͺ―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 X is generated by
a countable basis
\mathcal{U}_{n}:=\{\mathcal{B}(x;2^{-n}):\mbox{x\in\mathbb{X}}\} (n=1,2,β¦),
where B(x;2βn) is the open ball of center x and radius 2βn.
On the other hand, every uniform space X=(X,ΞΌXβ)
can be equipped with a topological structure, called the uniform topology.
A set OβX is open with respect to the uniform topology iff
for every pβO there exists UβΞΌXβ such that
st({p},U)βO.
We will denote by Οutβ(ΞΌ) the uniform topology induced by a uniformity ΞΌ.
Given any uniformity ΞΌ on X, one can choose a basis Ξ² consisting of open covers.
It is easy to see that uniform continuity implies topological continuity:
if a function f:(X,ΞΌXβ)β(Y,ΞΌYβ) is uniformly continuous, then
it is continuous as a function f:(X,Οutβ(ΞΌXβ))β(Y,Οutβ(ΞΌYβ)).
We say that a uniformity ΞΌ on X is compatible with a topology Ο if
Ο=Οutβ(ΞΌ).
A topological space X=(X,Ο) is said to be uniformizable if
there exists a uniformity ΞΌ on X compatible with Ο.
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 X=(X,Ο)
can be equipped with the finest uniformity ΞΌfineβ which contains all of the uniformities compatible with Ο.
A fine uniform space is a uniform space endowed with the finest uniformity (compatible with its uniform topology).
For a Tychonoff space X=(X,ΟXβ)
we denote by Xfineβ=(X,ΞΌfineβ) the fine uniform space
compatible with ΟXβ.
The finest uniformity can be characterized as follows.
Let Tych be the category of
Tychonoff spaces and continuous maps,
and Unif be the category of
uniform spaces and uniformly continuous maps.
The fine functor F:TychβΆUnif,
which assigns to each Tychonoff space X
the fine uniform space Xfineβ,
is left adjoint to
the topologizing functor G:UnifβΆTych,
which assigns to each uniform space Y the topological space Yutβ endowed with
the uniform topology:
[TABLE]
Thus, for every Tychonoff space X and uniform space 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 β
β’
[-.3em]β£
β 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 X is a set of pairwise coherent tokens in X.
By abuse of notation, we denote by X the set of all cliques of the coherence space X.
We also use the notations Xfinβ and Xmaxβ for the sets of
all finite cliques and maximal cliques, respectively.
Given tokens x,yβ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ξ =y.
Notice that coherence and strict coherence are mutually definable from each other.
The coherence relation β
β’
[-.3em]β£
β on the token set X is naturally extended to X as:
a\,\raisebox{-1.99997pt}{\shortstack{\frown[β.3em]\smile}}\,b\iff a\cup b\in{\boldsymbol{X}} (a,bβX).
This is equivalent to say that any token in a is coherent with any token in b.
An anti-clique of X is a set of pairwise incoherent tokens in X,
that is, a subset aβX such that \neg(x\,\raisebox{0.0pt}{\shortstack{\frown\\
[-.3em]$$}}\,y) for every x,yβa.
We will use the symbol β
β£
[-.3em]β’
β 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 X is
a clique of the dual coherence space {\boldsymbol{X}}^{\perp}:=(X,\,\raisebox{-1.99997pt}{\shortstack{\smile[β.3em]\frown}}\,).
Given a subset AβX, we also write ΟScoβ
for the induced subspace topology on A.
Note that X is a T0β-space, and is countably-based due to the assumption that
the token set X is countable.
Moreover, (Xmaxβ,Ο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 R:
Example 2 (coherence space for real numbers)
Let D:=ZΓN,
where each pair (m,n)βD is identified with
a dyadic rational numberm/2n.
We use the following notations for x=(m,n)βD: den(x):=n;
Dnβ:={xβDβ£den(x)=n} for each nβN; and
[x]:=[(mβ1)/2n;(m+1)/2n].
Hence n=den(x) denotes the exponent of the denominator
of x, and [x] denotes the compact interval of R
with center x and width 2β(nβ1).
We then have a mapping ΟRβ:RmaxββR defined by
ΟRβ(a):=limnβββxnβ.
Definition 2.3** (stable and linear maps)**
Let X and Y be coherence spaces.
A function F:XβY is said to be stable, written F:XβΆstβ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βX.
A function F:XβY is said to be linear, written F:XβΆlinβY,
if it satisfies that a=βiβIβaiββΉF(a)=βiβIβF(aiβ),
for any clique aβX and any family of cliques {aiβ}iβIββX.
Here β means the disjoint union of cliques.
It is easy to see that linearity implies stability.
There are alternative definitions.
Given a function F:XβΆY, call (a,y)βXfinβΓY
a minimal pair of F if F(a)βy and there is no proper subset
aβ²βa such that F(aβ²)βy.
Denote by tr(F) the set of all minimal pairs, called the trace of F.
Now, F is a stable map iff it is β-monotone and satisfies that:
if F(a)βy, there is a uniquea0ββa such that (a0β,y)βtr(F).
If F is furthermore linear, preservation of disjoint unions ensures that
the finite part a0β must be a singleton.
Thus F is a linear map iff it is β-monotone and satisfies that:
if F(a)βy, there is a uniquexβa such that ({x},y)βtr(F).
By abuse of notation, we simply write tr(F) for the set
{(x,y)β£({x},y)β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:
β’
1:=β₯=({β},{(β,β)}).
β’
{\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}:=(({\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 β€).
It easily follows that Xβ₯βXβββ₯.
A notable feature of coherence spaces
is that they have two closed structures:
the category Stab of coherence spaces and stable maps
is cartesian closed;
while the category Lin of
coherence spaces and linear maps
equipped with (1,β,ββ,β₯)
is *-autonomous.
Moreover, the co-Kleisli category of the linear exponential comonad !
on Lin is isomorphic to Stab in such a way that
a stable map F:XβΆstβY can be
identified with a linear map G:!XβΆlinβY
so that tr(F)=tr(G)βXfinβΓ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:XβΆlinβY, we have tr(F)βXββY.
Conversely, given any clique ΞΊβXββY,
the induced linear map ΞΊ:XβΆlinβY is defined by
\widehat{\kappa}(a):=\{y\in Y:\mbox{(x,y)\in\kappaforsomex\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.
For any subset AβX, we write Aβ₯ for the set
\{\mathfrak{c}\in{\boldsymbol{X}}^{\perp}:\mbox{\forall a\in\mathcal{A}.a\perp\mathfrak{c}}\} of anti-cliques of X.
One can immediately observe the following:
(i) AβAβ₯β₯βX;
(ii) BβA implies Aβ₯βBβ₯; and
(iii) Aβ₯=Aβ₯β₯β₯.
As a consequence, A=Aβ₯β₯ iff
A=Bβ₯ for some BβXβ₯.
Definition 3.1** (coherence spaces with totality)**
A coherence space with totality is
a coherence space X endowed with a set TXββX
such that TXβ=TXβ₯β₯β, called a totality.
Cliques in TXβ are said to be total.
Thus defining a totality is essentially equivalent to defining a strict totality.
Notice that aβTXβ iff
for every cβTXβ₯β, aβ₯c.
In particular, aβTXββ iff
for every cβ(TXβ₯β)β
there exists xβa such that xβc and
dually, for every xβa there exists
cβ(TXβ₯β)β such that xβc.
Our use of totality is inspired by Kristiansen and Normann [KN97],
although they use a set of anti-cliques of !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
TRβ:=Rmaxβ is a totality on R:
it is easy to see that TRβ₯β={Dnβ:nβN},
hence TRβ₯β₯β=Rmaxβ=TRβ.
Moreover, TRββ=Rmaxβ
since aββa and aββRmaxβ imply aβ=a.
Example 4
The idea of Example 2 can be generalized to a more general class.
Let X=(X,ΞΌ) be a uniform space with a countable basis Ξ²={Unβ}nβNβ
consisting of countable covers.
A metrization theorem states that such a uniform space must be separable metrizable
(see [Ke75] for instance).
The separable metrizable space X is represented by a partial map
Ξ΄Xβ:βBXββX defined by
Ξ΄Xβ(a):=pβΊpββnβNβUnβ,
for every pβX and a={Unβ:nβN}β(BXβ)maxβ.
Let us define a totality by TBXββ:=dom(Ξ΄Xβ)β₯β₯.
Notice that we do not have
dom(Ξ΄Xβ)=dom(Ξ΄Xβ)β₯β₯ in general, even though
{Unβ:nβN}βTBXββ₯β,
since dom(Ξ΄Xβ)β₯β₯=(BXβ)maxβ.
To make dom(Ξ΄Xβ) itself a totality,
we have to assume that 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 TXββX and
TYββY be totalities of X and Y, respectively.
Define:
β’
TXβ₯β:=TXβ₯β;
T1β:=1maxβ.
β’
TXβYβ:=(TXββTYβ)β₯β₯,
where aβb:={(x,y):xβa,yβb} for
aβX and bβY, and
TXββTYβ is pointwise defined.
T!Xβ:=(!TXβ)β₯β₯, where
!a:={a0ββX:a0ββfinβa} for aβX,
and !TXβ is pointwise defined.
The connectives β and ! admit
βinternal completenessβ in the following sense.
Proposition 1
(TXββTYβ)β₯β₯β=TXβββTYββ* holds whenever
totalities TXβ,
TYβ,
TXβ₯β and
TYβ₯β are all nonempty.
(!TZβ)β₯β₯β=!(TZββ)
holds
for an arbitrary totality TZβ.*
A proof is given in Appendix.
Let us now turn to the morphisms.
Definition 3.2
A linear map F:XβΆlinβY is called total
if tr(F)βTXββYβ,
or equivalently if F preserves totality: F[TXβ]βTYβ.
A stable map F:XβΆstβY is total
if so is the corresponding linear map G:!XβΆlinβY given in Β§2.2.
Denote by LinTotβ
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 LinTotβ is a model of classical linear logic
(i.e., a β-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 LinTotβ is essentially following the idea of
tight orthogonality categoryT(Lin) induced by
the orthogonality relation β₯, which can be shown to be a
symmetric stable orthogonality in Lin.
The category StabTotβ
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 X with totality TXβ,
the set of strict total cliques TXββ is
endowed with both a topology and a uniformity:
the totality TXββ is a set of points endowed with
a Hausdorff topology ΟScoβΒ ,
while
the co-totality (TXβ₯β)β is a uniform sub-basis.
Moreover, the co-totality (T!Xβ₯β)β on !X
is a uniform basis, which induces the finest uniformity on TXββ.
To emphasize the uniformity aspect,
we will use the notations ΟXbβ:=(TXβ₯β)β and
Ξ²Xubβ:=(T!Xβ₯β)β.
Each uni-cover can be considered as an unbounded-cover consisting of singletons:
ΟXbββΞ²Xubβ
by cβΟXbββ¦{{x}:xβc}βΞ²Xubβ.
The families ΟXbβ and
Ξ²Xubβ indeed generate uniformities on TXββ:
Proposition 2
(TXββ,Ξ²Xubβ)*
satisfies axioms (U1),
(U3) and (U4), while
(TXββ,ΟXbβ)
satisfies
(U3) and (U4)
in Definition 2.1.*
Consequently,
Ξ²Xubβ, as basis,
generates a uniformity ΞΌXubβ,
called the unbounded uniformity, while
ΟXbβ, as sub-basis,
generates another uniformity
ΞΌXbββΞΌXubβ,
called the bounded uniformity.
The index 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 Ξ²Xubβ, the set
ΟXbβ is not closed under finite meets.
To make it closed, we have to extend it to
another set Ξ²XbββΞ²Xubβ which consists of
all finite meets of uni-covers:
c1ββ§β―β§cmβ:={{x1β,β¦,xmβ}βX:xiββciβΒ (1β€iβ€m)}β.
Notice that
c1ββ§β―β§cmβ
consists of cliques of size at most m. That is why
ΞΌXbβ is called bounded.
Although ΞΌXbβ and ΞΌXubβ are
different as uniformities, they do induce the same uniform topology.
Proposition 3
The (un)bounded uniformity on TXββ is compatible with
the Scott topology restricted to TXββ. That is,
Οutβ(ΞΌb)=Οutβ(ΞΌub)=ΟScoβ.
The unbounded uniformity ΞΌub is hence
compatible with, and finer than the bounded uniformity ΞΌb.
We can furthermore show that it is the finest uniformity on TXββ.
The omitted proofs are found in Β§0.A.2.
Theorem 3.4
(TXββ,ΞΌXubβ)* is a fine uniform space.*
Due to the internal completeness (Proposition 1), we have a bijection TXβββT!Xββ
defined by aβTXβββ!aβT!Xββ. Notice also that
Ξ²Xubβ=(T!Xβ₯β)β=Ο!Xbβ and
fine uniformity is preserved under uniform homeomorphisms.
These facts together allow us to prove:
Corollary 1
There is a uniform homeomorphism
(TXββ,ΞΌXubβ)β(T!Xββ,ΞΌ!Xbβ). As a consequence,
(T!Xββ,ΞΌ!Xbβ) is a fine uniform space.
We are now ready to establish uniform continuity of linear maps.
Theorem 3.5
A total linear map F:XβΆlinβY is strongly uniformly continuous:
for any bβΟYbβ
there exists aβΟXbβ
such that β£aβbβ£<aΒ βΒ β£F(a)βF(b)β£<b
for every a,bβTXββ.
As a consequence:
(i)
Every total linear map F:XβΆlinβY is uniformly continuous
w.r.t. the bounded uniformities.
(ii)
Every total stable map F:XβΆstβY is topologically continuous
w.r.t. the uniform topologies.
We thus obtain a functor
J:LinTotββUnif which sends
a coherence space with totality (X,TXβ)
to the uniform space (TXββ,ΞΌ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:StabTotββTych sending
(X,TXβ) to the Tychonoff space
(TXββ,Ο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):
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 B=NΟ 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 (X,Ο,S) is called a representation of S
if X is a coherence space and Ο:βXβS
is a partial surjective function.
Below, we write XβΆΟβS,
or simply Ο for (X,Ο,S).
Representations enable us to express abstract functions as stable maps:
Definition 4.2** (stable realizability)**
Let XβΆΟXββS and YβΆΟYββT be representations.
A function f:SβT is stably realizable
with respect to ΟXβ and ΟYβ
if it is tracked by a stable map F:XβΆstβY.
That is, F makes the following diagram commute:
[TABLE]
We denote by StabRep
the category of coherent representations and stably realizable functions.
With the help of Longleyβs theory of applicative morphisms [Lon94],
one can compare 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 TTERep be a category which embodies TTE:
the category of TTE-representations and continuously realizable functions.
Then TTERep is equivalent to a full coreflexive subcategory of 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 SpStabRep
of StabRep
which is equivalent to TTERep,
and introduced a concept of admissibility of representations in SpStabRep.
The main result of [MT16] is as follows:
Let X and Y be topological spaces represented by
admissible representations XβΆΟXββX and YβΆΟYββY
in SpStabRep.
A function f:XβΆY is stably realizable
if and only if it is sequentially continuous, that is,
it preserves the limit of any convergent sequence:
xnββxΒ βΒ f(xnβ)βf(x).
For instance, the coherent representation RβΆΟRββR defined in Example 2
belongs to SpStabRep and is admissible.
Consequently, a function f:RβR is stably realizable w.r.t. ΟRβ
iff it is continuous.
This equivalence can be generalized
to any countably-based T0β-space (and more generally, any qcb-space in the sense of [Si03])
as shown in [We00, Sc02].
Notice that given any topological space X, its admissible representations are
βinterchangeableβ: if X0ββΆΟ0ββX and X1ββΆΟ1ββX are adimissible,
then the identity map id:XβΆX is realized by stable maps F:X0ββΆstβX1β
and G:X1ββΆstβX0β
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:Rβ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 XβΆΟXββS and YβΆΟYββT be representations.
A function f:SβT is linearly realizable
with respect to ΟXβ and ΟYβ
if it is tracked by a linear map F:XβΆlinβY.
That is, F makes the diagram (4) commute.
We denote by 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 AβX of a coherence space X,
the set Aβ₯β₯ is a totality on X, hence is endowed with
a bounded uniformity (observed in Β§3).
Here is an extension lemma for the double negation totalities:
Lemma 1
Let AβX and BβY
be arbitrary (non-empty) sets of cliques.
If F:XβΆlinβY satisfies F[A]βB
then F is indeed total: F[Aβ₯β₯]βBβ₯β₯.
Given any coherent representation XβΆΞ΄XββS,
let us endow X with a totality TXβ:=dom(Ξ΄Xβ)β₯β₯.
From the above lemma, we obtain that f:SβT is linearly realizable if and only if
it is tracked by a total linear map F:XβΆlinβY.
So one can say that a linearly realizable function is in fact
a βtotally linearly realizableβ function.
Recall that dom(ΟRβ)β₯β₯=dom(ΟRβ)β₯β₯β=Rmaxβ and
dom(Ξ΄Xβ)β₯β₯=dom(Ξ΄Xβ)β₯β₯β=(BXβ)maxβ.
Theorem 4.6
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 PER(A) over an LCA A
is a linear category.
We can naturally define an LCA Coh such that
LinRepβPER(Coh).
Indeed, coherence spaces have linear type structures and
there also exists a universal type, from which
we obtain an untyped LCA Coh
by a linear variant of the Lietz-Streicher theorem [LS02].
Consequently, the category LinRepβPER(Coh)
is a linear category. Β
From the categorical structure of PER(Coh),
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 LinRep!β
and StabRep.
Then one can see that a standard representation BXββΆΞ΄XββX of
a separable metrizable space 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 X
does not depend on the chocie of a uniform basis, up to linear isomorphisms.
Moreover, we can show that:
Theorem 4.7
Let X and Y be separable metrizable spaces with
standard representations BXββΆΞ΄XββX and BYββΆΞ΄YββY.
Then every uniformly continuous function f:XβY is linearly realizable.
Let X and Y be separable metrizable spaces represented by the standard representations.
Provided that X is chain-connected,
a function f:Xβ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:BXββΆlinβBYβ
which tracks f, hence F is uniformly continuous w.r.t. the bounded uniformities by Theorem
3.5.
Any standard representation Ξ΄Yβ is also uniformly continuous
as a partial map Ξ΄Yβ:βBYββY,
so is the composition Ξ΄YββF:dom(Ξ΄Xβ)βY.
Since Ξ΄Xβ is a uniform quotient by Lemma 15 in Β§0.A.6,
uniform continuity of fβΞ΄Xβ=Ξ΄YββF
implies that of f.
This result substantially and systematically
generalizes the already mentioned result in [MT16]:
a function f:RβR is linearly realizable w.r.t. Ο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 Coh, constructed
from the universal coherence spaceU in
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 U in fact resides in 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: TXββYβ=TXββYβ₯β₯β.
Proof
Notice that (XββY)β₯=XβYβ₯
and
ΞΊ(a)β₯c iff
ΞΊβ₯aβc for
any ΞΊβXββY, aβX and cβYβ₯.
It follows that ΞΊβTXββYβ iff
ΞΊ(a)β₯c for any
aβX and cβTYβ₯β iff ΞΊβ(TXββTYβ₯β)β₯.
The following lemmas prove the internal completeness of β and !
(Proposition 1).
Lemma 3
Given aβTXβ₯β and
bβTYβ₯β, let
aβb:={(x,y):xβa,Β yβb}.
Then
aβbβ(TXββTYβ)β₯.
Proof
First of all, aβb is an anti-clique
of XβY.
Indeed, given (x,y),(xβ²,yβ²)βaβb with (x,y)ξ =(xβ²,yβ²),
either xξ =xβ² or yξ =yβ². Assume that xξ =xβ².
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βTXβ and dβTYβ, we have
cβ₯a and dβ₯b, from which we
conclude
cβdβ₯aβb.
Lemma 4
TXβββTYβββ(TXββTYβ)β₯β₯β.
Proof
Let aβTXββ and
bβTYββ. It is clear that
aβbβ(TXββTYβ)β₯β₯. Too see strictness,
let (x,y)βaβb. Then there are
cβTXβ₯β and
dβTYβ₯β such that
xβc and yβd.
Hence
(x,y)βcβd and
cβdβ(TXββTYβ)β₯ by Lemma 3.
Lemma 5
Assume that TXβ₯β and
TYβ₯β are not empty.
Given cβ(TXββTYβ)β₯β₯, let
c1:={x:(x,y)βc\mboxforsomey}
and
c2:={y:(x,y)βc\mboxforsomex}.
Then
c1βTXβ and
c2βTYβ.
Proof
Let aβTXβ₯β.
Since we suppose that TYβξ =β
there is bβTYβ₯β
and aβbβ(TXββTYβ)β₯ by Lemma 3.
Hence cβ₯aβb and
we conclude that c1β₯a.
Lemma 6
Assume that TXβ and
TYβ are not empty.
Given cβ(TXββTYβ)β₯, let
c1:={x:(x,y)βc\mboxforsomey}
and
c2:={y:(x,y)βc\mboxforsomex}.
Then
c1βTXβ₯β and
c2βTYβ₯β.
Proof
Similarly.
Lemma 7
Assume that TXβ,
TYβ,
TXβ₯β and
TYβ₯β are all nonempty. Then
(TXββTYβ)β₯β₯ββTXβββTYββ.
Proof
Let cβ(TXββTYβ)β₯β₯β.
We prove that c1βTXββ
(and c2βTYββ). Since
cβc1βc2 and c1βc2 is strict in
(TXββTYβ)β₯β₯ by Lemma
4, we will be able to conclude that c=c1βc2βTXβββTYββ by strictness
of c.
Totality of c1 is due to Lemma 5.
To show strictness, let xβc1, so that (x,y)βc for some y.
Since c is strict, there is dβ(TXββTYβ)β₯ such that (x,y)βd.
We then have xβd1 and
d1βTXβ₯β by Lemma 6.
We have established the internal completeness of β.
Let us next proceed to connective !.
Lemma 8
Given c1β,β¦,cnββTXβ₯β,
let
[TABLE]
Then β§iβciββ(!TXβ)β₯.
In particular, β§c:={{x}βX:xβc}β(!TXβ)β₯.
Proof
Each β§iβciβ consists of finite cliques of X,
namely tokens of !X, which are pairwise incoherent in !X.
Indeed, given distinct {x1β,β¦,xnβ},{y1β,β¦,ynβ},
there is i such that xiβξ =yiβ and xiβ,yiββciβ.
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
β§iβciββ(!X)β₯.
It is easy to see that
every !aβ!TXββ belongs to
(!TXβ)β₯β₯. For strictness, let
a0β={x1β,β¦,xnβ}β!a. Since aβTXββ, there are
ciββTXβ₯β
such that
xiββciβ for each 1β€iβ€n.
Applying the previous lemma, we obtain
β§iβciββ(!TXβ)β₯, which contains a0β.
Let Ξ±β(!TXβ)β₯β₯β.
We prove that !Ξ±1βΞ±. Since
!Ξ±1β(!TXβ)β₯β₯β by combining Lemmas 9 and 10,
we will be able to conclude Ξ±=!Ξ±1β!TXββ by strictness of Ξ±.
Let a={x1β,β¦,xmβ}.
By assumption, there exists bβTXββ with bβa.
By strictness of b, each xiβ is contained in some ciββTXβ₯β, which we may assume is strict. Hence we have
aβc1ββ§β―β§cmβ.
The next lemma is used to cut down and divide the set TXββ.
Let XβStabSTotβ be a coherence space with totality.
Since (Ξ·cohβ)Xβ(a):=!a for every aβX,
(IΞ·cohβ)Xβ:(TXββ,ΟScoβ)β(T!Xββ,ΟScoβ) gives the bijection aβTXβββ¦!aβT!Xββ given in Proposition 1.
On the other hand, (Ξ·unifβ)IXβ:(TXββ,ΟScoβ)β(TXββ,ΟScoβ) is the identity,
therefore, IΞ·cohβ=(Ξ·unifβ)Iβ up to isomorphisms.
Let YβLinSTotβ be a coherence space with totality.
Recall that (Ο΅cohβ)Yβ:!YβΆlinβY is the dereliction
so that (Ο΅cohβ)Yβ(!a):=a for every aβY.
Hence (JΟ΅cohβ)Yβ:(T!Yββ,ΞΌ!Ybβ)β(TYββ,ΞΌYbβ)
also gives the uniform homeomorphism in Proposition 1.
Similarly, (Ο΅unifβ)JYβ:(TYββ,ΞΌfineβ)β(TYββ,ΞΌYbβ) is the identity,
therefore, we obtain JΟ΅cohβ=(Ο΅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:(XββY)βΆlinβZ is
uniformly continuous at single points:
for every cβΟZbβ,
there exist aβTXββ and a total linear map G:YβΆlinβZ
such that β£F(ΞΊ)βG(ΞΊ(a0β))β£<c for every ΞΊβTXββYββ.
Proof
By Theorem 3.5,
there exists fβΟXββYbβ such that
β£ΞΊβΞΊβ²β£<fΒ βΒ β£F(ΞΊ)βF(ΞΊβ²)β£<c
for all ΞΊ,ΞΊβ²βTXββYββ.
Notice that (XββY)β₯=XβYβ₯.
Hence ΟXββYbβ=TXβββ(TYβ₯β)β by Proposition 1,
so f=a0ββb for some a0ββTXββ and bβΟYbβ.
We now have β£ΞΊβΞΊβ²β£<a0ββbββ£F(ΞΊ)βF(ΞΊβ²)β£<c.
Let cβTXββ be an arbitrary uni-cover,
and define ΞΈβYβΆlinβ(XββY) as
\mathsf{tr}(\theta):=\{(y,(x,y)):\mbox{x\in\mathfrak{c},y\in Y}\}.
It is easy to see that ΞΈ is strictly total and
satisfies that ΞΈ(b)(a):=b for all aβTXβ and bβTYβ.
Then G:=FβΞΈ:YβΆlinβZ is a total linear map satisfying our requirement:
By letting b0β:=ΞΊ(a0β),
[TABLE]
What is interesting here is that the uniform structures on the constructed spaces
are determined by purely logical rules: for instance (XββY)β₯=XβYβ₯.
The following lemma indicates that Ξ΄Xβ is a representative example of linearish representations.
Lemma 14
For any subspace X0ββX and
any linearish representation XβΆΞ³βX0β,
there exists a linear map F:XβΆlinβBXβ with Ξ΄XββF=Ξ³.
In particular, it immediately follows that
standard representations of X are all isomorphic by letting X0β:=X, hence
they do not depend on the choice of uniform basis Ξ².
(i) F(a)βBXβ for every aβX.
Let (n,U),(m,V)βF(a) with (n,U)ξ =(m,V).
This means that
there exist
xβanβ, and wβamβ
such that Ο(x,n)=U, Ο(w,m)=V and
x,wβ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βanβ.
Hence U=Ο(x,n)=Ο(z,m)=V, contradicting
the assumption, so nξ =m.
Applying Lemma 14 to BXββΆΞ΄XββXβΆfβY0β,
we obtain a (total) linear map
F:BXββΆlinβBYβ such that Ξ΄YββF=fβΞ΄Xβ.
This concludes Theorem 4.7.
Let {Unβ:nβN} be a countable basis of X.
All we have to show is that
each uni-cover cβΟBXβbβ is of the form
c={(n,U):UβUnβ} for some nβN.
Then Ξ΄Xβ[c]=Unβ, hence they generate the uniformity on X.
Let cβΟBXβbβ be a uni-cover of dom(Ξ΄Xβ).
Since cξ =β , one can fix a token (n,Unβ)βc.
Repeating this argument, we obtain (n,U)βc for all UβUnβ.
0.A.7 Some Constructions of Coherent Representations
Typical constructions of coherent representations are naturally given as follows.
Given XβΆΟXββS and YβΆΟYββT, define:
β’
XβYβΆ[ΟXββΟYβ]βSΓT
is defined as
dom([ΟXββΟYβ]):=dom(ΟXβ)βdom(ΟYβ) and
[ΟXββΟYβ](aβb):=(ΟXβ(a),ΟYβ(b)),
where dom(Β ) means the domains of representations (as partial maps).
β’
XββYβΆ[ΟXβββΟYβ]βLR(ΟXβ,ΟYβ) is
defined as follows. Define [ΟXβββΟYβ]:βXββYβΆTS by
[TABLE]
LR(ΟXβ,ΟYβ)βYX is the range of [ΟXβββΟYβ], which consists of
linearly realizable functions.
β’
!XβΆ[!ΟXβ]βS is
defined as dom([!ΟXβ]):=!dom(ΟXβ)
and
[!ΟXβ](!a):=ΟXβ(a)
for every aβdom(ΟXβ).
Unfortunately,
the total extension lemma (Lemma 1) is no longer available for
these constructions.
For instance, we do not have
dom([ΟXββΟYβ])β₯β₯=TXβYβ in general,
where TXβYβ
is the tensor of the totalities TXβ and TYβ
which are the double negations of dom(ΟXβ) and dom(ΟYβ) respectively.
To avoid this, we consider the following condition.
A coherent representation XβΆΟXββS
is said to be classical if
dom(ΟXβ)=dom(ΟXβ)β₯β₯β
(i.e. the domain is a totality on X and consists of strict total cliques).
As noted in Example 4,
a complete space X has a classical standard representation Ξ΄Xβ.
Then it is easy to see that
if ΟXβ and ΟYβ are classical,
so are [ΟXββΟYβ] and [!ΟXβ],
due to the internal completeness (Proposition 1).
Although [ΟXβββΟYβ] is not classical,
one can naturally restrict it as follows.
Since [ΟXβββΟYβ](ΞΊ)=[ΟXβββΟYβ](ΞΊβ)
for every ΞΊβTXββYβ,
the strict restriction [ΟXβββΟYβ]β:TXββYβββLR(ΟXβ,ΟYβ)
is well-defined.
These representations are indeed compatible with the uniformities induced by totalities:
dom([ΟXββΟYβ])β₯β₯=TXβYβ,
dom([ΟXβββΟYβ]β)β₯β₯=TXββYβ and
dom([!ΟXβ])β₯β₯=T!Xβ,
where TXβ:=dom(ΟXβ) and TYβ:=dom(ΟYβ).
Bibliography35
The reference list from the paper itself. Each links out to its DOI / PubMed record.
1[AHS 02] S. Abramsky, E. Haghverdi, P.J. Scott. Geometry of interaction and linear combinatory algebras, Math. Struct. in Comput. Sci. 12(5):625-665, 2002.
2[AL 00] S. Abramsky and M. Lenisa. A fully complete PER model for ML polymorphic types. CSLβ2000 Springer LNCS 1862: 140-155, 2000.
3[AL 05] S. Abramsky and M. Lenisa. Linear realizability and full completeness for typed lambda-calculi. Ann. Pure Appl. Logic 134(2-3): 122-168, 2005.
4[As 90] A. Asperti. Stability and Computability in Coherent Domains. Information and Computation 86: 115-139, 1990.
5[Ba 00] A. Bauer. The Realizability Approach to Computable Analysis and Topology . Ph D thesis, School of Computer Science, Carnegie Mellon University, 2000.
6[Ba 02] A. Bauer. A relationship between equilogical spaces and type two effectivity. Mathematical Logic Quarterly 48(S 1): 1-15, 2002.
7[Ba 05] A. Bauer. Realizability as the Connection between Computable and Constructive Mathematics. In Proc. of CCA 2005, Kyoto, Japan , 2005.
8[Be 93] U. Berger. Total sets and objects in domain theory. Annuals of Pure and Applied Logic 60: 91-117, 1993.