Visualisation of lattice polynomials

The basic units of algebraic logic are lattice polynomials, while the basic units of algebraic geometry are ring polynomials. Unlike their ring counterparts, lattice polynomials can form a tree structure. This leads to the possibility of using tree visualisation methods on lattice polynomials. In order to make this visualisation more effective, I developed a simple color scheme:

• Meet: red
• Join: green

Green is typically considered a positive color while red is a negative color. So it makes sense that the join should be green while the meet is red. Every non-leaf node in a lattice polynomial is either a meet or join term, and so can be coloured coded accordingly. Due to associativity, a well formed lattice polynomial should always alternate between green and red at each level. In order to implement this, I used dorothy to create graphviz files from lattice polynomials.

(require '[dorothy.core :as dot])
(require '[dorothy.jvm :refer (render save! show!)])

(defn get-coordinates
  "Get the coordinates of the leaf nodes of an S-expression."
  [coll]

  (if (not (seq? coll))
    '(())
    (apply
      concat
      (map
        (fn [i]
          (map
            (fn [c]
              (cons i c))
            (get-coordinates (nth coll i))))
        (range (count coll))))))

(defn get-coordinate-value
  "Get the value of an S-expression at the given coordinate."
  [coll coordinate]

  (if (empty? coordinate)
    coll
    (get-coordinate-value
      (nth coll (first coordinate))
      (rest coordinate))))

(defn create-digraph
  "Create a digraph from the arithmetical form 
   of a lattice polynomial."
  [coll]

  (letfn [(create-vertex [coll coordinate]
            (let [v (get-coordinate-value coll coordinate)
                  cstr (.toString coordinate)]
              (cond
                (= v '*) [cstr {:label     ""
                                :fillcolor "crimson"
                                :style     "filled"}]
                (= v '+) [cstr {:label     ""
                                :fillcolor "green"
                                :style     "filled"}]
                :else [cstr {:label (.toString v)}])))
          (create-vertices [coll coordinates]
            (concat
              (map
                (partial create-vertex coll)
                coordinates)))
          (find-next-leaf [coll coordinate]
            (if (seq? (get-coordinate-value coll coordinate))
              (find-next-leaf coll (concat coordinate (list 0)))
              coordinate))
          (successor-edges [coordinate]
            (let [fixed-coordinate (if (&= (count coordinate) 1)
                                     '()
                                     (butlast coordinate))
                  parent-sequence (get-coordinate-value 
                                    coll 
                                    fixed-coordinate)]
              (map
                (fn [i]
                  [(.toString 
                     (seq (concat fixed-coordinate (list 0))))
                   (.toString 
                     (seq (find-next-leaf 
                            coll 
                           (concat fixed-coordinate (list i)))))])
                (range 1 (count parent-sequence)))))
          (create-edges [coll coordinates]
            (apply
              concat
              (for [i coordinates
                    :when (= (last i) 0)]
                (successor-edges i))))]
    (let [coordinates (get-coordinates coll)]
      (vec
        (concat
          (create-vertices coll coordinates)
          (create-edges coll coordinates))))))

In order to demonstrate this approach to lattice polynomial visualisation, I have prepared a couple of examples. In order to encode a lattice polynomial as an S-expression, I use the arithmetical syntax of defining the meet operation as multiplication and the join operation as addition. This follows from the fact that the meet operation is the product operation in a thin category, while the join operation is the coproduct.

(def expoly1
  '(+ (* a b)
      (* c (+ d e))))

This simple approach can be used to visualize arbitrarily large lattice polynomials, with an arbitrary number of variables and operations nested to any depth. Therefore, our second example is a bit larger then the first.

(def expoly2
  '(* (+ (* a b)
         (* c d)
         e)
      (+ (* f g) h)
      (+ i j k)
      l))

This demonstrates a way of visualising lattice polynomials in algebraic logic. Of course, we can often perform visualisations of a different sort for the ring polynomials in algebraic geometry: the visualisation of algebraic varieties formed by ring polynomials. In either case, visualisation techniques will always be important in logic and geometry.

The identity functor

