Electronic Notes in Theoretical Computer Science 83 (2004)

URL: http://www.elsevier.nl/locate/entcs/volume83.html 18 pages

Intensional double glueing, biextensional collapse, and the Chu construction

Dominic Hughes

Computer Science Department Stanford University

Abstract

The superficial similarity between the Chu construction and the Hyland-Tan double glueing construction G has been observed widely. This paper establishes a more formal mathematical relationship between the two.

We show that double glueing on relations subsumes the Chu construction on sets: we present a full monoidal embedding of the category chu(Set, K) of biextensional Chu spaces over K into G(Rel^{K}), and a full monoidal embedding of the category Chu(Set, K) of Chu spaces over K into IG(Rel^{K}), where we define IG, the intensional double glueing construction, by substituting multisets for sets in G.

We define a biextensional collapse from IG to G which extends the familiar notion on Chu spaces. This yields a new interpretation of the monic specialisation implicit in G as a form of biextensionality.

1 Introduction

The Chu construction [2] and the Hyland-Tan double glueing construction G [21] have each produced models of multiplicative linear logic [8] which are fully complete in the sense of Abramsky and Jagadeesan [1]. The following superficial similarity between the two constructions has been observed widely. Each starts with a category ℂ (with appropriate structure) and builds a starautonomous category ℂ′ (hence a model of multiplicative linear logic [20]) in which:

• An object of ℂ′ possesses ‘points’ and ‘copoints’ in ℂ.

• Duality in ℂ′ interchanges points and copoints.

• A morphism in ℂ′ transforms points forwards and copoints backwards.

This paper establishes a more formal mathematical relationship between the two constructions.

\begin{matrix}c \\ ◯ \end{matrix}2004 Published by Elsevier Science B. V.

Hughes

Relating the Chu construction and double glueing  Fig. 1
Chu(Set, K)

IG(Rel^{K})

chu(Set, K)

G(Rel^{K})

[figure] F^{+}

[figure] F

[figure: ] [figure: ]

“ Chu = chu + multiplicity ”
“ IG = G + multiplicity ”
“ F^{+} = F + multiplicity ”

Both squares in the diagram commute, hooked arrows are full embeddings, and ( ) denotes biextensional collapse. The full embeddings F and F^{+} are monoidal. See main text for details.

Together with the commentary below, Figure 1 summarises the results presented in this paper. The first result corresponds to the lower edge in the commuting square of Figure 1:

(1) The Hyland-Tan double glueing construction G on relations subsumes the biextensional Chu construction chu on sets.

More precisely, we define (section 3) a full monoidal embedding F of chu(Set,K) into G(Rel^{K}), where Set is the category of sets, K is any set, and Rel is the category of sets and binary relations. (In writing the functor category Rel^{K} we view K as a discrete category.) The biextensional Chu construction chu (lower case, following Pratt [17] and Barr [4]), is the Chu construction followed by restriction to biextensional (i.e., separated and extensional) objects [4,5]. Following Pratt (e.g. [17]), the objects of Chu(Set, K), and hence also of the biextensional full subcategory chu(Set, K), are commonly known as Chu spaces over K. Figure 2 (overleaf) sketches the idea behind the embedding with a simple example.

The remaining results stem from the point of view captured by the slogan

“ Chu = chu + multiplicity ”

or “every Chu space can be viewed as an underlying biextensional Chu space together with multiplicity information”. To clarify our slogan, consider the Chu space A below-left (drawn according to the conventions of Figure 2):

\begin{aligned}& x & y & z \\ a & 0 & 0 & 0 \\ b & 0 & 0 & 0 \\ c & 0 & 0 & 0 \\ d & 0 & 1 & 1 \\ e & 0 & 1 & 1 \end{aligned}  ⇝  \begin{aligned}& \{x\} & \{y, z\} \\ \{a, b, c\} & 0 & 0 \\ \{d, e\} & 0 & 1 \end{aligned}

Sketch of F : chu(Set, K) ↪ G(Rel^{K})  Fig. 2

[figure: chu(Set, K); \begin{matrix}x & y \\ 0 & 0 & a \\ 0 & 1 & b \end{matrix}; \begin{aligned}& v & w \\ c & 0 & 0 \\ d & 0 & 1 \\ e & 1 & 1 \end{aligned}; g; f; F; F; G(Rel^{K}); 0; 0; 0; 1; 0; 0; 0; 1; 1; 1; R]

Top-right is a morphism (f, g) from a Chu space A (with two points a, b and two copoints (or states) x, y) to a Chu space B (with three points c, d, e and two copoints v, w). The matrix (or pairing) ⟨−, −⟩ of each is given by the tables (e.g. ⟨a, y⟩ = 0, ⟨e, w⟩ = 1; assume 0, 1 ∈ K.) The graphs of f (forwards) and g (backwards) are shown (e.g. f(b) = e, g(w) = y). Underneath is the image of (f, g) : A → B in G(Rel^{K}) under F, a binary relation R between the four tokens of F (A) (three 0-tokens and one 1-token) and the six tokens of F (B) (three 0-tokens and three 1-tokens). The four edges of R are shown curved and dotted. By definition, an object of G(ℂ) has ‘values’ and ‘covalues’, which in this case (ℂ = Rel^{K}) are sets of tokens. Values are circumscribed by a rounded border [figure], and covalues by an oblong border . (Thus F (A) has two values and two covalues (each with two tokens), and F (B) has three values (each with two tokens) and two covalues (each with three tokens)). The definition of F on objects is as follows: matrix entries become tokens, matrix rows (resp. columns) become values (resp. covalues). On morphisms: R is a ‘conjunction’ of f and g (e.g. R relates the top-right token of F (A) to the top-right token of F (B) because f(a) = c (“f(top) =top”) and g(w) = y (“g(right) = right”)).

