## Prelude

In my previous post “Rewrite rules and a specific fold: use optimization techniques from GHC.Base”, I described a technique to optimize composition of a custom fold and some functions on algebraic graphs, implemented in Haskell in the `alga` library.

The goal of this post is to try to specify exactly what are the classes of functions we can optimize. I will try to do this in a “mathematical” way (don’t run, this is actually fun), with all my results proved in Coq, a very cool proof assistant (it is a first time for me, please be indulgent with my code :) ).

All the work can be found at https://github.com/nobrakal/coq-alga/.

The version of this repositiory when I wrote this article can be found at https://github.com/nobrakal/coq-alga/tree/4586bda0847b059b263cc4a1c8685004c9461d6c.

## Alga theory

I had to implement some of the already known algebraic graphs theory in Coq (already know because proved in `agda` on a dedicated repository).

All of this work is in the `src/Graph.v` file:

1. The data structure, an inductive one called `Graph`.
2. Some standards functions (`foldg`, `isEmpty`…).
3. Useful lemmas on them.
4. Axioms on the graph equality (in a Coq class called `EqG`).
5. Indications for Coq to allow rewriting (using the `rewrite` tactic) when working with equal graphs.
6. Some proofs about the graph equality (especially, that `Empty` is the identity for `Overlay`).

### A note on equality

Here the `=` symbol is ambiguous.

So we will distinguish:

• `a = b` for the structural equality (a.k.a. Leibniz equality) between `a` and `b`.
• `R a b` for graph equality relation between `a` and `b` (note that the axioms of this relation are satisfied by others relations than graph equality, so things are not so simple).

## Homomorphism

The work described here can be found in the `src/Homomorphism.v` file.

### Graph homomorphism

An `homomorphism` in algebra theory is (quoting Wikipedia) “a structure-preserving map between two algebraic structures of the same type”.

For us, a correct homomorphism `f :: Graph a -> Graph b` should satisfy:

• `f Empty = Empty`
• `f (Overlay a b) = Overlay (f a) (f b)`
• `f (Connect a b) = Connect (f a) (f b)`

This is encoded in a Coq class called `Homomorphism`:

``````Class Homomorphism {A B:Type} (f : Graph A -> Graph B) : Prop := {
Hom_Empty :> f Empty = Empty;
Hom_Overlay :> forall a b, f (Overlay a b) = Overlay (f a) (f b) ;
Hom_Connect :> forall a b, f (Connect a b) = Connect (f a) (f b)
}.
``````

### Equivalence with bind-functions

Let us recall briefly the concerned Haskell functions:

``````data Graph a = Empty
| Vertex a
| Overlay (Graph a) (Graph a)
| Connect (Graph a) (Graph a)

foldg :: b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> Graph a -> b
foldg e v o c = go
where
go Empty         = e
go (Vertex  x  ) = v x
go (Overlay x y) = o (go x) (go y)
go (Connect x y) = c (go x) (go y)

(>>=) :: Graph a -> (a -> Graph b) -> Graph b
g >>= f = foldg Empty f Overlay Connect g
``````

A cool result is that such homomorphisms are exactly bind-functions, that is to say any graph homomorphism can be expressed with the `(>>=)` operator.

#### Proof

So any function expressed with `(>>=)` is clearly a graph homomorphism (this is proved in the `bind_is_hom` lemma).

A fun fact is that the reciprocal is also true, like shown in the `hom_is_bind` lemma:

``````Lemma hom_is_bind A B (hom: Graph A -> Graph B):
Homomorphism hom -> hom = bind (hom ∘ Vertex).
``````

That is, an homomorphism is equal to `bind` with its definition for a vertex. A graph homomorphism is indeed entirely defined by what it is doing on a leaf of the graph expression.

#### Examples

• `fmap f` is a graph homomorphism, using `Vertex . f` as `bind` argument.
• `removeVertex v` is a graph homomorphism, using `\x -> if v == x then Vertex x else Empty` as `bind` argument.

### Theorem 1: Composition of a graph homomorphism and a foldg function

Any graph homomorphism can be fused with a foldg-function, like show in the `foldg_bind` theorem:

``````Theorem foldg_bind A B C (e : C) (v: B -> C)
(o:C -> C -> C) (c:C -> C -> C) (f_v : A -> Graph B):
foldg e v o c ∘ bind f_v = foldg e (foldg e v o c ∘ f_v) o c.
``````

Basically, because a graph homomorphism preserve the structure, it can easily be fused with something that destruct this structure: this is shortcut deforestation.

### Theorem 2: Composition of graph homomorphisms

A cool corollary of the previous theorem is that the composition of two graph homomorphisms is again a graph homomorphism.

#### Proof

This is proved in the `bind_compo` theorem:

``````Theorem bind_compo A B C (hom1 : Graph A -> Graph B) (hom2 : Graph B -> Graph C):
(Homomorphism hom1) /\ (Homomorphism hom2) ->
hom2 ∘ hom1 = bind (hom2 ∘ hom1 ∘ Vertex).
``````

### Problems

So graph homomorphisms are cool, but not always what we want: in the examples of graph homomorphisms, `removeVertex` is leaving empty leaves in the structure. If it was removing them (like the actual `removeVertex` in the `alga` library), it will change the graph structure, and thus will not be a graph homomorphism as we defined it. Such functions are very useful, so we must lower our restrictions and only require preservation of the graph equality to include them.

## Reduced graph homomorphism