The most basic and fundamental topoi are $Sets$ and $Sets^{\to}$. These describe the fundamentals of sets and functions respectively. As these are the most important objects of topos theoretic mathematics, it would be nice if the two could be related to one another in a way.

Definition. let $Sets$ be the topos of sets and $Sets^{\to}$ the topos of functions. Then let $id : Sets \to Sets^{\to}$ be the function of categories that maps each set $X$ to its identity function $id_X: X \to X$ with $f(x) = x$ and that maps each morphism of sets $f : A \to B$ to the morphism of functions $id_f : id_A \to id_B$ defined by the ordered pair of functions $(f,f) : A^2 \to B^2$.

Theorem. $id : Sets \to Sets^{\to}$ is a monofunctor, which makes $Sets$ into a full subcategory of $Sets^{\to}$.

Proof. (1) let $f: A \to B$ and $g : B \to C$ be morphisms of $Sets$ then their composition is $f \circ g : A \to C$. The corresponding morphisms of $Sets^{\to}$ are $(id_f,id_f)$ and $(id_g,id_g)$ defined as ordered pairs of functions. Then their composition is defined componentwise to be $(id_f \circ id_g, id_f \circ id_g)$ which can be be refactored as $(id_{f \circ g}, id_{f \circ g})$. So that $id_{f} \circ id_{g} = id_{f \circ g}$ which makes $id$ a functor.

(2) let $id_A : A \to A$ and $id_B : B \to B$ be the identities of $A$ and $B$ respectively. Suppose that $(f,g)$ is a morphism of functions from $id_A$ to $id_B$ then it must satisfy the commutative diagram which says that $id_B \circ f = g \circ id_A$ which is logically equivalent to $f = g$. By the fact that $f=g$, it follows that any morphism of identity functions is of the form $(f,f) : id_A \to id_B$ which can be defined by identity functor $id_f$ which makes $Sets$ a full subcategory of $Sets^{\to}$. $\square$

This embeds the topos $Sets$ into the topos $Sets^{\to}$ as the full subcategory $Id$. It would be interesting, if we could further determine the properties of this embedding and the extent to which it preserves the topos theoretic properties of $Sets$.

Theorem. $Id$ is closed under taking products and coproducts, but not under subobjects and quotients.

Proof. (1) suppose that $id_A: A \to A$ is an identity function, then it has as a subobject all non-surjections that are taken by reducing the domain and not the codomain. Likewise, given $id_A : A \to A$ we can define a congruence of functions by $(=_A, true)$ which has a constant quotient, rather then an identity quotient. So $Id$ is not closed under subobjects or quotients.

(2) on the other hand suppose that $id_A : A \to A$ and $id_B : B \to B$ are two identity functions. Then $id_A \times id_B : A \times B \to A \times B$ takes $f(a,b)$ to $(id_A(a),id_B(b))$ which is equal to $(a,b)$ so it is still an identity function. Similarily, the coproduct $id_A + id_B : A + B \to A + B$ takes any $a \in A$ to $a$ and $b \in B$ to $b$ so that it is still an identity function. $\square$

This completes the process of relating $Sets$ to $Sets^{\to}$. In the other direction, there are a couple of ways to relate $Sets^{\to}$ back to $Sets$. Firstly, given any category $C$ with subcategory $S$ then we can define a morphism of topoi $Sets^{C} \to Sets^{S}$ that reduces each set-valued functor to its $S$ components. Using this, we can define input set and output set functors on $Sets^{\to}$.

A limitation of this approach is that it doesn't make $Sets^{\to}$ into a concrete category, so in order to do that we simply need to use the coproduct construction. This takes any function $f : A \to B$ to its coproduct set $A + B$ constructed from its input and output sets. Together with the input and output set functors, these functors relate $Sets{\to}$ and $Sets$.

The future of declarative programming

The declarative programming space is divided between the functional and logic programming paradigms. Historically, these two paradigms were represented by Lisp on the functional side and prolog on the other. Lisp had greater traction in America and prolog was more popular in Europe, and so a divide naturally formed between them.

Each paradigm has its own merits. Logic programming is used in artificial intelligence systems to create logical models of a number of domains and even entire ontologies and knowledge bases. Functional programming is typically a better model of computation then logic programming, which gives it a greater degree of practicality.

