Clojure java interop

The Java virtual machine is a general building material for programs, not necessarily tied to any language or programming paradigm. All that matters is that you can produce JVM bytecode. Since it is all the same in the end, it is worth asking what advantages the Java language has for generating JVM bytecode.

• Support for variable names and distinguished argument lists.
• Type deduction in opcode generation. In particular, you don't have to distinguish between iadd, ladd, fadd, and dadd when adding two numbers. Likewise, for the other arithmetic operations, loading and storing values in arrays, returning values, casting, etc. By the same token, you don't have to fully specify method signatures.
• The import statement saves you from always having to fully specify java class names. There is no corresponding import opcode for the Java virtual machine, so this is purely a Java language feature.
• The Java language doesn't force you to have to distinguish between different opcodes when loading constants. The Java virtual machine supports the different opcodes to make more compact bytecode. Any high level language (including the ASM bytecode library) should handle this automatically.
• Java provides control flow constructs in the place of goto and conditional jumps. Part of this is the uniform condition system, which prevents you from having to determine which conditional jump opcode to use.
• A uniform call syntax so you don't have to distinguish between invokestatic, invokevirtual, invokeinterface, and invokespecial.
• Built in support for l-values and generalized place forms, so you can use a general assignment form on local variables, array indices, and static and instance fields. You can even set values in multidimensional arrays and the Java compiler will produce the correct combination of opcodes for you for that.
• Last but not least, the Java language automatically handles arguments on the stack for you. This can be useful for example when dealing with mathematical expressions.

The Java language does a lot when you put it like that, but this by no means that Java virtual machine bytecode is hard to use. The Java virtual machine is still a high level architecture which is easier to use than any C-machine. Hopefully this explains why you might use the Java language to generate JVM bytecode, but it is all the same if you want to use something else or even write you or own compiler as I have.

Setting up a mixed project:
So in order to set up a mixed Java and Clojure project I suggest using Intellij IDEA. Intellij is the only Java focused IDE that also has good support for Clojure. Then you just need to create separate Java and Clojure folders and configure Leiningen to specify your Clojure folder in :source-paths and your Java folder in :java-source-paths.

Creating a Java class:
In order to create a first example of Java and Clojure interop, I have chosen the special case of defining a prime number sieve. Obviously, you could easily do this in Clojure, but perhaps some mathematical functionality should be written in Java so that they are more performant.

import java.util.BitSet;

public class NumberUtilities {

    public static int[] sieve(int n) {

        BitSet primes = new BitSet(n+1);
        primes.flip(2, n+1);

        for(int p = 2; p*p <= n; p++) {
            if(primes.get(p)) {
                for(int i = p*p; i <= n; i += p) {
                    primes.set(i, false);
                }
            }
        }

        return primes.stream().toArray();
    }

}

I mentioned that the Java language is just a tool for generating Java virtual machine bytecodes. Its kind of like an M-expression syntax for the JVM, and Lisp Flavoured Java is an S-expression syntax. Clojure is a different beast entirely from either of them. For the purposes of this demonstration, lets examine the output bytecode as it appears with Jasmin.

.class public NumberUtilities