Since A has duplicate rows/columns (e.g. two copies of row 011), it is not biextensional. The slogan “Chu = chu+multiplicity” expresses the idea that A can be encoded as in the table to the right of A: a biextensional Chu space Ã (two distinct rows (00 and 01) and two distinct columns), with information regarding multiplicity (i.e., regarding duplication of rows and columns in the original Chu space A).

With this perspective in mind, we observe (section 3.4) that the full monoidal embedding F : chu(Set, K) ↪ G(Rel^{K}) seems not to extend in any obvious way to a full embedding of the whole of Chu(Set, K) into G(Rel^{K}) because there is not enough ‘room’ in G to retain multiplicity information from Chu. To make room, we define (section 4) a variant IG of G, which we call the intensional double glueing construction, by analogy with our earlier Chu slogan:

IG = G + multiplicity.

We follow this prescription literally: where G attaches sets of points and copoints, IG attaches multisets of points and copoints. Our second result (section 5) corresponds to the upper edge in the commuting square of Figure 1:

(2) The intensional double glueing construction IG on relations subsumes the Chu construction on sets.

Specifically, we extend F : chu(Set, K) ↪ G(Rel^{K}) to a full monoidal embedding F^{+} : Chu(Set, K) ↪ IG(Rel^{K}) in three steps, as illustrated by the dotted arrows in Figure 3, overleaf: given a Chu space A, to define F^{+}(A) first discard multiplicity by taking the biextensional collapse Ã of A (the downward dotted arrow in Figure 3), then use F to embed Ã into G(Rel^{K}) (the left-to-right dotted arrow), and finally restore any multiplicities that were present before the collapse (the upward dotted arrow), using the multisets available in IG(Rel^{K}). (Note that the upwards “restore multiplicity” arrow is not a functor, since it uses multiplicity information about A back in Chu(Set, K).) Thus the definition of F^{+} adheres to the pattern of our previous two slogans:

F^{+} = F + multiplicity

.

In section 4.1 we define a functorial biextensional collapse ( ) from IG to G by collapsing multisets to sets. Our third and final result (section 6) is:

(3) Biextensional collapse on double glued categories subsumes the extant notion on Chu spaces.

This corresponds to the square in Figure 1 commuting from top-left to bottomright.

Biextensional versus intensional models. In the language of Hyland and Schalk’s comprehensive study of glueing and orthogonality for models of linear logic [9], IG is the result of omitting the monic specialisation implicit in G. Hence our results provide a new interpretation of this monic specialisation as a

Defining F^{+} by “ F^{+} = F + multiplicity ”  Fig. 3

[figure: Chu(Set, K); IG(Rel^{K}); chu(Set, K); G(Rel^{K}); F^{+}; F; discard; multiplicity; restore; multiplicity]

\begin{aligned}& x & y & z \\ a & 0 & 0 & 0 \\ b & 0 & 0 & 0 \\ c & 0 & 0 & 0 \\ d & 0 & 1 & 1 \\ e & 0 & 1 & 1 \end{aligned}

discard multiplicity

F^{+}

\begin{aligned}& \{x\} & \{y, z\} \\ \{a, b, c\} & 0 & 0 \\ \{d, e\} & 0 & 1 \end{aligned}

F [figure: 0; 0; 0; 1]

restore multiplicity

[figure: 0; 0; 0; 1]

form of biextensionality. Correspondingly, one can view models of linear logic constructed using G, such as those of Hyland, Schalk, and Tan [21,9], and the work in progress of Blute, Hamano and Scott on double glued hypercoherences [7], as biextensional. In constrast, the Chu space model of [6] can be seen as intensional (non-biextensional).

This distinction between biextensional and intensional models of linear logic suggests further avenues for research, such as exploring the intensional counterparts of the aforementioned models based on G, and the general relationship between intensional and biextensional linear logical structure.

2 Background material

2.1 Chu spaces

A Chu space over a set K is an object of the category Chu(Set, K), the result of applying Barr’s construction Chu [2] to the category of sets with the set K as dualising object. Chu spaces have a remarkably rich structure, even in the simple case of K a two-element set 2 = {0, 1}. Lafont and Streicher [12] made the elegant observation that the category of topological spaces embeds fully into Chu(Set, 2), as does Girard’s category of coherence spaces [8]. Via logical relations, Chu(Set, 2) yields a fully complete model for multiplicative linear logic [6]. Pratt has uncovered connections between Chu spaces and a wide variety of fields [15,16,18,19].

The structure of the star-autonomous category Chu(Set, K) is as follows. We adopt much of Pratt’s terminology and notation [17].

• Objects. Triples (A, r, X), where A a set of points, X a set of copoints^{1} , and r is a function A × X → K, the matrix or pairing.

• Morphisms. A morphism (A, r, X) → (B, s, Y) is a pair (f, g) of functions f : A → B and g : Y → X satisfying the adjointness condition:

