It would be useful to be able to compute with a lattice structure. For instance a total lattice (which has all meets, joins, top and bottom).
An important application would be to work with pointless topologies but lattice structures occur across many other area of mathematics.
How do we code such a structure? I would like a representation for a total lattice which is:
- efficient - scales up well.
- fast - for functions like meet and join.
- enforces axioms to minimise runtime checking for errors.
The obvious way to represent is as a directed acyclic graph, but that does not seem specially efficient and it does not enforce the axioms about the existence of meet, join, top and bottom.
| To make the graph representation more efficient for lattices I will start with the observation that the graph of a lattice often contains diamond shapes like this: |  |
So if we code this as a single element it can replace 2 nodes and 4 edges.
| This might appear any place in the graph |  |