Visualising information flows of finite functions

One way that I can demonstrate that information flows is through visualisation. That information flows form a lattice can be seen intuitively by realising that if the information in $P_1$ determines the information in $Q_1$ and the information in $P_2$ determines the information in $Q_2$ then the combined information $P_1P_2$ determines the information in $Q_1Q_2$. That they form a lattice also means they can be displayed as Hasse diagrams, so you can see what they look like.

All visualisations will be done with Clojure and Graphviz. In order to create set theoretic functions, we need the data of an input set, an output set, and a Clojure function or map. This ensures that we can handle functions that are not surjective. But in the easier case where they are surjective, we can just get a function using the to-function method. The elements of the information flow lattices are partition pairs, which are vectors of disjoint families of sets.

Small functions:

(SetFunction. #{0} #{0} {0 0})

(SetFunction. #{0 1} #{0} {0 0, 1 0})

(SetFunction. #{0 1} #{0 1} {0 0, 1 1})

(SetFunction. #{0 1} #{0 1} {0 0, 1 0})

(SetFunction. #{0 1 2} #{0} {0 0, 1 0, 2 0})

(SetFunction. #{0 1} #{0 1 2} {0 0, 1 1})

(SetFunction. #{0 1 2} #{0 2} {0 0, 1 0, 2 2})

(SetFunction. #{0 1 2} #{0 1 2} {0 0, 1 1, 2 2})

Intermediate sized functions:

(to-function {0 0, 1 0, 2 0, 3 0})

(to-function {0 0, 1 0, 2 2, 3 2})

(to-function {0 0, 1 0, 2 0, 3 3})

(to-function {0 0, 1 1, 2 2, 3 2})

(to-function {0 0, 1 1, 2 2, 3 3})

(to-function {0 0, 1 0, 2 0, 3 0, 4 0})

(to-function {0 0, 1 0, 2 2, 3 2, 4 2})

(to-function {0 0, 1 0, 2 0, 3 0, 4 4})

(to-function {0 0, 1 0, 2 0, 3 3, 4 4})

(to-function {0 0, 1 1, 2 1, 3 3, 4 3})

(to-function {0 0, 1 1, 2 2, 3 3, 4 3})

(to-function {0 0, 1 1, 2 2, 3 3, 4 4})

Large or infinite functions:
By generality, functions larger then these have information flow lattices even if we cannot visualize them. The algebraic theory of information ensures that we can exist. Using mathematical techniques we can describe their properties even in the infinite case.

References:
[1] Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.

[2] Lausmaa, T. (2005). Extropy-based quantitative evaluation of finite functions. Proceedings of the Estonian Academy of Sciences. Physics. Mathematics, 54(2), 67. https://doi.org/10.3176/phys.math.2005.2.01

Paying homage to the work of Hartmanis and Stearns

A commenter alerted me to the fundamental work of Hartmanis and Stearns: Algebraic Structure Theory of Sequential Machines (1966). This came closest to capturing the fundamental ideas that I was getting at in my study of information flows. To put my work in context, I want to do something to pay homage to this prior work.

When I first thought about what to title my paper, I couldn't think of anything particularly good that would stick. So I took the good old fashioned shotgun approach and made a big title with a bit of everything: "The Topos Theory of Computing: Introduction to the Mathematics of Dataflow." Yet its clear that calling this a theory of computing doesn't get to the point, because the whole point of this thesis is an examination of structures.

By changing the title of my work to Toposic Structure Theory of Computations (2023) I get an intrinsically better title while also more effectively paying homage to the excellent prior work of Hartmanis and Stearns. This hopefully reduces any controversy around my work and puts it into an appropriate historical context. We now have two different types of structure theory in computer science:

• The algebraic structure theory
• The toposic structure theory

The Algebraic Structure Theory of Sequential Machines (1966) is one of those marvelous gems of science and technology that due to historical accident seems to have fallen to the way side. It is something that despite its age still has something to teach us, just like the Lisp machines. There is always something to be learned from studying the best technologies of the past.

But I am not here to revive old technologies. In my work, I developed novel new foundations for the mathematics of information flows using topos theory. It is demonstrated that the information flows of Hartmanis and Stearns are nothing more then quotients in $Sets^{\to}$. By establishing functors from a wide variety of different categories to $Sets^{\to}$ information flows are applied to a wider variety of contexts then ever before.

It is shown that morphisms in $Sets^{\to}$ preserve and reflect partition pairs. The result is a monotone Galois connection between information flow lattices of functions associated to every morphism in $Sets^{\to}$. This opens up a wide variety of different computations that would not be possible without the topos theoretic framework. All of this makes this subject an exciting and fertile ground for further exploration.

References:
Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.

A new way of programming with information flows

Informal discussion:
The physical world is highly parallel, with many things happening side by side. A realistic model of computation is dataflow, which can be conceptualized as a kind of motion. Much like how particles move around in physical systems, bits of information move around in computers. This motivates our development of a theory of information flows.

But what exactly are these bits of information? Consider even and odd; then both are bit-valued functions that produce ones and zeros. But even and odd produce the same bits of information. They represent the information in two different ways. If $n$ is even then we know it is not odd, and if its not even then we know it is odd. The same applies the other way around.

To represent the same bit of information as evenness or oddness, we can use a partition. Both the even and odd functions are representations of the abstract notion of parity, which can be defined as a partition with two elements. An abstract bit of information is then a partition of a set into two different classes. It does not matter rather you get the parity from even, odd, 2 * mod(n,2), or any other representation. An abstract bit of information may be realized in many different forms.

A piece of information, in general, is just a collection of bits of information. We can call these partitions, but the important point is that they refer to a place within the information of a larger structure. A piece of information is larger than another one if it has more bits than it. Partitions abstract functions so that every function can now be treated as a representation of a piece of information.

We now know how to think abstractly about places within an information system, but we still need to understand how information moves around. Let $f: A \to B$ be a function; then we can describe a flow relation on $f$ by a pair (P,Q) which proclaims that the function moves the information in the place $P$ to the place $Q$. We now have a fundamental notion of information flows.

As an example, return back to our notion of parity. If we take a function like $x+1$ then we see that $x+1$ maps the parity information in its input to the parity information in its output. So (parity, parity) is a datflow relation on $x+1$. If we take an even number and add one to it, then we get an odd number and if we take an odd number and add one to it we get an even number. So $x+1$ flips parity bits around.

On the other hand, $x^2$ leaves the parity bit as it is: the square of an even number is even, and the square of an odd number is odd. Two other examples are $2x$, which always produces a number of even parity, and $2x+1$, which always produces one that is odd. Other functions like $\Omega$ might not map parities back to parities at all. These functions might take different numbers of the same parity and map them to numbers of different parities.

It would be nice if we could take a place in an input structure, like the parity of a number, and then find out exactly what place in the output it flows into. By doing this, we will depart from the traditional view of set theory which is that functions values in sets and instead make them take values in partitions.

In fact, we can do this if we take the notion of a partition image $f(P)$. This produces the set of information we know from $f$ when it is given the information in $P$. So the partition image directly codifies how a function moves information from places to places, and it lets you compute how a function moves bits from one location back to another. The dual concept is the partition inverse image $f^{-1}(Q)$, which is the collection of all bits of information that map into $Q$.

Partition images are the basis of our new way of programming with dataflow relations. A whole new parallel universe of functions that take operate on partitions is created alongside those that take values in sets. This is a new paradigm of computing in information systems which we call functional dataflow.

We provide a system of support for smart functions: special data types of functions that know things about their own data flow characteristics. These are combined with special partition data types, so that smart functions can have computable partition images. They can take a place in a system and return the place it maps to. This makes information flows accessible to the user.

As a basic example, consider a transposition permutation on pairs. Then this function swaps the order in an ordered pair $f(x,y) = (y,x)$. We might make this into a smart function that records its own flow information so that it records that the information in the first index is moved to the second index, and the information in the second is moved to the first. This flow information might be made computable using partition images, so that if you $f$ what it maps the first index to it will return the second index.

If bits of information are the simplest units of storage, then this suggests that bit-flow relations $(P,Q)$ between bits of information $P$ and $Q$ are the simplest forms of dataflow. We already saw an example of a bit flow relation with the (parity, parity) relations in arithmetic functions. These bit-flow relations are the atomic building blocks for all other dataflow relations.

Information flows can now be seen to form an ordering by scale. There can be large events with millions of bits moving around to ones with only one or two. By the same token, an event in a physical system might have anything from the motion of an astronomical body on the higher end to the motions of subatomic particles on the smallest scales. In both cases, we have an intuitive notion of scale. We now have a way of capturing information flows from the smallest scales to the largest.

For technical experts:
For aficionados of functors, categories, adjunctions, toposes, lattices, lenses, theorems and proofs: the topos structure theory of computing

Toposic structure theory of computations FAQ

As I present this new thesis on the role of topos theory in computing to the world, I have anticipated a number of possible questions and answers ahead of time. I will do my best to answer any questions you may have.

What prior work is closest to yours?
With the help of a commentor on hacker news, I have determined that the Algebraic Structure Theory of Sequential Machines (1966) comes closest my work. Most impressively, they came close to developing the idea of a dataflow relation without using Sierpinski topos theory. Instead of an ordinary algebraic structure theory, I provide an updated theory based instead upon topoi.

What other prior works do you build upon the most?
The first and foremost is probably Robert Goldblatt's Topoi: The Categorial Analysis of Logic. It is with this text that I first discovered the Sierpinski topos which opened up the way for my own further studies in the subject. A second reference text is Sketches of an Elephant – A Topos Theory Compendium. Aside from these a variety of lattice theory textbooks and papers provided extra tidbits of information.

What is the practical basis of applied topos theory?
I believe the answer to this is the principle of locality. The physical universe of which we are all a part is organized around this principle which states that an object is influenced directly only by its immediate surroundings. This creates an organizing principle of relevance to all fields of engineering. In classical physics this motivates the modeling of physical systems based upon their local behaviour. In computing, this motivates our theories of local computation and dataflow.

What use is a topos theory of computing?
The topos theory of computing can be used to model information loss and information flow. The first is relevant because the second law of thermodynamics states that the entropy of a logical system cannot decrease - which implies that information loss leads to heat dissipitation. The second is relevant because the principal of locality necessitates that computer systems should be modeled in terms of information flows and local effects.

What is this topos theory of computing?
I would like to explain it by analogy to physics. In physics we study the movement of particles from place to place. In this theory of computing, we instead study the movement of packets of bits from place to place. In order to describe these information flows I have presented a new formalism based upon Sierpinski topos theory.

Toposic structure theory of computations

Abstract:
The theory of data-flow analysis of computer programs has been extensively studied. The increasing need for dataflow analysis in the automatic parallelization of computer programs motivates the development of mathematical foundations for this field. We present a new approach to program dataflow analysis that incorporates partition lattices and the Sierpinski topos.

Link:
The topos theory of computing: introduction to the mathematics of dataflow

The enriched presheaves framework

The Locus computer algebra system is going to be centered around the idea of presheaf theory. It is our claim that presheaves make for the best models of computation, and presheaves can be a unifying fabric for logical and functional programming. Logic programming is modeled using the topos $Sets$ and functional programming is modeled using $Sets^{\to}$.

With this initial effort, we saw that a number of presheaf topos $Sets^{C}$ had interesting properties. MSets and their topoi $Sets^M$ could be used to model the fundamental properties of monoids and their Green's relations through their subobject lattices. Categories can be described by the topos of compositional quivers or by simplicial sets using the nerve construction.

However, there is only so far you can go with this construction without considering other types of functors, like structure presheaves. This leads to the enriched presheaves framework in particular. I have in mind as part of this framework that modules, left modules, right modules, and bimodules should be considered to be types of Ab-enriched presheaves. This will allow more of our fundamental constructions to be integrated into the presheaf theoretic and sheaf theoretic world view.

First examples of enriched categories:
Let $Cat$ be the category of categories and functors. Then $Ord$, $CMon$, and $Ab$ are closed subcategories of $Cat$, and it follows naturally from this that they are self-enriched. So these form the most fundamental examples of enriched categories:

• Locally ordered categories: categories enriched in $Ord$
• Ringoids: categories enriched in $Ab$
• Semiringoids: categories enriched in $CMon$

Each of the categories $Ord$,$CMon$, and $Ab$ are also concrete: so abelian presheaves, preordered presheaves, and presheaves of commutative monoids are all examples of structure presheaves. Now using their enriched category structure we can form modules as special types of structure presheaves.

The general framework
The general framework is for defining an enriched category over a monoidal category, also called a $V$-enriched category. In particular, every cartesian monoidal category is a monoidal category $V$ which can be used to form enriched categories. Then a $V$-enriched structure presheaf is a functor from a $V$ enriched category to a $V$ enriched concrete category. If $V$ is a concrete closed category, then $V$ enriched functors to $V$ are used to form modules.

Modules as structure presheaves:
Rings in general are partially commutative, with totally commutative rings being a special case (*). In order to deal with this most general context, we need to deal with differences between left and right composition. This leads to notions of left and right modules, which fortunately can be handled nicely be the structure copresheaves framework.

• Left modules: $Ab$-enriched copresheaves of abelian groups
• Right modules: $Ab$-enriched presheaves of abelian groups
• Bimodules: $Ab$-enriched profunctors of abelian groups
• Modules: the same as left modules except that the source category $R$ is a commutative ring

How fortuitous that we already have presheaf-theoretic counterparts for each of the different types of modules. Left modules are just copresheaves, right modules are presheaves, and bimodules are profunctors.

Sets	Ab
Left modules	Copresheaves
Right modules	Presheaves
Bimodules	profunctors

This means in effect that whilst left modules, right modules, and bimodules are to be treated the same as in any other computer algebra system, in a presheaf based computer algebra system, we can in addition implement for them the methods get-object, get-morphism, get-set, and get-function so that they can optionally be treated as structure copresheaves as well. This will be a strictly advantageous result.

Semimodules as structure presheaves:
The same approach as for modules works for semimodules, if we replace all the enriched categorical machinery of $Ab$ with $CMon$. In fact, this will work for any similarly closed category.

• Left semimodules: $CMon$-enriched copresheaves of commutative monoids
• Right semimodules: $CMon$-enriched presheaves of commutative monoids
• Bisemimodules: $CMon$-enriched profunctors of commutative monoids
• Semimodules: the same as left semimodules except the source category is a commutative semiring

The generalisation of modules to semimodules is necessary because a great number of constructions in modern mathematics are based upon semirings. For instance, the ideals of a commutative ring form an idempotent semiring.

Presheaves of preorders:
In our presheaf theoretic foundations, we have already made presheaf versions of most categorical constructions. In particular, we can generalize the lattice of preorders on a set to the lattice of preorders on a presheaf.

Definition. let $F$ be a presheaf then $Ord(F)$ is its lattice of preorders. Its objects are presheaves of preorders with underlying presheaf $F$ with the join and meet defined componentwise.

Another construction is that for any given preorder $P$ we can form its condensation which is a partial order. This generalizes to preorderd presheaves, so that for any presheaf we can form its condensed presheaf of partial orders by composition with the condensation functor.

Definition. let $F$ be a presheaf of preorders then $C(F)$ is its underlying presheaf of partial orders.

We previously considered the idea of a locally ordered category. A special case is a locally ordered monoid. We can form modules over locally ordered monoids, in a similar manner to rings using this structured presheaf framework, and the same technique is even applicable to locally ordered categories.

Definition. let $C$ be a locally ordered category. Then a left module over $C$ is simply a $Ord$ copresheaf of partial orders well a right module is an $Ord$ enriched presheaf of partial orders.

In particular, let $M$ be a locally ordered monoid. Then as a monoid it has left and right MSets define over it. In the case that $M$ is locally ordered, these further form $Ord$ enriched presheaves of partial orders, which are order modules. These are analogous to the left and right induced modules over rings. Most modules over ordered monoids can be formed this way, or by their restrictions by change of index functors defined by monotone monoid homomorphisms.

References:
[1] Enriched categories

[2] Enriched functor

[3] Categorical algebra

[4] Presheaves

[5] Copresheaves

[6] Profunctors

Locus 1.5

Locus 1.5 has been pushed to github. I would say the impetus for the recent series of changes was so that I could implement various categorical adjunctions that generalize images/inverse images. Towards that end, I have a multimethod for images and preimages which dispatches its arguments based upon the type of both of its values. So we have that images can be formed from various function-like objects applied to various mathematical objects.

• Set images are applicable to partial functions and multi-valued functions as well as ordinary functions. The image of a set under a multivalued function or set relation can be formed by the image multimethod.
• In most textbooks on category theory there is a mention of the topos $Quiv$ of binary quivers, which consists of two parallel functions from the edge set to the vertex set. I have generalized this to ternary quivers, and indeed all the way to nary quivers. The nary quivers implementation is new in this version.
• Given any nary quiver there are set images and inverse images: the set image of a set of edges in a nary quiver is the union of the sets of vertices in each edge, or in other words the union of all set images of the set under each component function. Inverses images are uniquely defined so that they form an adjunction.
• I implemented two new concepts for completions sake: partial quivers and hyperquivers. A hyperquiver is a functor from the parallel arrows category $T_{2,n}$ but to $Rel$ instead of $Sets$. Partial quivers are defined the same way but using te subcategory of partial functions. Set images under hyperquivers are formed by the union of all set images produced by all hte multivalued functions of the hyperquiver.
• Set images are defined for MSets and so instances of the MSet class implement the image multimethod now. The image of a set under an MSet is the set of all outputs of all actionts on the MSet applied to all elements of the set. Inverse images are defined dually so they form an adjunction.
• Images and inverse images are defined for set partitions. So that given a function you can apply it to a SetPartition rather then a set and you will get the appropriate set partition as an output using the image multimethod. This implements the adjunction between partition images and inverse images.
• Likewise, given any preorder you can apply it to a function instead of a set to get the preorder image or inverse image.
• The adjointness definition of continuous maps is defined by topological images/inverse images. So given a member of the TopologicalSpace class, it is interpreted properly by the image method to get an output topological space which is the maximal topological space which makes that map continuous. Topological inverse images are also defined so this forms an adjunction. So images/inverse images work in the most contexts possible now.
• A new class of copresheaves: Galois copresheaves is implemented now. These are just Galois connections without any reference to any underlying ordering.
• A new order theory framework integrating adjunctions is provided. New classes for residuated maps, coresiduated maps, and Galois connections are defined. The framework for supporting adjunctions has been greatly improved, motivated by this work on images and inverse images.
• Finally, new support for ordered algebraic structures is provided by new classes. These will be the first step towards algebraic structures like quantales which can always be formed from any algebraic structure using images and inverse images.

The implementation of the images/preimages framework is a good and necessary first step. A great many categories are defined by image/inverse image adjunctions, but the next steps will see us further improve the support for structure presheaves. Structure presheaves are our main focus.