Lattices
| L | \(\sqsubseteq\) | \(\sqcap\) | \(\sqcup\) | \(\bot\) | \(\top\) |
|---|---|---|---|---|---|
| Bool | implies | and | or | false | true |
| Reals | \(\leq\) | min | max | \(-\infty\) | \(\infty\) |
| Nat | divides | gcd | lcm | 1 | 0 |
- Substructures of a datatype with substructural ordering
- sets, subset ordering
- list, subsequence ordering
- tree, subtree ordering
Ordering : a relation \(\sqsubseteq :: L \times L \rightarrow Bool\) that satisfy the refl,trans,antisym
\[refl:\ a\sqsubseteq a \qquad trans:\ a\sqsubseteq b \land b \sqsubseteq c \rightarrow a \sqsubseteq c \qquad antisym:\ a \sqsubseteq b \land b \sqsubseteq a \rightarrow a \equiv b\]
Bounded : \(\top,\bot \in L\) that are the upper,lower bounds of ALL elements in L
lattice : meet, join \(\sqcap,\sqcup :: L \times L \rightarrow L\) monoidal operations
\[ a \sqsubseteq c \land b \sqsubseteq c \iff a \sqcup b \sqsubseteq c \]
\[ c \sqsubseteq a \land c \sqsubseteq b \iff c \sqsubseteq a \sqcap b \]
1 Examples
- join
- a < c and b < c then min(a,b) < c
- a divides c and b divides c then gcd(a,b) divides c
2 Laws of Meet and Joins
:Symmetry * min(a,b) = min(b,a) * max(a,b) = max(b,a) * gcd(a,b) = gcd(b,a) * lcm(a,b) = lcm(b,a)
Associativity
- min(a,min(b,c)) = min(a,(min(b,c)))
Idempotency
- min(a,a) = a
Zero
- max(a,inf) = inf
- gcd(a,1) = 1
- lcm(a,0) = 0
Identity
- max(a,-inf) = a
- gcd(a,0)
Absorption
Weakening
