Classical.Structures.Lattice.Free¶

Free lattices¶

This is the Classical.Structures.Lattice.Free module of the Agda Universal Algebra Library.

This is a barrel module: it declares nothing of its own and re-exports the modules that construct the free lattice FL(X) and decide its order by Whitman's solution to the word problem (Freese, Ježek, and Nation (1995), Chapter I). The development is syntactic: FL(X) is the set of lattice terms ordered by the relation Whitman's rules define, and the rules are proved sound and complete for the order of every lattice, rather than read off a model built by Day's doubling construction as in the book.

Guide to the submodules of Classical.Structures.Lattice.Free¶

Classical.Structures.Lattice.Free.Term: the lattice terms LatTerm X, their rank, their evaluation in any lattice, and the translation to and from the generic Term X over Sig-Lattice;
Classical.Structures.Lattice.Free.Whitman: Whitman's rules as the inductive relation _≤ʷ_, its decision procedure, reflexivity, transitivity, and formal meet and join as infimum and supremum;
Classical.Structures.Lattice.Free.Universal: the free lattice FL X, soundness and completeness of the rules (Whitman's theorem), and the universal property;
Classical.Structures.Lattice.Free.Derivability: the bridge to equational logic, which makes derivable equality under Th-Lattice, and hence equality in the relatively free algebra 𝔽[ X ], decidable.

The worked example Examples.Classical.Lattices.FreeLattice3 decides a few inequalities in FL(3) by evaluation.

{-# OPTIONS --without-K --exact-split --safe #-}

module Classical.Structures.Lattice.Free where

open import Classical.Structures.Lattice.Free.Derivability  public
open import Classical.Structures.Lattice.Free.Term          public
open import Classical.Structures.Lattice.Free.Universal     public
open import Classical.Structures.Lattice.Free.Whitman       public