r(a, g(y)) = s(f(a), y) for all points a ∈ A and copoints y ∈ Y.

• Duality. (A, r, X)^{⊥} = (X, r^{∘}, A), where r^{∘}(x, a) = r(a, x).

• Internal hom and tensor. Given A = (A, r, X) and B = (B, s, Y),

A −∘ B = ( hom(A, B), ev, A × Y )
ev((f, g), ⟨a, y⟩) = r(a, g(y)) ( = s(f(a), y)) ∈ K
A ⊗ B = (A × B, ev^{∘}, hom(A, B^{⊥}))
ev^{∘}(⟨a, b⟩, (h, k)) = r(a, k(b)) ( = s(b, h(a))) ∈ K

• Tensor unit. (1, π_{K}, K), where 1 = {0} and π_{K}(0, k) = k ∈ K.

2.1.1 Biextensional collapse Fix a Chu space A = (A, r, X) over K. Points a, a′ ∈ A are equivalent, denoted a ∼ a′, if they are indistinguishable in terms of their interaction with copoints: r(a, x) = r(a′, x) for all copoints x ∈ X. For example, points a and c of the 5-by-3 Chu space in Figure 3 (page 5) are equivalent. Dually, copoints x, x′ ∈ X are equivalent, also denoted x ∼ x′, if they are indistinguishable in terms of their interaction with points: r(a, x) = r(a, x′) for all points a∈A. For example, copoints y and z of the 5-by-3 Chu space in Figure 3 are equivalent. We say that A is separated if it has no distinct equivalent points (a ∼ a′

1 We deviate from Pratt’s terminology states in order to emphasise the duality.

only if a = a′), extensional if it has no distinct equivalent copoints (x ∼ x′ only if x = x′), and biextensional if it is separated and extensional. (This terminology is in line with the view of Chu(Set, 2) as a category of generalised topological spaces.) Following Pratt [17] and Barr [4], we write chu(Set, K) for the biextensional full subcategory of Chu(Set, K).

Write q̃ for the ∼-equivalence class of a point or copoint q, and write Ã and X̃ for the quotients of A and X by ∼, i.e.,

\begin{matrix}Ã = & A/∼ ≡ & \{ ã : a ∈ A \} \\ X̃ = & X/∼ ≡ & \{ x̃ : x ∈ X \}. \end{matrix}

Define the quotient r̃: Ã × X̃ → K of r : A × X → K by r̃(ã, x̃) = r(a, x). (Overloading the tilde notation α̃ streamlines our later presentation of the main results. Pronounce α̃ as “collapse α”, whatever the type of α.) The biextensional collapse of a Chu space A = (A, r, X) is

Ã = (Ã, r̃, X̃).

For example, the bottom-left (2-by-2) Chu space of Figure 3 (page 5) is the biextensional collapse of the 5-by-3 Chu space above it. Biextensional collapse is functorial from Chu(Set, K) to chu(Set, K): given A = (A, r, X) and B = (B, s, Y) in Chu(Set, K) and a morphism m = (f, g) from A to B, the biextensional collapse of m is m̃ = (f̃, g̃) : Ã → B̃, where f̃\binom{}{a} = f̃(a) and g̃(ỹ) = g̃(y).

The biextensional full subcategory chu(Set, K) of Chu(Set, K) is starautonomous with tensor ˜⊗ and internal hom ˜−∘ inherited from Chu(Set, K) by biextensional collapse: A ˜⊗ B = { \atop A⊗B} and A ˜−∘ B = { \atop A−∘B}.

2.2 The Hyland-Tan double glueing construction G

The double glueing construction G, abstracting Loader’s category LLP of linear logical predicates [11], was suggested by Hyland and developed in Tan’s Ph.D. thesis [21]. When applied to a compact closed category ℂ [10], the construction produces a star-autonomous category G(ℂ) with a more refined structure: G(ℂ) has a distinct tensor and par, and supports the mix rule iff (in ℂ) the identity is the only morphism I → I. Tan shows how full completeness proofs for G(ℂ) can be ‘lifted’ from the underlying compact closed category ℂ. In particular, she obtains a more abstract proof of Loader’s full completeness result for LLP ≅ G(Rel).

Let ℂ be a star-autonomous category with tensor ⊗ : ℂ × ℂ → ℂ, tensor unit I, duality (−)^{⊥} : ℂ^{op} → ℂ, and internal hom −∘ : ℂ^{op} × ℂ → ℂ. Let ⊥ = I^{⊥}, the dual of the tensor unit. For any object U of ℂ, define a U-value to be a morphism I → U and a U-covalue to be a morphism U → ⊥, and write

(−)_{∗} ≡ ℂ(I, −) : ℂ → Set  (the values functor)
(−)^{∗} ≡ ℂ(−, ⊥) : ℂ → Set^{op} (the covalues functor)

Thus U_{∗} is the set of U-values and U^{∗} is the set of U-covalues. A morphism R : U → V maps values forwards (as R_{∗}) and covalues backwards (as R^{∗}):

\begin{aligned}U_{∗} & \underrightarrow{R_{∗}} & V_{∗} & R_{∗}(a) & = & R ∘ a \\ U^{∗} & \overleftarrow{R^{∗}} & V^{∗} & R^{∗}(y) & = & y ∘ R \end{aligned}  [figure: U; V; I; ⊥; a; R_{∗}(a); y; R^{∗}(y); R]