Theorems of this section are in the `src/ReducedHomo.v` file.

### Definition

A function `f :: Graph a -> Graph b` is called a reduced graph homomorphism if:

``````R (f Empty) Empty
R (f (Overlay a b)) (Overlay (f a) (f b))
R (f (Connect a b)) (Connect (f a) (f b))
``````

So we require only that the function has the same properties than a graph homomorphism, but with graph equality instead of the structural one.

This idea is encapsulated in the `Reduced_hom` Coq class:

``````Class Reduced_hom {A B : Type} (R: relation (Graph B)) (f : Graph A -> Graph B) : Prop :=
{
RHom_EqG :> EqG B R;
RHom_Empty :>  R (f Empty) Empty ;
RHom_Overlay :> forall a b, R (f (Overlay a b)) (Overlay (f a) (f b)) ;
RHom_Connect :> forall a b, R (f (Connect a b)) (Connect (f a) (f b))
}.
``````

### Theorem 3: Reduced graph homomorphism are indeed reduced graph homomorphism

Graph homomorphism are reduced graph homomorphism.

The reverse is false.

#### Proof

• “graph homomorphism are reduced graph homomorphism.”

This is proved in the `hom_is_reduced_hom` theorem.

The idea is only to use the fact that, for all `a b :: Graph A`, if `a = b` then `R a b`.

• “The reverse is false”. Using
``````wforget :: Graph a -> Graph b
wforget _ = Empty
``````

`wforget` is clearly a reduced homomorphism (this is proved in the `const_empty_is_reduced_hom` theorem).

But it is also clearly not a graph homorphism, this is proved by the absurd in the `const_empty_is_not_hom` theorem.

## The case of empty leaves: a class of reduced graph homomorphism

Theorems of this section are in the `src/SmartHomo.v` file.

#### Prelude

``````-- Remove empty leaves around a graph operator (usually Overlay or Connect)
kSimpl :: (Graph a -> Graph a -> Graph a) -> Graph a -> Graph a -> Graph a
kSimpl c x y =
if isEmpty x
then if isEmpty y
then Empty
else y
else if isEmpty y
then x
else c x y

-- Remove empty leaves of a graph
dropEmpty :: Graph a -> Graph a
dropEmpty = foldg Empty Vertex (kSimpl Overlay) (kSimpl Connect)
``````

### Definition

A function `f :: Graph a -> Graph b` is called a smart graph homomorphism if it can be described using `f_w :: a -> Graph b` such that

``````f g = dropEmpty (g >>= f_w)
``````

Obviously, such a function can go through the graph only once, using

``````f = foldg Empty f_w (kSimpl Overlay) (kSimpl Connect)
``````

This is proved in the `smart_hom_single` theorem.

#### Example

`induce` is a smart graph homomorphism (maybe the definition was made for it…):

``````induce :: (p -> Bool) -> Graph a -> Graph a
induce p =
foldg
Empty
(\x -> if p x then Vertex x else Empty)
(kSimpl Overlay)
(kSimpl Connect)
``````

This is proved in the `induce_smart_hom` theorem.

### Theorem 4: smart graph homomorphisms are reduced homomorphisms.

This seems clear because empty leaves does not play any role in graph equality, but it takes me anyway 44 lines to prove it.

It is proved in the `smart_hom_is_reduced_hom` theorem:

``````Theorem smart_hom_is_reduced_hom A B (R: relation (Graph B))
(f : Graph A -> Graph B) :
EqG B R -> Smart_hom f -> Reduced_hom R f.
``````

### Theorem 5: Composition of smart graph homomorphisms

The composition of two smart graph homomorphisms is again a smart graph homomorphism.

#### Proof

This was hard to prove because not clear at first glance (well mostly, it was long, using 280 lines ^^). The idea is to see that the composition of two smart graph homomorphisms is something not so strange:

``````Theorem smart_hom_compo A B C (s1 : Graph A -> Graph B)
(s2 : Graph B -> Graph C): (Smart_hom s1) /\ (Smart_hom s2) ->
s2 ∘ s1 = foldg Empty (s2 ∘ s1 ∘ Vertex) (kSimpl Overlay) (kSimpl Connect).
``````

(The proof is here).

Then see that this form allow us to prove that the composition is again a smart graph morphism:

``````Theorem smart_hom_compo_is_smart A B C (s1 : Graph A -> Graph B)
(s2 : Graph B -> Graph C):
(Smart_hom s1) /\ (Smart_hom s2) -> Smart_hom (s2 ∘ s1).
``````

(The proof is here).

## Conclusion

So all this work to prove that we can optimize anything like:

``````foldg e v o c . morph1 . morph2 . [...] . morphn
``````

to a function that will only go through the graph once.

if `morph1`, `morph2`, …, `morphn` are graph homomorphisms (theorem 1 and theorem 2).

We can also optimize any combination of smart graph homomorphisms (theorem 5).

### What is left

There is certainly some things to do playing with these results:

• Find a cool (and efficient) implementation for the `alga` library.
• The composition of smart graph homomorphisms is preserving graph structure, maybe there is an efficient one that is only preserving graph equality ?
• Determine precisely the class of reduced homomorphisms. That is to say, is there an equivalence with a well known class of functions like for graph homomorphisms ?
• What is the class of reduced homomorphisms that we can compose ?
• Can this be generalised to arbitrary algebraic data types that have some notion of an Empty constructor?
• And certainly many other things :)

#### Thanks

Thanks to Andrey Mokhov for his review of this article.