lattice package:lattices

In mathematics, a lattice is a partially ordered set in which every two elements have a unique supremum (also called a least upper bound or join) and a unique infimum (also called a greatest lower bound or meet). In this module lattices are defined using meet and join operators, as it's constructive one.

An algebraic structure with joins and meets. See http://en.wikipedia.org/wiki/Lattice_(order) and http://en.wikipedia.org/wiki/Absorption_law. Lattice is very symmetric, which is seen from the laws: Associativity

x \/ (y \/ z) ≡ (x \/ y) \/ z
x /\ (y /\ z) ≡ (x /\ y) /\ z

Commutativity

x \/ y ≡ y \/ x
x /\ y ≡ y /\ x

Idempotency

x \/ x ≡ x
x /\ x ≡ x

Absorption

a \/ (a /\ b) ≡ a
a /\ (a \/ b) ≡ a

Fine-grained library for constructing and manipulating lattices In mathematics, a lattice is a partially ordered set in which every two elements x and y have a unique supremum (also called a least upper bound, join, or x /\ y) and a unique infimum (also called a greatest lower bound, meet, or x \/ y). This package provide type-classes for different lattice types, as well as a class for the partial order.

A join-semilattice with an identity element bottom for \/. Laws

x \/ bottom ≡ x

Corollary

x /\ bottom
≡⟨ identity ⟩
(x /\ bottom) \/ bottom
≡⟨ absorption ⟩
bottom

A meet-semilattice with an identity element top for /\. Laws

x /\ top ≡ x

Corollary

x \/ top
≡⟨ identity ⟩
(x \/ top) /\ top
≡⟨ absorption ⟩
top