The star-autonomous structure of G(ℂ) is as follows.

• Objects. Triples (U, A, X) where · U is an object of ℂ, · A is a set of U-values (i.e., A ⊆ U_{∗} = ℂ(I, U)), · X is a set of U-covalues (i.e., X ⊆ U^{∗} = ℂ(U, ⊥)).

• Morphisms. A morphism (U, A, X) → (V, B, Y) is a morphism R : U → V in ℂ such that R_{∗}(A) ⊆ B and R^{∗}(Y) ⊆ X (i.e., such that R_{∗}(a) ∈ B whenever a ∈ A, and R^{∗}(y) ∈ X whenever y ∈ Y).

• Duality. (U, A, X)^{⊥} = (U^{⊥}, X, A), modulo (U^{⊥})_{∗} ≅ U^{∗} and (U^{⊥})^{∗} ≅ U_{∗}.

• Internal hom and tensor. Given A = (U, A, X) and B = (V, B, Y),

\begin{aligned}A −∘ B & = & (U −∘ V, hom(A, B), A ⊗ Y^{⊥}) \\ A ⊗ B & = & (U ⊗ V, A ⊗ B, hom(A, B^{⊥})) \end{aligned}

where

hom(A, B) ⊆ ℂ(U, V) ≅ (U −∘ V)_{∗}
A ⊗ Y^{⊥} = { a ⊗ y^{⊥} : a ∈ A and y ∈ Y }
⊆ ℂ(I ⊗ I, U ⊗ V^{⊥}) ≅ (U −∘ V)^{∗}
A ⊗ B = { a ⊗ b : a ∈ A and b ∈ B }
⊆ ℂ(I ⊗ I, U ⊗ V) ≅ (U ⊗ V)_{∗}
hom(A, B^{⊥}) ⊆ ℂ(U, V^{⊥}) ≅ (U ⊗ V)^{∗}.

• Tensor unit. (I, {id_{I}}, I^{∗} = ℂ(I, ⊥) ).

The original presentation of G in [21] applied to a compact closed category ℂ; the above generalisation to star-autonomous ℂ is immediate.

Proposition 2.1 G(ℂ) is star-autonomous, with the above structure.

Proof. See Hyland and Schalk [9], pages 28–9. □

3 The biextensional full monodial embedding

In this section we present a full and faithful monoidal functor

F : chu(Set, K) → G(Rel^{K}).

This functor runs from left to right in Figure 1 on page 2. We first review the (degenerate, compact closed) star-autonomous structure of Rel^{K} (section 3.1), then calculate G(Rel^{K}) (section 3.2). The embedding is defined in section 3.3.

3.1 The category Rel^{K} of relations over K

In writing Rel^{K} we interpret the set K as a discrete category. To smooth the presentation of our main results, we identify an object ⟨U_{k}⟩_{k∈K} of the functor category Rel^{K}, a K-indexed family of sets, with the pair (U, r), where U is the disjoint union of the U_{k} and r : U → K is r(u) = k iff u ∈ U_{k}(↪ U). Given functions U →^{r} K ←^{s} V, we use the following notation for K-fibred product (pullback):

\begin{aligned}U ×_{K} V & = & \{ ⟨u, v⟩ : r(u) = s(v) \} ⊆ U × V \\ r ×_{K} s (u, v) & = & r(u) ( = s(v)) ∈ K. \end{aligned}

The (degenerate, compact closed) star-autonomous structure of Rel^{K} is:

• Objects. Pairs (U, r) comprising a set U of tokens and a K-colouring function r : U → K.

• Morphisms. A morphism (U, r) → (V, s) is a binary relation R ⊆ U × V between tokens which respects colour: uRv only if r(u) = s(v).

• Duality. Trivial: (U, r)^{⊥} = (U, r).

• Internal hom and tensor. Both are given by K-fibred product (pullback): (U, r) −∘ (V, s) = (U, r) ⊗ (V, s) = (U ×_{K} V, r ×_{K} s).

• Tensor unit. (K, id_{K}).

3.2 The category G(Rel^{K}) of double glued relations over K

Applying the Hyland-Tan double glueing construction to Rel^{K} yields the starautonomous category G(Rel^{K}). To reduce bracket clutter, we flatten the triplets ((U, r), A, X) coming out of the application of G.

• Objects. Tuples (U, r, A, X) where · U is a set of tokens, · r : U → K is a colouring function, · A is a set of subsets of U, the values, · X is a set of subsets of U, the covalues.

• Morphisms. A morphism R : (U, r, A, X) → (V, s, B, Y) is a binary relation R ⊆ U × V between tokens which · respects colour, i.e., uRv only if r(u) = s(v); · maps values to values by direct image, i.e., for all a ∈ A,

R_{∗}(a) ≡ { v ∈ V : uRv for some u ∈ a }

is in B; · maps covalues to covalues by inverse image, i.e., for all y ∈ Y,

R^{∗}(y) ≡ { u ∈ U : uRv for some v ∈ y }

is in X.

• Duality. (U, r, A, X)^{⊥} = (U, r, X, A), exchanging values and covalues.

• Internal hom and tensor. Given A = (U, r, A, X) and B = (V, s, B, Y),

