Dialectica spaces were first developed by Valeria de Paiva in her thesis. They happen to be a model of linear logic, in particularly they are a model of full intuitionistic linear logic. This fact came as quite a surprise to Valeria and her Ph.D. advisor Martin Hyland. The project they were working on was to give a categorical interpretation of Gödel’s dialectica interpretation. Naturally, they thought it would give rise to a cartesian closed category, but it turned out to be a model of linear logic!
There is a close cousin to dialectica spaces called Chu spaces. These spaces were developed by Michael Barr and his masters student Po-Hsiang Chu as a model of linear logic. They have also been widely studied by Vaughan Pratt and his group at Stanford. One of the most interesting computational applications of Chu spaces is in concurrency theory.
This post can be thought of as some of my notes on understanding the relationship between dialectica spaces and Chu spaces. The results in this post are mostly due to Valeria de Paiva and Vaughan Pratt; citations will be given below. The main objective of this post is to highlight the differences between the two types of spaces, and to show that Chu spaces can be embedded into dialectica spaces using Valeria’s work. Then we show that all \(n\)-ary relational structures can be embedded into dialectica spaces using Pratt’s work. Finally, we conclude with an application.
Consider the following definitions.
A dialectica space is a function \(r : A \times X \to \Sigma\) such that \(\Sigma\) is a lineale. We call \(\Sigma\) the alphabet and \(X\) the set of states of the dialectica space. Given a dialectica space we can define a new function that returns the columns of the space given a state by \(r_c = \mathsf{cur}(\beta;r) : X \to (A \to \Sigma)\) where beta is the canonical isomorphism \(\beta : X \times A \to A \times X\) and \(\mathsf{cur}\) is the canonical currying isomorphism. When \(r_c\) is injective we call \(r\) extensional.
A Chu space is a function \(r : A \times X \to \Sigma\). We call \(\Sigma\) the alphabet and \(X\) the set of states of the Chu space. Chu spaces can be extensional which is defined exactly how it is defined for dialectica spaces.
The previous definitions imply that we can think of dialectica and Chu spaces as matrices where the set of values in their cells are from \(\Sigma\). Extensional spaces are often easier to work with because the states of the space are unique.
There is only one difference between the two previous definitions, which is the requirement that \(\Sigma\) is a lineale in the definition of dialectica spaces. What is a lineale, and why do we need it? Consider the first question.
A
monoidal poset is a poset \((\Sigma,\leq)\) with a given given compatible monoidal structure \((L,\circ,e)\). That is, \(L\) is a set with a reflexive, symmetric, and transitive relation \(\leq\,\subseteq L \times L\) together with a monoidal multiplication \(\circ : L \times L \to L\) and distinguished object \(e \in L\) satisfying the following:
- Associativity: \(a \circ (b \circ c) = (a \circ b) \circ c\)
- Symmetry: \(a \circ b = b \circ a\)
- Identity: \(a \circ e = e \circ a = a\)
- Compatibility: if \(a \leq b\) then \(a \circ c \leq b \circ c\), for all \(c \in L\)
A lineale is a monoidal poset \((L, \leq, \circ, e)\) such that for any \(a,b \in L\), there exists a largest \(x \in L\) where \(a \circ x \leq b\). This element is denoted by \(a \Rightarrow b\) and is called the relative pseudocomplement of \(a\) wrt \(b\). This definition implies that following hold:
- Application: \(a \circ (a \Rightarrow b) \leq b\)
- Currying: \(a \circ c \leq b\) iff \(c \leq a \Rightarrow b\)
- If \(a \leq b\), then for any \(c \in L\), \(c \Rightarrow a \leq c \Rightarrow b\) and \(b \Rightarrow c \leq a \Rightarrow c\)
Thus, lineales can be seen as a trivialization of a symmetric monoidal closed category.
Lineales are needed to define transformations between dialectica spaces. We define these next along with transformations between Chu spaces. These are what really set the two types of spaces apart.
Suppose \(r : A \times X \to \Sigma\) and \(s : B \times Y \to \Sigma\) are two dialectica spaces over \(\Sigma\). Then a dialectica transformation is a pair of functions \((f,F) : r \to s\) where \(f : A \to B\), \(F : Y \to X\), and the following constraint holds:
\(\forall a \in A.\forall y \in Y.r(a,F(y)) \leq_\Sigma s(f(a),y)\). We call the previous constraint the semi-adjointness condition, and this condition is the reason why we need the alphabet to be a lineale.
Suppose \(r : A \times X \to \Sigma\) and \(s : B \times Y \to \Sigma\) are two Chu spaces over \(\Sigma\). Then a Chu transformation is a pair of functions \((f,F) : r \to s\) where \(f : A \to B\), \(F : Y \to X\), and the following constraint holds:
\(\forall a \in A.\forall y \in Y.r(a,F(y)) = s(f(a),y)\). We call the previous constraint the adjointness condition.
Taking dialectica spaces over \(\Sigma\) as objects and dialectica transformations as morphisms we obtain a category called \(\mathsf{Dial}(\Sigma)\), and doing the same for Chu spaces we obtain a category called \(\mathsf{Chu}(\Sigma)\). We have arrived at the following result.
Suppose \(\Sigma\) is a lineale. Then there is an embedding \(E : \mathsf{Chu}(\Sigma) \to \mathsf{Dial}(\Sigma)\).
Take \(E\) to be the identity functor. ◼
The results up to now are not new. They were first investigated by Valeria de Paiva in her TAC paper. She makes a lot more interesting connections between the two types of spaces. The interested reader should see her paper for more fun! We now use her result to show that every \(n\)-ary relation can be represented by a dialectica space.
\(n\)-ary Relations in Dialectica Spaces
Vaughan Pratt showed that any \(n\)-ary relation can be represented by a Chu space over \(\mathsf{2}^n = \{0,1\}^n\) for some \(n \in \mathbb{N}\). This results in Chu spaces being able to represent a large number mathematical structures. We would like this same result for dialectical spaces, and we can obtain it by using the embedding discussed above. However, we must show that \(\mathsf{2}^n\) is a lineale in order to obtain our result. We do this now.
First, we show that we can construct a category of lineales. We have morphisms between lineales.
Suppose \((L_1,\leq_1, \circ_1, e_1,\Rightarrow_1)\) and \((L_2,\leq_2, \circ_2, e_2,\Rightarrow_2)\) are two lineales. Then a
lineale map between \(L_1\) and \(L_2\) is a function \(f : L_1 \to L_2\) satisfying the following properties:
- If \(a \leq_1 b\), then \(f(a) \leq_2 f(b)\)
- \(f(a \circ_1 b) = f(a) \circ_2 f(b)\)
- \(f(e_1) = e_2\)
- \(f(a \Rightarrow_1 b) = f(a) \Rightarrow_2 f(b)\)
It is easy to see that we can now form a category of lineales where composition and identities are set theoretic. We denote this category by \(\mathsf{Lin}\). Next we show that this category has products.
\(\mathsf{Lin}\) has all finite products.
Suppose \((L_1,\leq_1, \circ_1, e_1,\Rightarrow_1)\) and \((L_2,\leq_2, \circ_2, e_2,\Rightarrow_2)\) are two lineales. Then we can construct the monoidal poset \((L_1 \times L_2,\leq_\times, \circ_1 \times \circ_2, (e_1,e_2))\) where \(\leq_\times\) is the lexicographic combination of \(\leq_1\) and \(\leq_2\). Now we must prove that for any \((a,b),(c,d) \in L_1 \times L_2\), there exists a largest \((x_1,x_2) \in L_1 \times L_2\) where \((a,c)\,(\circ_1 \times \circ_2)\,(x_1,x_2) \leq (b,d)\). Choose \(a \Rightarrow_1 b\) for \(x_1\) and \(c \Rightarrow_2 d\) for \(x_2\). Certainly, each of these are largest within their respective set, and hence, their pairing will be largest in the cartesian product. Therefore, \((L_1 \times L_2,\leq_\times, \circ_1 \times \circ_2, (e_1,e_2),\Rightarrow_1 \times \Rightarrow_2)\) is a lineale.
Clearly, there are two lineale maps \(\pi_1 : (L_1 \times L_2,\leq_\times, \circ_1 \times \circ_2, (e_1,e_2),\Rightarrow_1 \times \Rightarrow_2) \to (L_1,\leq_1, \circ_1, e_1,\Rightarrow_1)\) and \(\pi_2 : (L_1 \times L_2,\leq_\times, \circ_1 \times \circ_2, (e_1,e_2),\Rightarrow_1 \times \Rightarrow_2) \to (L_2,\leq_2, \circ_2, e_2,\Rightarrow_2)\) defined by the set theoretic projections. Finally, we must show that the following diagram commutes:
where \((L_3,\leq_3, \circ_3, e_3,\Rightarrow_3)\) is a lineale. Suppose \(f : L_3 \to L_1\) and \(g : L_3 \to L_2\) are two lineale maps. Then choose the set theoretic function \(\langle f,g \rangle : L_3 \to L_1 \times L_2\) for \(h\). Clearly, in sets the previous diagram commutes, but we must verify that \(\langle f,g \rangle\) is a lineale map. We do this verification as follows:
- Suppose \(a,b \in L_3\) and that \(a \leq_3 b\). Then \(\langle f,g \rangle(a) = (f(a),g(a))\) and \(\langle f,g \rangle(b) = (f(b),g(b))\). By assumption \(f\) and \(g\) are lineale maps, and thus, \(f(a) \leq_1 f(b)\) and \(g(a) \leq_2 g(b)\) which implies that \((f(a),g(a)) \leq_\times (f(b),g(b))\).
- Suppose \(a,b \in L_3\). Then
\(
\begin{array}{llllll}
\langle f,g \rangle(a \circ_3 b)
& = & (f(a \circ_3 b),g(a \circ_3 b))\\
& = & (f(a) \circ_1 f(b),g(a) \circ_2 g(b))\\
& = & (f(a),g(a))\,(\circ_1 \times \circ_2)\,(f(b),g(b))\\
& = & \langle f,g \rangle(a)\,(\circ_1 \times \circ_2)\,\langle f,g \rangle(b).\\
\end{array}
\)
- First, \(\langle f,g \rangle(e_3) = (f(e_3),g(e_3))\), and because \(f\) and \(g\) are lineale maps \((f(e_3),g(e_3)) = (e_1,e_2)\).
- Suppose \(a,b \in L_3\). Then
\(
\begin{array}{llllll}
\langle f,g \rangle(a \Rightarrow_3 b)
& = & (f(a \Rightarrow_3 b),g(a \Rightarrow_3 b))\\
& = & (f(a) \Rightarrow_1 f(b),g(a) \Rightarrow_2 g(b))\\
& = & (f(a),g(a))\,(\Rightarrow_1 \times \Rightarrow_2)\,(f(b),g(b))\\
& = & \langle f,g \rangle(a)\,(\Rightarrow_1 \times \Rightarrow_2)\,\langle f,g \rangle(b).\\
\end{array}
\)
At this point all that is left to do is show that there is a terminal object. Let \(L_T\) be any one element set where \(\star \in L_T\) is its distinguished object. Then we can construct the lineale \((L_T, \leq_T, \circ_T, \star, \Rightarrow_T)\) as follows:
- Set \(\leq_T = \{(\star,\star)\}\).
- Set \(\star \circ_T \star = \star\).
- Set \(\star \Rightarrow_T \star = \star\).
It is trivial to see that \(L_T\) is a lineale given the previous definitions. Suppose \((L, \leq, \circ, \star, \Rightarrow)\) is a lineale. Then there is a lineale map \(\diamond : L_1 \to L_T\) is simply the terminal map from sets. The verification that it is lineale is straightforward. ◼
If \(L\) is a lineale, then \(L^n = \underbrace{L \times \cdots \times L}_n\) is a lineale for any \(n \in \mathbb{N}\).
To conclude that \(\mathsf{2}^n\) is a lineale it is enough to show that \((\mathsf{2} = \{0,1\},\leq_B\,=\{(0,0),(0,1),(1,1)\},\land,1,\Longrightarrow) \), where \(\land\) and \(\Longrightarrow\) are binary conjunction and implication respectively, is a lineale. It is easy to see via truth tables that conjunction is symmetric, associative, and \(1\) is its identity. Thus, \(\mathsf{2}\) is a monoidal poset. Now consider the following truth table:
\(
\begin{array}{ccccc}
a & x & a \land x & b\\
0 & 1 & 0 & 0\\
0 & 1 & 0 & 1\\
1 & 0 & 0 & 0\\
1 & 1 & 1 & 1\\
\end{array}
\)
This truth table proves that for any \(a,b \in \mathsf{2}\), there exists a greatest \(x \in \mathsf{2}\) such that \(a \land x \leq_B b\). Furthermore, notice that the columns for \(a\), \(b\), and \(x\) defines binary implication where \(x = a \Longrightarrow b\). Therefore, \((\mathsf{2},\leq_B,\land,1,\Longrightarrow) \) is a lineale. By the fact that \(\mathsf{Lin}\) is cartesian we may conclude that \(\mathsf{2}^n\) is a lineale.
At this point we simply replay Vaughan Pratt’s result. First, we define \(n\)-ary relations.
An \(n\)-ary relational structure \((X,\rho)\) consists of a set \(X\) and an \(n\)-ary relation \(\rho \subseteq X^n\) on \(X\). A homomorphism \(f : (X,\rho) \to (Y,\sigma)\) between \(n\)-ary relational structures is a function \(f : X \to Y\) such that \(f(\rho) = \{(f(a_1),\cdots,f(a_n)) \mid \overrightarrow{a_i} = (a_1,\cdots,a_n) \in \rho \} \subseteq \sigma\). Taking the relational structures as objects and their homomorphisms as morphisms defines a category called \(\mathsf{Str}_n\).
Next we define an embedding \(E’ : \mathsf{Str}_n \to \mathsf{Dial}(\mathsf{2}^n)\).
We define the object part of \(E’ : \mathsf{Str}_n \to \mathsf{Dial}(\mathsf{2}^n)\) as taking the \(n\)-ary relational structure \((A,\rho)\) to the dialectica space \(r : A \times X \to \mathsf{2}^n\) defined as follows. Take the set of states, \(X\), to be the subset of \(n\)-tuples \(r \in \mathcal{P}(A)^n\) for which \(\Pi_i r_i \subseteq \overline{\rho} = A^n – \rho\). Finally, define \(r : A \times X \to \mathsf{2}^n\) by \(v(a,x) = 1\) if \(a \in r_i\), and \(0\) otherwise.
The object part as defined above is injective.
For all \(\overrightarrow{a_i} \in A^n\), \(\overrightarrow{a_i} \in \rho\) iff for any \(r \in X\), there exists an \(i < n\), such that, \(r(a_i,x)_i = 0\).
It also turns out that \(r : A \times X \to \mathsf{2}^n\) is extensional. See lemma 12 of Pratt’s paper.
We still need to define the morphism part of \(E’\).
We define the morphism part of \(E’ : \mathsf{Str}_n \to \mathsf{Dial}(\mathsf{2}^n)\). Suppose \(f : (A, \rho) \to (B, \sigma)\) be a homomorphism between \(n\)-ary relations, where \(E'(A,\rho) = r : A \times X \to \mathsf{2}^n\) and \(E'(B,\sigma) = s : B \times Y \to \mathsf{2}^n\). Define \(f^{-1} : (\mathsf{2}^n)^B \to (\mathsf{2}^n)^A\) by \(f^{-1}(g : B \to \mathsf{2}^n) = f;g : A \to \mathsf{2}^n\). Finally, define \(E'(f) = (f,f’)\). The correctness of this definition can be found in Pratt’s paper in definition 13.
By theorem 14 of Pratt’s paper \(E’\) is concrete, full, and faithful. Thus, it is an embedding.
Application: Multisets in Dialectica Spaces
This line of inquiry of mine was started because I wanted a way to represent multisets by dialectica spaces over a finite alphabet. A multiset, \(m : A \to \mathbb{N}\), can be represent by an equivalence relation, \(\cong_m \subseteq A \times A\), such that, for any \(a \in A\), \(|[a]_{\cong_m}| = m(a)\). That is, the cardinality of the equivalence class of a particular element in the multiset is the elements multiplicity. Taking this representation of multisets and the previous result we now have a means of interpreting multisets into dialectica spaces over a finite alphabet.