distributive lattices

published on 2019-02-11

Lattices show up everywhere in math and logic. They are as fundamental a building block as the set, the function or the category. And like all of the above, they can be used as a foundational element on which to build all the rest of mathematics and logic. So even though it at least as powerful as established concepts like the function or the set, the lattice isn't as well known. High time for a quick introduction, wouldn't you say?

A lattice is a partially ordered set (L,)(L, \leq) such that for every two elements a,bLa, b \in L there exists both a unique least upper bound (or join) aba \vee b and a unique greatest lower bound (or meet) aba \wedge b.

The canonical examples of lattices is the collection of subsets of any given set XX with the inclusion relation. Indeed, take any two subsets A,BXA, B \subseteq X, then there exists exactly one subset of XX that contains both AA and BB and is contained in every other subset containing AA and BB. To make this more concrete, let's consider a concrete example where XX is the set of all months, A:=January,AprilA:=\{ \text{January}, \text{April}\} and B:=December,April,JulyB:=\{\text{December}, \text{April}, \text{July}\}. Then AB=January,April,July,DecemberA \cup B = \{ \text{January}, \text{April}, \text{July}, \text{December} \} contains both AA and BB. Further, it's clear that any other set containing AA and BB must also contain ABA \cup B. It is precisely the smallest set containing them both, or, in lattice terms, their least upper bound. Completely analogously, ABA \cap B is their greatest lower bound.

Because lattices have such a clear structure, they are easily drawn using Hasse diagrams. In these diagrams, things that are greater with respect to the given relation are placed before lesser elements. Below is the Hasse diagram for a lattice type system that is similar to one you might find in a programing language like Scala. In this example, the objects are types and the relation is given by inheritence. Every type inherits the Object\text{Object} type, and every type is in turn inherited by Nothing\text{Nothing}1. The join of two types is now their earliest shared ancestor. The meet can be thought of the first common successor. In this example, and in fact for most type systems, this will be the Nothing\text{Nothing} type whenever two types are not already in an inheritance relation with eachother. Programming language with multiple inheritance like C++ can have shared successors that are neither of the input types nor the Nothing\text{Nothing} type, but it will generally not be unique.

NothingObjectStringAnimalCowChickenInteger

A particularly useful kind of lattice is the distributive lattice. Those have the additional property that for any three elements a,b,ca, b, c in the lattice, a(bc)=(ab)(bc)a \vee (b \wedge c) = (a \vee b) \wedge (b \vee c). We say that taking joins distributes over taking meets. Somewhat surprisingly, from this it follows that meets distribute over joins as well. Such an equational definition may look convoluted, but the property really is quite natural. Our favorite lattices, the subsets with inclusion relation, are distributive. Indeed, taking the intersection of a subset with the union of two others produces the same result as taking the union of the intersections of the first set with the others. We can think of distributive lattices of being set-like, in a way. This idea is formalized by Birkhoff's representation theorem, which was proven in 1939.

a∨(b∧c)abc(a∨b)∧(b∨c)

Logic is one of the places where distributive lattices show up often. Lattices and logic are so intertwined even, that the symbols for the meet and join operators are overloaded with the logic operators for disjunction and conjunction. Take for example the set of (equivalent) formulas on the single propositional variable pp. They form a very simple distributive lattice for which the meet and join operations behave exactly as you'd expect them to from a classical logic perspective. The formulas of all but the very funkiest of logics form distributed lattices. These special lattices are known as Lindenbaum algebras.

p¬pT

The distributive property is so natural and widespread that it was once thought that all lattices are distributive. Alas, this is not the case. For example, the diamond and pentagram lattices are not distributive. In the diamond, a(bc)=a0=aa \vee (b \wedge c) = a \vee 0 = a, while (ab)(bc)=11=1(a \vee b) \wedge (b \vee c) = 1 \wedge 1 = 1. Can you see why the pentagram is not distributive?

01abc01def

Luckily, these are essentially the only two lattices that are not distributive, in the sense that a lattice is distributive if and only if it does not contain either the diamond or the pentagram as a sublattice. It is reminiscent of Kuratowski's theorem, which states that finite graphs can be drawn without crossing any lines if and only if it does not contain certain subgraphs. Such characterization results are often thought to be among the most beautiful and most useful results in mathematics. They allow us to reframe problems in a different context, connecting distinct fields of mathematics and thereby enabling the use of techniques from one field to prove things about objects in another.

Magic.

1

Nothing types, empty types and uninhabited types are all names for the type without any values. It is useful for strictly typed systems to produce expressions that always match the required type. For example, return expressions are often given a never type so that functions like this typecheck:

fn collatz_terminates(x: u64) -> bool {
    let next: u64 = if x == 1 {
        return true
    } else if x % 2 == 0 {
        x / 2
    } else {
        3 * x + 1
    };
    collatz_terminates(next)
}