\begin{aligned}A −∘ B & = & ( U ×_{K} V, r ×_{K} s, hom(A, B), A ×_{K} Y ) \\ A ⊗ B & = & ( U ×_{K} V, r ×_{K} s, A ×_{K} B, hom(A, B^{⊥}) ) \end{aligned}

where

\begin{aligned}A ×_{K} Y & = & \{ a ×_{K} y : a ∈ A and y ∈ Y \} & ⊆ & U ×_{K} V \\ A ×_{K} B & = & \{ a ×_{K} b : a ∈ A and b ∈ B \} & ⊆ & U ×_{K} V. \end{aligned}

• Tensor unit. (K, id_{K}, {K}, P(K)), where P denotes powerset.

3.3 The biextensional full monoidal embedding F : chu(Set, K) → G(Rel^{K})

Let A = (A, r, X) be a biextensional Chu space over K. Given a point a ∈ A and a copoint x ∈ X, define^{2}

\begin{aligned}row(a) & = & \{a\} × X & ⊆ & A × X \\ col(x) & = & A × \{x\} & ⊆ & A × X \end{aligned}

and define

rows(r) = { row(a) : a ∈ A }
cols(r) = { col(x) : x ∈ X }

Note that rows(r) ≅ A and cols(r) ≅ X (since A is biextensional). On objects, define

F (A, r, X) = (A × X, r, rows(r), cols(r)).

Given a morphism (f, g) : (A, r, X) → (B, s, Y) in chu(Set,K), define the binary relation

F (f, g) ⊆ (A × X) × (B × Y)

2 Different to a common definition of “row” of (A, r, X) as any function ρ : X → K such that ρ = r(a, −) for some a ∈ A.

by

⟨a, g(y)⟩ F (f, g) ⟨f(a), y ⟩

for every point a ∈ A and copoint y ∈ Y. See Figure 2 (page 3) for an example. To be a G(Rel^{K}) morphism, the binary relation F (f, g) must (1) respect colour, (2) map values forwards to values by direct image, and (3) map covalues back to covalues by inverse image. Property (1) follows immediately from the adjointness of f and g. Properties (2) and (3) will follow from the more general (non-biextensional) case in section 5. In the meantime, observe that (1)–(3) hold for the example in Figure 2 (page 3). That F is full, faithful, and monoidal will also follow from the more general case in section 5.

3.4 No obvious extension

Note that the definition of F above does not depend on biextensionality. The very same definition, verbatim, yields a functor from Chu(Set, K) to G(Rel^{K}). Although F is faithful on chu(Set, K), this extension to Chu(Set, K) is not: faithfulness fails on morphisms between Chu spaces with no points and more than one copoint (and vice versa). For example, let A ∈ Chu(Set, K) be a Chu space with two points and no copoints (hence non-biextensional). There are 2^{2} = 4 morphisms from A to A, one for each function f from the twoelement set to itself; however, there is only one morphism from F (A) to F (A) (the empty binary relation, since F (A) has no tokens).

Thus the natural extension of F to a functor Chu(Set, K) → G(Rel^{K}) is a “near miss” for a nice relationship between the Chu construction and the Hyland-Tan double glueing construction. The intensional double glueing construction IG defined below was conceived as a “fix” for the failure of this extension to be faithful: in section 5, following the strategy outlined in Figure 3 (page 5), we extend F : chu(Set, K) ↪ G(Rel, K) to a full monoidal embedding F^{+} : Chu(Set, K) → IG(Rel^{K}).

4 The intensional double glueing construction IG

We define the intensional double glueing construction IG by substituting multisets for sets in Hyland and Tan’s G [21]. The construction has similar properties to its progenitor G: when ℂ is star-autonomous, IG(ℂ) is star-autonomous, and when ℂ is compact closed [10] (therefore with isomorphic tensor and par), IG(ℂ) has distinct tensor and par. Thus IG, like G, is a potentially useful tool in the search for fully complete models of linear logic.

Define a multiset A = (A, |−|_{A}) over a set V to be a set A equipped with a valuation |−|_{A} : A → V. We shall typically omit subscripts from valuations. A morphism (f, v) : A → B between multisets A over V and B over W is a function f : A → B together with a function v : V → W which tracks f in the sense that |f(a)| = v(|a|):

[figure: A; B; V; W; f; v; |−|; |−|]

Let ℂ be a star-autonomous category with tensor ⊗ : ℂ × ℂ → ℂ, tensor unit I, duality (−)^{⊥} : ℂ^{op} → ℂ, and internal hom −∘ : ℂ^{op} × ℂ → ℂ. Let ⊥ = I^{⊥}, the dual of the tensor unit. Recall the following shorthand from section 2.2:

(−)_{∗} ≡ ℂ(I, −) : ℂ → Set  (the values functor)
(−)^{∗} ≡ ℂ(−, ⊥) : ℂ → Set^{op} (the covalues functor)

The star-autonomous structure of IG(ℂ) is as follows. The reader may wish to make a line-by-line comparison with the structure of G(ℂ) (page 7).

• Objects. Triples (U, A, X) where · U is an object of ℂ, · A is a multiset of U-values (i.e., a multiset over U_{∗} = ℂ(I, U)), · X is a multiset of U-covalues (i.e., a multiset over U^{∗} = ℂ(U, ⊥)). We refer to the elements of A and X as points and copoints, respectively. Each point a ∈ A determines a U-value |a| = |a|_{A} : I → U, and each copoint x ∈ X determines a U-covalue |x| = |x|_{X} : U → ⊥.