.method public static sieve(I)[I
    .limit stack 4
    .limit locals 4

; initialize the bit set
    new java/util/BitSet
    dup
    iload_0
    iconst_1
    iadd
    invokespecial java/util/BitSet.(I)V

; flip the possible primes to true
    astore_1
    aload_1
    iconst_2
    iload_0
    iconst_1
    iadd
    invokevirtual java/util/BitSet.flip(II)V

; initial the first prime to two
    iconst_2
    istore_2

; start a loop in order to do the sieve on the main bit set
loop:
    iload_2
    iload_2
    imul
    iload_0
    if_icmpgt loop_breakpoint

; ensure that this number is a prime before starting the inner loop
    aload_1
    iload_2
    invokevirtual java/util/Bitset.get(I)Z
    ifeq inner_loop_breakpoint

; initialize the current multiple to the first non flipped index
    iload_2
    iload_2
    imul
    istore_3

; flip all multiples of the current prime to false
inner_loop:
    iload_3
    iload_0
    if_icmpgt inner_loop_breakpoint

; set the current index to false
    aload_0
    iload_3
    iconst_0
    invokevirtual java/util/BitSet.set(IZ)V

    iload_3
    iload_2
    iadd
    istore_3
    goto inner_loop

inner_loop_breakpoint:

    iinc 2,1
    goto loop
loop_breakpoint:

    ; convert the bitset into an int array containing all true indices and return
    aload_1
    invokevirtual java/util/BitSet.stream()Ljava/util/stream/IntStream;
    invokeinterface java/util/stream/IntStream.toArray()[I
    areturn
.end method

The advantages of the Java language can clearly be seen by comparing the Java language code to the Java virtual machine bytecode. Whenever someone says that Java is verbose, I just remember how much typing it saves from having to write JVM bytecode in hand, which I have a done a lot. Too much.

A notable aspect of this is how the compiler structures the output of for loops. There is quite a lot to unpack when using a for loop, and its logic appears all over the place in the compiled output. That is why some parts of the for loop appear before the loop starts, at the start of the loop, and at the end. Once you unpack all of that it is fairly easy to see how Java code corresponds to bytecode. In that sense, Java is one of the easier languages to understand in terms of its compiler output.

Calling Java functions from Clojure
All the countless hours spent reading the documentation of the Java virtual machine, the Java language, and the thousands of classes in the Java standard library are finally rewarded by using Clojure, which has seamless Java interop.

(prn (seq (NumberUtilities/sieve 1000)))

The execution of the sieve function written in Java produces the first prime numbers up to a thousand, which confirms our memory of the smallest primes.

(2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59 61 67 
71 73 79 83 89 97 101 103 107 109 113 127 131 137 139 
149 151 157 163 167 173 179 181 191 193 197 199 211 223 
227 229 233 239 241 251 257 263 269 271 277 281 283 293 
307 311 313 317 331 337 347 349 353 359 367 373 379 383 
389 397 401 409 419 421 431 433 439 443 449 457 461 463 
467 479 487 491 499 503 509 521 523 541 547 557 563 569 
571 577 587 593 599 601 607 613 617 619 631 641 643 647 
653 659 661 673 677 683 691 701 709 719 727 733 739 743 
751 757 761 769 773 787 797 809 811 821 823 827 829 839 
853 857 859 863 877 881 883 887 907 911 919 929 937 941 
947 953 967 971 977 983 991 997)

Clojure is able to call the Java sieve function because they both speak the same basic language: Java virtual machine bytecode. We saw the JVM output of the Java class. The corresponding Clojure class produces the same sort of opcodes, starting with a call with invokestatic to call the sieve function. The only difference is that Clojure might have to use reflection if not enough type information is provided to it.

In this case that isn't necessary because NumberUtilities doesn't use method overloading, but in general the most important performance benefit you can add to your Clojure code is to use type hints so you don't have to use reflection to determine method signatures at runtime. Finally, after calling sieve we use seq in order to print it, because sequences produce better output when converted to Strings. A more Java like solution would be to use java.util.Arrays/toString.

The Java language and Clojure perfectly complement each other, because Clojure isn't just another copy of Java. Java is static, imperative, heteroiconic, etc while Clojure is dynamic, functional, and homoiconic. The fact that two languages that are so different from one another can come together is the ultimate testament to the power of the Java virtual machine.

Decade in review and changes

I can now reflect on the past decade in order to determine what has been done right or wrong, and whats next. In particular, I will explain my programming philosophy and how it has developed over the years. Finally, I will explain the new blog description.

Fully embracing Clojure
I've had several years to really pick up on Common Lisp and Scheme, and I never have. Two important points in Clojure's favor are its richer and more modern syntax and the fact that it is hosted on a virtual machine. Most importantly, it is what I have invested most of my time in. By focusing on Clojure alone, I will have more time to embrace more of the Clojure and ClojureScript ecosystem.

Switching to Intellij:
I am not going to be touching any Lisp dialects other then Clojure, and that includes Emacs Lisp. I am proud to announce that I have switched to Intellij IDEA for everything including Clojure development. I think it was wrong of me to use Emacs so much, and Intellij IDEA is a godsend. It will free me up to mix Java, Clojure, and other JVM languages together in the same project as I see fit.

Virtual machines are more important then languages:
There is an old quote from Alan Kay which is a favourite of mine, which is that Lisp isn't a language it is a building material. Lisp doesn't constrain you to any type of programming, instead it opens up the language for you to develop as you see fit. Macros liberate you from the constraints of the compiler.

"Lisp isn't a language, it's a building material."

There is something equally and perhaps even more true which is that the Java virtual machine (JVM) is also a building material. What opened up my eyes was doing a compiler project for a JVM language. The JVM is a building tool by which can you can build anything you want by generating JVM bytecode.

"The Java virtual machine isn't a language, it's a building material."

The same is true of the Common Language Runtime (CLR), which shares most of the advantages of the JVM. There are a few differences, like the CLR has overloaded arithmetic, reified generics, value types (to be added in the JVM with Valhala), etc. But on a fundamental architectural level, they both share all the most important advantages of each other and they are excellent pieces of technology.

Programming today should surely be done on one of these virtual machines. That is the most important thing, as they can be used as the building material of today for programmers and language developers. I am more comfortable and at home at this point using Java and making use of the JVM then I am with using SBCL and no virtual machine even though the later is a Lisp dialect. In this sense, virtual machines are more important then languages.

This raises the issue: why not use both Lisp and the Java virtual machine at the same time? They are both building materials that you can meld into any form you like: so why not use them together. And of course, that is what we do when programming Clojure, but by far the most important thing is that we have a virtual machine underneath to fall back on.

The Java virtual machine gives us garbage collection, a higher level architecture, a highly optimized just in time compiler, a whole wealth of libraries, a compiler target, and a programming ecosystem with support for multiple languages. In this sense, it is the most important tool in the programmer's arsenal and not the individual language, which is just a nice way of expressing its features.

Knowledge engineering
The title of this blog is Lisp AI, which pays homage to the history of Lisp in artificial intelligence. The phrase artificial intelligence, first coined by John McCarthy, has now evolved to take on many meanings from many different subjects. I am primarily concerned with knowledge engineering and creating ontologies, and so that has been added to the description.

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

Subobject and quotient lattices of functions

Let $f: A \to B$ be a function. Then the topos of functions $Sets^{\to}$ associates $f$ with subobject and quotient lattices. The distributive subobject lattice describes subobjects and functions, and the quotient lattice describes I/O relationships which generalize congruences.

The study of I/O relationships of functions, which is described by topos theory, demonstrates that congruences don't simply belong to abstract algebra but also to set theory and mathematical foundations because they are applicable to any function. We've talked a lot about these lattices associated to functions, but we haven't presented any diagrams of them yet. With the help of clojure and graphviz I can now do that.

(mapfn {:x 1 :y 2 :z 3})

Given a SetFunction object in the topos of functions, we can produce its subobject and quotient lattices as well as perform out operation of computational topos theory like products and coproducts. Towards that end, I have created subobject and quotient lattices of a simple function, which demonstrates that these concepts of universal algebra are applicable even to individual functions.

A notable aspect of the subobject and quotient lattices of functions, is that they tend to expand really quickly, just like power sets which are the subobject lattices of the topos of sets. At the same time, they are trivial for the smallest functions. So a simple function like {:x 1 :y 2 :z 3} is at the sweet spot where its lattice diagrams are not to big or too small.

Subobject lattice:
Congruence lattice:
A notable property that we can infer from the subobject and quotient lattices of a function, from visual inspection is that the smallest subobjects and congruences of functions are determined by relations on the image rather then on the domain. This is because an inherent property of the subobjects and congruences of functions is that they must preserve set and equivalence images.

The atoms in the subobject lattice are elements of the codomain and the atoms in the congruence lattice are equal isations of pairs in the codomain. Only once an element in the codomain has been selected for its inclusion can its fibers in the domain be included into the subobject. Likewise, only once a pair in the codomain has been an equalized can the fibers of its respective element be equalized in the domain partition.

These diagrams are presented for education and research in topos theory, the undoubted foundation of math. Topos theory resolves all the issues of universal algebra, such as the theory of subobjects and congruences, on the level of individual functions. At the same time, it opens up exciting new ground in the theory of I/O relations of functions which have applications in the mathematical dataflow analysis of computation.

Functorality of Green's relations

Green's relations are part of the relationship between order theory and monoid theory. Green's relations can be expressed in category theory as functors from the categories of monoids to the category of preorders, both of which are full subcategories of the category of categories $Cat$.

Theorem. Green's preorders $\subseteq_L, \subseteq_R, \subseteq_J$ are forgetful functors from the category of monoids to the categories of preorders. \[ \subseteq_L : Mon \to Ord \] \[ \subseteq_R : Mon \to Ord \] \[ \subseteq_J : Mon \to Ord \] Proof. (1) suppose that that $a \subseteq_L b$ then $\exists x : xa = b$ which implies that $f(x)f(a) = f(b)$. This implies that $f(a) \subseteq_L f(b)$ by $f(x)$.

(2) similarly, if $a \subseteq_R b$ then $\exists y: ay = b$ which implies that $f(a)f(y) = f(b)$. This implies that $f(a) \subseteq_R f(b)$ by $f(y)$.

(3) finally, by combining the two we have that $a \subseteq_J b$ then $\exists x,y : xay = b$. This implies that $f(x)f(a)f(y) = f(b)$ which implies that $f(a) \subseteq f(b)$ by $f(x)$ and $f(y)$. $\square$

Green's preorders are functors from the category of monoids to the category of preorders, and Green's relations are as well. The only difference is that Green's relations are always symmetric.

Theorem. Green's relations $L,R,J,D,H$ are functors from the category of monoids to the category of preorders.

Proof. (1) suppose that $a \text{ L } b$ then $a \subseteq_L b$ and $b \subseteq_L a$ so by functoriality $f(a) \subseteq_L f(b)$ and $f(b) \subseteq_L f(a)$ which implies that $f(a) \text{ L } f(b)$. The same applies for $R$ and $J$.

(2) suppose that $a \text { H } b$ then $a \text{ L } b$ and $a \text{ R } b$. By part (1) we have that this implies $f(a) \text{ L } f(b)$ and $f(a) \text{ R } f(b)$. By combination this implies $f(a) \text{ H } f(b)$.

(3) finalyl suppose that $a \text{ D } b$ then because $D$ is defined by transitive closure this implies that there is a chain $a \text{ L } x_1 \text{ R } ... \text{ L } x_n \text{ R } b$. Then we can apply $f$ to this chain of relations to get $f(a) \text{ L } f(x_1) \text{ R} ... \text{ L } f(x_n) \text{ R} f(b)$. This implies that $f(a) \text{ D } f(b)$. $\square$

Green's preorders can be defined as the action preorders of monoid actions, but this is not functorial because each monoid has a different topos of monoid actions, so there is no single output category to define a functor for. So we are going to have make do with the functorality of Green's relations for now.

These theorems can be used as a foundation of a number of more advanced constructions in semigroup theory. For example, we can use this to show that monotone maps reflect ideals from which it follows that semigroup morphism reflect ideals as well. That ring maps reflect ideals immediately follows.