What these two paradgims have in common is their origin in the basic structures of mathematics: sets and functions. Instead of describing computation imperitively through a combination of side effects and control flow, functional and logic programs use the basic structures of mathematics as building blocks of programs. Their commonalities mean that it is possible to unify these two paradigms under a single umbrella.

It had never occurred to me that topos theory could provide the framework for the common unification of functional and logic programming paradigms. It is such a simple idea the basic structures of logic are defined by the topos $Sets$ and of functional programming are defined by the topos $Sets^{\to}$ that this has to be the right way of doing things. In the other direction, any implementation of the fundamentals of topos theory is going to have to be in a functional logic language.

Logic programming
The basic object of a logic programming is a predicate, which is a computational generalization of a set. In the place of functions, logic programming languages focus on relations which can be queried both backwards and forwards. This means that logical languages don't have the forwards directionality of functional languages.

This is a significant disadvantage when performing computations, which also have an element of time directionality. Logic programming languages like Prolog nonetheless have a niche use as a part of some artificial intelligence application that model domains using ontologies and semantic networks.

Functional programming
A natural solution to the limitations of logic programming languages like Prolog is to use a functional programming language. There are two issues that need to be resolved for any functional programming language: (1) how can we provide logically models of information in the language (2) how can we reason logically about functions themselves in the language.

The first issue can be resolved to some extent by tacking on a logic programming library to the language, which is fairly common. This is not an elegant solution but its just good enough in most cases. The second issue can only be resolved by topos theory which is the indispensible tool for reasoning logically about the functional structures of abstract algebra.

Sets and functions are not so different after all
In order to produce a functional logic synthesis, we should first ask is this worthwhile at all? Some things are genuinely different and so cannot be susceptible to unification. Yet topos theory tells us that sets, which are the building blocks of logic programs, and functions, which are the basic building blocks of functional programs, are not so different after all.

The commonality between sets and functions is that they are both members of topoi. Therefore, they have all the same common features of any topos object: subobject and quotient lattices, products, coproducts, initial and terminal objects, morphisms, epimorphisms, monomorphisms, isomorphisms, etc. A number of common methods can therefore be defined for both sets and functions.

The functional logic synthesis
Now that we have provided sufficient motivation for the functional logic synthesis, all that remains is to implement it. In this synthesis of functions and logic, each object will be associated with its own fundamental topoi:

Logic programming	$Sets$
Functional programming	$Sets^{\to}$

Interfaces will be defined that contain methods for dealing with any topos object, like products, coproducts, etc and those should be implemented by both sets and functions, and then these same interfaces should be extendible by users who want to work with other topoi.

Topoi as models of declarative programming:
As a result of this approach, we see that topos theory provides a fundamental framework for declarative programming, just as it provides the foundation of mathematics. To each declarative subparadigm we associate a topos that it is focused on. This applies to the most basic paradigms like logic and functional programming, and it opens up a

The ultimate conclusion of this unification is that there is no reason to have separate and incompatible declarative programming languages like Lisp and Prolog, and so it is possible to unify them under a single umbrella with common semantics for logic, functions, and other declarative programming components.

There may still need to be separate languages for imperiative programming like Java and C#, that can deal with lower level issues of the virtual machine. But there is no reason that these imperiative programming languages nonetheless cannot run on the same virtual machine as the declarative language of the future.

Topoi as models of computation:
We have briefly discussed how topoi provide new foundations for declarative programming. Another interesting direction, is how topoi can be used to provide mathematical models of abstract computation. The foundation of this approach is the mathematical logic of dataflow analysis of functions provided by topos theory.

A central issue in computer science is the locality of computation, which is a consequence of the spatial distribution of computers. Corresponding to this idea of the locality of computation, topos theory provides a way to define the local effects of functions. Topos theory, which emerged from efforts in algebraic geometry, is now also the key to mathematically defining the geometry of computation.

References:
Sketches of an elephant volume one
Peter Johnstone

Sketches of an elephant volume two
Peter Johnstone

Topoi: the categorical analysis of logic
Robert Goldblatt