The theory of algebraic graphs
We use Agda to formalise the theory of algebraic graphs and prove a few key theorems.
This repository is fully self-contained and does not depend on any Agda libraries. We use
this Travis build script for continuous
verification of the proofs. To verify whether your implementation is correct,
you can invoke the
Below we describe the purpose of all source files contained in the
Algebrafolder, we define the following structures:
Dioid, a semiring (or rng) where the
+operation is idempotent.
Bool, an implementation of a dioid.
ShortestDistance, another instance.
Graph, an algebraic graphs.
LabelledGraph, an extension of a
for each of these there are three files:
Structure.agda, the main implementation.
Structure/Reasoning.agda, syntactic sugar for writing equational proofs.
Structure/Theorems.agda, some theorems of the structure.
Preludedefines products, lists and other functionality for describing Haskell APIs.
APIdefines key functions from the API of the algebraic-graphs library.
API/Theoremsproves theorems of the API.