Topoi as foundations of computation:
The topos theoretic foundations of computation used in the Locus project are based upon congruence lattices in copresheaf topoi. In particular, we have the following distinction:
- Memory locations: congruences in $Sets$
- Data dependencies: congruences in $Sets^{\to}$
The next level of abstraction:
The congruence lattices of sets and functions are in general not distributive. On the other hand, subobject lattices are always distributive in any topos. We would like to handle the congruence lattices of sets and functions in a manner similar to more familiar distributive lattices and boolean algebras. So a second abstraction level makes this possible.
We establish the second layer of abstraction by reference to the allegory $Rel$ of sets and set relations. Memory locations are modeled by sets of places and data dependencies are modeled by relations between places. This produces a second layer in the model of memory and two classes are implemented to handle this second layer.
- Product decompositions: objects in $Rel$
- Flow models: morphisms in $Rel$
- Image: let $R : A \to B$ be a relation and $X \subseteq A$ then the image is defined by $R(X) = \bigcup_{x \in X} R(X)$.
- Inverse image: let $R : A \to B$ be a relation and $Y \subseteq B$ then the inverse image $R^{-1}(Y) = \{x \in X : R(X) \subseteq Y\}$.
A distinction occurs between the inverse image and the converse relation image, that does not occur on the level of functions. We define the converse relation image in the following manner: \[ R^C(Y) = \bigcup{y \in Y} : \{ x \in X : y \in r(X) \} \] This does not have anything to do with the construction of the distributive subalgebra lattice, but it is simply a consequence of the converse involution in the dagger category $Rel$. By clearly distinguishing between the types of relation images and constructing the distributive lattices $Sub(R)$ we are ready to start working with the second layer of abstraction.
Interfacing between the two abstraction levels:
We essentially want to have an abstraction level over memory locations and data dependencies that uses the allegory $Rel$ and the mechanisms we previously described. In order to do that, we need to relate sets to set congruences and relations to function congruences.
Definition. let $I$ be generating system for a boolean algebra of $Part(A)$ whose partitions all form direct products of one another then $I$ forms a product decomposition of $A$. This produces a correspondence from sets to partitions $f_I: \wp(I) \to Con(A)$.
Definition. let $f : A \to B$ be a function and suppose that $I$ and $J$ are product decompositions of $A$ and $B$. Then a flow model $F$ is a morphism $m : J \to I$ in the allegory $Rel$ such that for each $j \in J$ we have that $(f_I(m(j)),f_J(\{j\}))$ is a function congruence of $f$.
This provides a contravariant correspondence, as flow models from $A$ to $B$ are defined by set relations from locations in $B$ to locations in $A$. We now have two different monotone maps of lattices: \[ f_I: \wp(I) \to Con(A) \] \[ F: Sub(m) \to Con(f) \] In addition, we can use this abstraction to model partition images and inverse images in terms of their relational counterparts. Given a partition of $B$ indexed by $S$ in $J$ then its partition inverse image is the relational image of $m$ and dually for a partition of $A$ indexed by $S$ in $I$ its partition image is the relational inverse image of $m$ over that index set.
As a result, although we are able to model the theory of data dependencies using the allegory $Rel$ rather then a base topos, the topos theoretic foundations are always there and available to us by conversion. The abstractions provided over $Sets$ and $Sets^{\to}$ by $Rel$ can only ever produce subsets of the congruences of sets and functions.
There can be many different abstraction layers over our foundation in the topos of functions $Sets^{\to}$. For example, in semigroup theory we have an abstraction we have an abstraction layer whereby a congruence $C$ is defined by a single set rather then pairs of sets $(C^2,C)$. There can be many different abstraction layers, but as long as we keep ourselves firmly footed within the topos theoretic foundations in $Sets$ and $Sets^{\to}$ then we will always have a common interface for reasoning about different abstraction layers.
Compositionality:
Suppose that we have a function with a flow model $(f,m)$ in $Sets \times Rel^{op}$. Then the flow models describing distributive lattices of respective functions, compose with one another. The contravariance of the composition of flow models is a result of the obvious forgetful functor to the opposite category: \[ F: Sets \times Rel^{op} \to Rel^{op} \] The flow models of product decompositions provide a composable logic for reasoning about the relations between memory locations, which is modeled on an underlying topos theory. By maintaining flow models under composition we can maintain as much information about function congruences as possible.
References:
[1] The allegory Rel of sets and relations
[2] The topos Set of sets and functions