• Morphisms. A morphism (U, A, X) → (V, B, Y) is a triple (R, f, g): · a morphism R : U → V in ℂ, · a function f : A → B on points, and · a function g : Y → X on copoints, such that R_{∗} tracks f and R^{∗} tracks g, i.e., such that the squares

[figure: A; B; U_{∗}; V_{∗}; f; R_{∗}; |−|; |−|; X; Y; U^{∗}; V^{∗}; g; R^{∗}; |−|; |−|]

commute, i.e., such that (f, R_{∗}) and (g, R^{∗}) are multiset morphisms.

• Duality. (U, A, X)^{⊥} = (U^{⊥}, X, A), modulo (U^{⊥})_{∗} ≅ U^{∗} and (U^{⊥})^{∗} ≅ U_{∗}.

• Internal hom. Given A = (U, A, X) and B = (V, B, Y),

A −∘ B = (U −∘ V, hom(A, B), A × Y )

with the following valuations on hom(A, B) and A × Y:

\begin{aligned}|(R, f, g)| & = & R ∈ ℂ(U, V) ≅ (U −∘ V)_{∗} \\ |⟨a, y⟩| & = & |a| ⊗ |y| ∈ ℂ(I ⊗ V, U ⊗ ⊥) ≅ (U −∘ V)^{∗}. \end{aligned}

• Tensor. Given A = (U, A, X) and B = (V, B, Y),

A ⊗ B = (U ⊗ V, A × B, hom(A, B^{⊥}))

with the following valuations on A × B and hom(A, B^{⊥}):

\begin{aligned}|⟨a, b⟩| & = & |a| ⊗ |b| ∈ ℂ(I ⊗ I, U ⊗ V) ≅ (U ⊗ V)_{∗} \\ |(R, f, g)| & = & R ∈ ℂ(U, V^{⊥}) ≅ (U ⊗ V)^{∗}. \end{aligned}

• Tensor unit. ( I, {id_{I}}, I^{∗} = ℂ(I, ⊥) ), with identity valuations.

Proposition 4.1 IG(ℂ) is star-autonomous.

This proposition follows from abstract considerations in section 4.2.

4.1 Biextensional collapse

This section is motivated by, and parallels, the biextensional collapse of Chu spaces (section 2.1.1). Deine an object of IG(ℂ) as biextensional if its valuations are injections. Up to equivalence (namely, taking objects whose valuations are inclusions, rather than injections), the biextensional full subcategory of IG(ℂ) is Hyland and Tan’s category G(ℂ). Define the collapse of a multiset M = (M, |−|_{M}) over V to be the image |M| = { |m|_{M} : m ∈ M } ⊆ V of its valuation. Given an object A = (U, A, X) ∈ IG(ℂ), define its biextensional collapse Ã ∈ G(ℂ) by collapsing its point and copoint multisets to sets:

Ã = (U, |A|, |X|).

Biextensional collapse is functorial from IG(ℂ) to G(ℂ): given A = (U, A, X) and B = (V, B, Y) in IG(ℂ) and a morphism m = (R, f, g) : A → B, its biextensional collapse m̃ is simply R : U → V. Since (f, R_{∗}) and (g, R^{∗}) are multiset morphisms, R maps values forwards and covalues backwards, as required of a morphism of G(ℂ).

Analogous to the way in which the star-autonomous structure on biextensional chu(Set, K) is inherited from Chu(Set, K) by biextensional collapse (section 2.1.1), tensor ˜⊗ and internal hom ˜−∘ in G(ℂ) can be viewed as being inherited from IG(ℂ) by biextensional collapse: A ˜⊗ B = { \atop A⊗B} and

A ˜−∘ B = { \atop A−∘B}.

4.2 Abstract perspective

In this section we consider IG from a more abstract point of view, and prove that IG(ℂ) is star-autonomous (Proposition 4.1).

The result of glueing along a functor F : ℂ → 𝔹 is the comma category (id ↓ F) (see MacLane [13]). Double glueing along functors 𝔹 ←^{F} ℂ →^{G} 𝔻 appears under the notation /F, G/ as Pavlović’s category of interpolants [14], and in Hyland and Schalk’s comprehensive study of glueing and orthogonality for models of linear logic [9]. Objects of /F, G/ are triples (b, C, d) where C is an object of ℂ, b is a morphism in 𝔹 into F (C), and d is a morphism in 𝔻 out of G(C). A morphism (b, C, d) → (b′, C′, d′) is a triple of morphisms (f, g, h) ∈ 𝔹 × ℂ × 𝔻 where g : C → C′ and the following squares commute:

[figure: F (C); F (C′); b; b′; f; F (g); G(C); G(C′); d; d′; h; G(g)]

Let ℂ be a star-autonomous category with tensor unit I, and let ⊥ = I^{⊥}. The category IG(ℂ) is the category of interpolants /ℂ(I, −), ℂ(−, ⊥)/, i.e., the result of double glueing along the functors

Set ⟵^{ℂ(I,−)} ℂ ⟶^{ℂ(−,⊥)} Set^{op}

Proof that IG(ℂ) is star-autonomous. We appeal to a more general result of Hyland and Schalk: in Proposition 4.14 on page 27 of [9], set E = Set and L = ℂ(I, −). This uses the fact that Set is symmetric monoidal closed with pullbacks.

