Alga.FSharp

Alga.FSharp is an F# port of the Algebraic graphs library by Andrey Mokhov. The library is .NET Standard, so can be built and run on Windows, Linux and macOS alike.

Checkout, building and editing

To work on Alga.FSharp, I recommend using the cross-platform editor Visual Studio Code with the Ionide extension.

First, ensure you have the following installed:

• .NET Core (https://www.microsoft.com/net/download)
• Visual Studio Code (https://code.visualstudio.com/)
• From inside Visual Studio Code, the Ionide extension

Now, run the following commands in the terminal:

git clone https://github.com/nickcowle/alga-fsharp.git
cd alga-fsharp
dotnet build
code .

Main idea

Consider the following data type, which is defined in the top-level module Graph of the library:

type 'a Graph =
    | Empty
    | Vertex of 'a
    | Overlay of 'a Graph * 'a Graph
    | Connect of 'a Graph * 'a Graph

We can give the following semantics to the constructors in terms of the pair (V, E) of graph vertices and edges:

• Empty constructs the empty graph (∅, ∅).
• Vertex x constructs a graph containing a single vertex, i.e. ({x}, ∅).
• Overlay (x, y) overlays graphs (Vx, Ex) and (Vy, Ey) constructing (Vx ∪ Vy, Ex ∪ Ey).
• Connect (x, y) connects graphs (Vx, Ex) and (Vy, Ey) constructing (Vx ∪ Vy, Ex ∪ Ey ∪ Vx × Vy).

The laws associated with the constructors of this type are remarkably similar to those of a semiring, so we use + and * as convenient shortcuts for Overlay and Connect, respectively:

• (+, Empty) is an idempotent commutative monoid.
• (*, Empty) is a monoid.
• * distributes over +, that is: x * (y + z) == x * y + x * z and (x + y) * z == x * z + y * z.
• * can be decomposed: x * y * z == x * y + x * z + y * z.

This algebraic structure corresponds to unlabelled directed graphs: every expression represents a graph, and every graph can be represented by an expression. Other types of graphs (e.g. undirected) can be obtained by modifying the above set of laws. Algebraic graphs provide a convenient, safe and powerful interface for working with graphs in F#, and allow the application of equational reasoning for proving the correctness of graph algorithms.