5 Extending the full monoidal embedding

We saw in section 3.4 that the natural extension of F : chu(Set, K) ↪ G(Rel^{K}) to the whole of Chu(Set, K) fails to be faithful. In this section we “fix” the lack of faithfulness on Chu(Set, K), extending F to a full monoidal embedding F^{+} : Chu(Set, K) → IG(Rel^{K}). Figure 3 (page 5) outlines our strategy.

5.1 The category IG(Rel^{K}) of intensionally double glued relations over K

To reduce bracket clutter, we flatten the triplets ((U, r), A, X) coming out of the application of IG, and present IG(Rel^{K}) as follows. The reader may wish to make a line-by-line comparison with the structure of G(Rel^{K}) (page 9).

• Objects. Tuples (U, r, A, X) where · U is a set of tokens, · r : U → K is a colouring function, · A is a multiset of subsets of U (i.e., a multiset over P(U)), · X is a multiset of subsets of U (i.e., a multiset over P(U)). Each a ∈ A is a point, each x ∈ X is a copoint, |a| = |a|_{A} ⊆ U is a value, and |x| = |x|_{X} ⊆ U is a covalue.

• Morphisms. A morphism (R, f, g) : (U, r, A, X) → (V, s, B, Y) is: · a binary relation R ⊆ U × V between tokens which respects colour, i.e., uRv only if r(u) = s(v), · a function f : A → B on points, and · a function g : Y → X on copoints, such that direct image R_{∗} tracks f and inverse image R^{∗} tracks g:

|f(a)| = R_{∗}(|a|) ≡ { v ∈ V : uRv for some u ∈ |a| }
|g(y)| = R^{∗}(|y|) ≡ { u ∈ U : uRv for some v ∈ |y| }.

• Duality. (U, r, A, X)^{⊥} = (U, r, X, A), interchanging points and copoints.

• Internal hom and tensor. Given A = (U, r, A, X) and B = (V, s, B, Y),

A −∘ B = ( U ×_{K} V, r ×_{K} s, hom(A, B), A × Y )
A ⊗ B = ( U ×_{K} V, r ×_{K} s, A × B, hom(A, B^{⊥}) )
|(R, f, g)| = R  (valuation in hom(A, B), hom(A, B^{⊥}))
|⟨a, q⟩| = |a| ×_{K} |q|  (valuation in A × Y, A × B)

• Tensor unit. (K, id_{K}, {K}, P(K)), with identity valuations.

The biextensional collapse Ã of A = (U, r, A, X) ∈ IG(Rel^{K}) is (U, r, |A|, |X|) ∈ G(Rel^{K}) and the biextensional collapse of a morphism (R, f, g) is R.

5.2 The full monoidal embedding F^{+} : Chu(Set, K) → IG(Rel^{K})

Figure 3 (page 5) sketches the idea. Define F^{+} on objects by

F^{+}(A, r, X) = ( Ã × X̃, r̃, A, X )

where ( ) is biextensional collapse on the components of a Chu space (section 2.1.1), and valuations on A and X (respectively) are:

\begin{aligned}|a| & = \{ ã \} × X̃ & ⊆ & Ã × X̃ \\ |x| & = Ã × \{ x̃ \} & ⊆ & Ã × X̃ \end{aligned}

Thus the value of a point is its ‘biextensional row’, and the covalue of a copoint is its ‘biextensional column’. See Figure 3.

Given a morphism m = (f, g) : (A, r, X) → (B, s, Y) in Chu(Set, K), define F^{+}(m) = (F (m̃), f, g). Thus the binary relation

F (m̃) ⊆ (Ã × X̃) × (B̃ × Ỹ)

relates ⟨ã, g̃(y)⟩ and ⟨f̃(a), ỹ⟩ for all a ∈ A and y ∈ Y.

The well-definedness, fullness and faithfulness of F^{+} follow from the lemma below. Given non-empty sets A and X define a row (resp. column) of A×X to be any subset of A × X of the form {a} × X (resp. A × {x}).

Lemma 5.1 Pairs of functions ( A →^{f} B, X ←^{g} Y ) between non-empty sets are in bijection with binary relations R ⊆ (A × X) × (B × Y) whose direct image R_{∗} maps rows of A × X to rows of B × Y and inverse image R^{∗} maps columns of B × Y back to columns of A × X.

Proof. The correspondence is: [f(a) = b and g(y) = x] iff [R_{∗}({a} × X) = {b} × Y and R^{∗}(B × {y}) = A × {x}] iff ⟨a, b⟩R⟨x, y⟩. □

F^{+} is monoidal (but not strict or strong monoidal) with

\begin{matrix}F^{+}(A) ⊗ F^{+}(B) & ⟶ & F^{+}(A ⊗ B) \\ (K, id_{K}, \{K\}, P(K)) & ⟶ & F^{+}(1, π_{K}, K) \end{matrix}

defined as follows. Let A = (A, r, X) and B = (B, s, Y), so

F^{+}(A) ⊗ F^{+}(B) = ( (Ã × X̃) ×_{K} (B̃ × Ỹ), r̃×_{K} s̃, A × B, hom(A, B^{⊥}) )
F^{+}(A ⊗ B) = ( { \atop (A×B)} × { \atop hom(A, B^{⊥})}, ẽv, A × B, hom(A, B^{⊥}) )

(with the obvious valuations). Define the natural morphism from the former to the latter to be (R, id, id), where R is given by

⟨ ⟨ã, g̃(b)⟩ , ⟨b̃, f̃(a) ⟩ ⟩ R ⟨ { \atop ⟨a, b⟩} , { \atop ⟨f, g⟩} ⟩

for all a ∈ A, b ∈ B, and morphisms (f, g) : A → B^{⊥} in Chu(Set, K). The map

(K, id_{K}, {K}, P(K)) ⟶ F^{+}(1, π_{K}, K) ≅ (K, id_{K}, {K}, K)

is (id, id, η_{K}) where η_{K} : K → P(K) takes k ∈ K to {k} ∈ P(K).

Biextensional case. Since tensor ˜⊗ and internal hom ˜−∘ in the biextensional categories chu(Set, K) and G(Rel^{K}) are inherited from the corresponding larger categories by biextensional collapse (A ˜⊗ B = { \atop A⊗B} and A ˜−∘ B = { \atop A−∘B}), the biextensional full embedding F : chu(Set, 2) ↪ G(Rel^{K}) is also monoidal: take the biextensional collapse of F^{+}(A) ⊗ F^{+}(B) → F^{+}(A ⊗ B).

6 Biextensional collapse

Biextensional collapse ( ) : IG → G extends the familiar notion on Chu spaces, in the sense that the square in Figure 1 (page 3) commutes from topleft to bottom-right, i.e., F ∘ ( ) = ( ) ∘ F^{+} : Chu(Set, K) → G(Rel^{K}). (This fact is immediate from the definitions of F and F^{+}.)

In the terminology of Hyland and Schalk [9], IG is the result of omitting the specialisation to monic structure maps implicit in G [21]. Thus, since G(ℂ) is (equivalent to) the biextensional full subcategory of IG(ℂ), we obtain a new interpretation of the monic specialisation as a form of biextensionality. This leads to the distinction between intensional and biextensional models described in the introduction (page 4).

Acknowledgement

Many thanks to Martin Hyland, Duško Pavlović and Vaughan Pratt for their interest and feedback during the development of this work.

References

[1] Abramsky, S., and R. Jagadeesan, Games and full completeness for multiplicative linear logic, J. Symbolic Logic 59.2(1994) 543–574.

[2] Barr, M., “Star-autonomous Categories,” Lecture Notes in Mathematics 752, Springer-Verlag, 1979.

[3] Barr, M., Star-autonomous categories and linear logic, Math. Structures in Computer Science 1.2(1991) 159–178.

[4] Barr, M., The separated extensional Chu category, Theory and Applications of Categories 4.6(1998) 137–147.

[5] Barr, M., Star-autonomous categories: once more round the track, Theory and Applications of Categories 6.1(1999) 5–24.

[6] Devarajan, H., D. Hughes, G. Plotkin, and V. Pratt, “Full completeness of the multiplicative linear logic of chu spaces,” Proc. IEEE Logic in Computer Science 14, 1999.

[7] Ehrhard, T., Hypercoherences: a strongly stable model of linear logic, Math. Structures in Computer Science 3.4(1993) 365–385.

[8] Girard, J.-Y., Linear Logic, Theoretical Computer Science 50.1(1987) 1–102.

[9] Hyland, J.M.E., and A. Schalk, Glueing and orthogonality for models of linear logic, Theoretical Computer Science 294(2003) 183–231.

[10] Kelly, G.M., and M.L. Laplaza, Coherence for compact closed categories, Journal of Pure and Applied Algebra 19(1980) 193–213.

[11] Loader, R., “Linear logic, totality and full completeness,” Proc. IEEE Logic in Computer Science 9, 1994.

[12] Lafont, Y., and T. Streicher, “Games semantics for linear logic,” Proc. IEEE Logic in Computer Science 6, 43–49, 1991.

[13] Mac Lane, S., “Categories for the Working Mathematician,” Springer-Verlag, 1971.

[14] Pavlović, D., “Categorical Interpolation: Descent and the Beck-Chevalley Condition,” Proc. Category Theory, Como 1990. Lecture Notes in Mathematics, 1488, 1–77, Springer-Verlag, 1991.

[15] Pratt, V.R., “The Stone Gamut: A Coordinatization of Mathematics”, Proc. IEEE Logic in Computer Science 10, 444–454, San Diego, 1995.

[16] Pratt, V.R. “Chu spaces and their interpretation as concurrent objects,” Lecture Notes in Computer Science 1000, 392–405, 1995.

[17] Pratt, V.R., “Chu Spaces,” Notes for the School on Category Theory and Applications, University of Coimbra, Portugal, July 13-17, 1999. Downloadable

as http://boole.stanford.edu/pub/coimbra.ps.gz.

[18] Pratt, V.R., Chu Spaces from the Representational Viewpoint, Annals of Pure and Applied Logic 96(1999) 319–313.

[19] Pratt, V.R., Chu spaces as a semantic bridge between linear logic and mathematics, Theoretical Computer Science 294.3(2003) 439–471.

[20] Seely, R.A.G., Linear logic, star-autonomous categories and cofree coalgebras, Contemporary Mathematics 92(1989) 371–382.

[21] Tan, A., “Full completeness for models of linear logic,” Ph.D. thesis, King’s College, University of Cambridge, October 1997.