Classical.Structures.Lattice.Free.Universal¶
The free lattice and its universal property¶
This is the Classical.Structures.Lattice.Free.Universal module of the Agda Universal Algebra Library.
The free lattice FL(X) on a set X is a lattice generated by X into which
every map from X to a lattice extends, uniquely, to a homomorphism. This module
constructs it from Whitman's order of Classical.Structures.Lattice.Free.Whitman
and proves the universal property, together with the two halves of Whitman's
theorem (Freese, Ježek, and Nation (1995), Theorem 1.11): the rules of
_≤ʷ_ are sound, valid in every lattice under every assignment,
and complete, deriving every inequality that holds in all lattices.
The construction is order first, as the library builds every lattice whose
operations come from an order. The carrier is the set of lattice terms, its
equality is mutual _≤ʷ_, and formal meet and join are the
infimum and supremum of _≤ʷ_; the standard library then derives
the lattice equations, and setoidEqsToLattice packages the result
as a Lattice. Nothing about FL X is quotiented:
its elements are terms, and when equality of generators is decidable, so is its
equality, by _≈ʷ?_.
The proofs of soundness and completeness are short, and their shortness is the
point of the syntactic route. Soundness is an induction on derivations, one line
per rule, each rule valid by the order properties of Classical.Properties.Lattice.
Completeness needs no induction on derivations: an inequality valid in every
lattice is valid in FL X under the assignment of each generator
to itself, which evaluates every term to itself.
The carrier¶
The carrier setoid of FL X is the set of lattice terms under mutual
_≤ʷ_.
FL-setoid : (X : Type χ) → Setoid χ χ FL-setoid X = record { Carrier = LatTerm X ; _≈_ = _≈ʷ_ ; isEquivalence = ≈ʷ-isEquivalence }
The order-theoretic lattice¶
Formal join is the supremum of _≤ʷ_ (FL-supremum):
the two upper-bound clauses are ∨̇-upperˡ and
∨̇-upperʳ, and the least-upper-bound clause is rule 2,
∨≤. Formal meet is the infimum
(FL-infimum), with ≤∧ as the greatest-lower-bound
clause. With reflexivity, transitivity, and antisymmetry (which holds by the
definition of _≈ʷ_), these make the standard library's
order-theoretic lattice FL-OrderLattice X.
FL-supremum : Supremum (_≤ʷ_ {X = X}) _∨̇_ FL-supremum s t = ∨̇-upperˡ , ∨̇-upperʳ , λ u → ∨≤ FL-infimum : Infimum (_≤ʷ_ {X = X}) _∧̇_ FL-infimum s t = ∧̇-lowerˡ , ∧̇-lowerʳ , λ u → ≤∧ FL-isOrderLattice : IsOrderLattice (_≈ʷ_ {X = X}) _≤ʷ_ _∨̇_ _∧̇_ FL-isOrderLattice = record { isPartialOrder = record { isPreorder = record { isEquivalence = ≈ʷ-isEquivalence ; reflexive = proj₁ ; trans = ≤ʷ-trans } ; antisym = _,_ } ; supremum = FL-supremum ; infimum = FL-infimum } FL-OrderLattice : (X : Type χ) → OrderLattice χ χ χ FL-OrderLattice X = record { Carrier = LatTerm X ; _≈_ = _≈ʷ_ ; _≤_ = _≤ʷ_ ; _∨_ = _∨̇_ ; _∧_ = _∧̇_ ; isLattice = FL-isOrderLattice }
The free lattice¶
FL X is the equational lattice the library works with. The eight
equations of Th-Lattice come from the order: the standard
library's algLattice turns FL-OrderLattice X into
an algebraic lattice with commutativity, associativity, congruence, and
absorption, its Properties module supplies idempotence, and the second
absorption law, in the shape (a ∧ b) ∨ a ≈ a that Th-Lattice
states, is read off the order directly. The interpretation clauses of
setoidEqsToLattice apply the argument tuple, so the curried meet
and join of FL X are definitionally _∧̇_
and _∨̇_.
FL : (X : Type χ) → Lattice χ χ FL X = setoidEqsToLattice (FL-setoid X) _∧̇_ _∨̇_ (λ {x} {y} {u} {v} → AL.∧-cong {x} {y} {u} {v}) (λ {x} {y} {u} {v} → AL.∨-cong {x} {y} {u} {v}) (λ {a} {b} {c} → AL.∧-assoc a b c) (λ {a} {b} → AL.∧-comm a b) (λ {a} → AP.∧-idem a) (λ {a} {b} {c} → AL.∨-assoc a b c) (λ {a} {b} → AL.∨-comm a b) (λ {a} → AP.∨-idem a) (λ {a} {b} → AL.∧-absorbs-∨ a b) (∨≤ ∧̇-lowerˡ ≤ʷ-refl , ∨̇-upperʳ) where module OP = OrderLatticeProperties (FL-OrderLattice X) module AL = AlgLatticeBundles.Lattice OP.algLattice module AP = AlgLatticeProperties OP.algLattice
The order of the free lattice is Whitman's order¶
Lattice-Order of Classical.Properties.Lattice equips every
lattice with its meet order, a ≤ b meaning a ∧ b ≈ a. In
FL X that order is _≤ʷ_: one direction is the
infimum property, the other transitivity through the lower bound
∧̇-lowerʳ. The generators are pairwise distinct in
FL X, since two generators are related by rule 1 alone
(ℊ-injective); this is the part of Freese, Ježek, and Nation
(1995), Corollary 1.5, that says x ≤ y implies x = y for generators.
module _ {X : Type χ} where open Lattice-Order (FL X) using ( _≤_ ) ≤ʷ→≤ : s ≤ʷ t → s ≤ t ≤ʷ→≤ p = ∧̇-lowerˡ , ≤∧ ≤ʷ-refl p ≤→≤ʷ : s ≤ t → s ≤ʷ t ≤→≤ʷ (_ , s≤s∧t) = ≤ʷ-trans s≤s∧t ∧̇-lowerʳ ℊ-injective : ℊ x ≈ʷ ℊ y → x ≡ y ℊ-injective (p , _) = ℊ≤ℊ-inv p
Every term evaluates to itself¶
The generic assignment sends each generator x to the term ℊ x. Evaluating a
term in FL X under it rebuilds the term, constructor for
constructor, so every element of FL X is the value of a term in
the generators (⟦⟧-ℊ), and FL X is generated by
X. The equality is propositional, by induction, because the meet and join of
FL X are the formal ones.
module _ {X : Type χ} where open Evaluation (FL X) using ( ⟦_⟧ ) ⟦⟧-ℊ : (t : LatTerm X) → ⟦ t ⟧ ℊ ≡ t ⟦⟧-ℊ (ℊ x) = refl ⟦⟧-ℊ (s ∧̇ t) = cong₂ _∧̇_ (⟦⟧-ℊ s) (⟦⟧-ℊ t) ⟦⟧-ℊ (s ∨̇ t) = cong₂ _∨̇_ (⟦⟧-ℊ s) (⟦⟧-ℊ t)
Validity¶
𝑳 ⊧ s ≤ t says that the inequality s ≤ t holds in the lattice
𝑳 under every assignment of its elements to the generators, for the
meet order of Lattice-Order. It is the inequational counterpart of
the satisfaction relation _⊧_≈_ of
Setoid.Varieties.EquationalLogic, stated for lattice terms.
infix 4 _⊧_≤_ _⊧_≤_ : {X : Type χ} → Lattice α ρ → LatTerm X → LatTerm X → Type (χ ⊔ α ⊔ ρ) _⊧_≤_ {X = X} 𝑳 s t = (η : X → 𝕌[ proj₁ 𝑳 ]) → ⟦ s ⟧ η ≤ ⟦ t ⟧ η where open Evaluation 𝑳 using ( ⟦_⟧ ) open Lattice-Order 𝑳 using ( _≤_ )
Soundness¶
Every rule of _≤ʷ_ is valid in every lattice, so every derivation
is (≤ʷ-sound). The proof is an induction on the derivation with
one clause per constructor: rule 2 is ∨-least, rule 3 is
∧-greatest, rule 1 is reflexivity, and each disjunct of rules 4,
5, and 6 composes the inductive hypothesis with a bound of
Lattice-Order (∨-upperˡ and
∨-upperʳ below a join, ∧-lowerˡ and
∧-lowerʳ above a meet). Antisymmetry turns soundness for
_≤ʷ_ into soundness for _≈ʷ_
(≈ʷ-sound): terms that are equal in FL X have
equal values in every lattice.
module _ (𝑳 : Lattice α ρ) where open Evaluation 𝑳 using ( ⟦_⟧ ) open Lattice-Order 𝑳 using ( ≤-refl ; ≤-trans ; ≤-antisym ; ∧-lowerˡ ; ∧-lowerʳ ; ∧-greatest ; ∨-upperˡ ; ∨-upperʳ ; ∨-least ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ) ≤ʷ-sound : s ≤ʷ t → 𝑳 ⊧ s ≤ t ≤ʷ-sound (∨≤ p q) η = ∨-least (≤ʷ-sound p η) (≤ʷ-sound q η) ≤ʷ-sound (ℊ≤∧ p q) η = ∧-greatest (≤ʷ-sound p η) (≤ʷ-sound q η) ≤ʷ-sound (∧≤∧ p q) η = ∧-greatest (≤ʷ-sound p η) (≤ʷ-sound q η) ≤ʷ-sound (ℊ≤ℊ refl) η = ≤-refl ≤ʷ-sound (ℊ≤∨ˡ p) η = ≤-trans (≤ʷ-sound p η) ∨-upperˡ ≤ʷ-sound (ℊ≤∨ʳ p) η = ≤-trans (≤ʷ-sound p η) ∨-upperʳ ≤ʷ-sound (∧ˡ≤ℊ p) η = ≤-trans ∧-lowerˡ (≤ʷ-sound p η) ≤ʷ-sound (∧ʳ≤ℊ p) η = ≤-trans ∧-lowerʳ (≤ʷ-sound p η) ≤ʷ-sound (∧ˡ≤∨ p) η = ≤-trans ∧-lowerˡ (≤ʷ-sound p η) ≤ʷ-sound (∧ʳ≤∨ p) η = ≤-trans ∧-lowerʳ (≤ʷ-sound p η) ≤ʷ-sound (∧≤∨ˡ p) η = ≤-trans (≤ʷ-sound p η) ∨-upperˡ ≤ʷ-sound (∧≤∨ʳ p) η = ≤-trans (≤ʷ-sound p η) ∨-upperʳ ≈ʷ-sound : s ≈ʷ t → (η : X → 𝕌[ proj₁ 𝑳 ]) → ⟦ s ⟧ η ≈ ⟦ t ⟧ η ≈ʷ-sound (p , q) η = ≤-antisym (≤ʷ-sound p η) (≤ʷ-sound q η)
Completeness¶
Conversely, an inequality that holds in every lattice is derivable
(≤ʷ-complete). It holds in particular in FL X
under the generic assignment, where it reads s ≤ t for the meet order of
FL X, because each side evaluates to itself; and that order is
_≤ʷ_. The hypothesis is needed only for lattices at the level
of X, where FL X lives; together with soundness, which holds
at every level, it is Whitman's theorem (≤ʷ⇔⊧).
≤ʷ-complete : {X : Type χ} {s t : LatTerm X} → ((𝑳 : Lattice χ χ) → 𝑳 ⊧ s ≤ t) → s ≤ʷ t ≤ʷ-complete {X = X} {s} {t} valid = subst₂ _≤ʷ_ (⟦⟧-ℊ s) (⟦⟧-ℊ t) (≤→≤ʷ (valid (FL X) ℊ)) ≤ʷ⇔⊧ : {X : Type χ} {s t : LatTerm X} → s ≤ʷ t ⇔ ((𝑳 : Lattice χ χ) → 𝑳 ⊧ s ≤ t) ≤ʷ⇔⊧ = mk⇔ (λ p 𝑳 → ≤ʷ-sound 𝑳 p) ≤ʷ-complete
The universal property¶
Fix a lattice 𝑳 and a map f from the generators to its
carrier. Evaluation under f is a setoid map out of
FL X (FL-extend), well defined because equal
terms have equal values (≈ʷ-sound). It is a homomorphism
(FL-extend-hom), since it sends each formal operation to the
operation of 𝑳, and it extends f, definitionally
(FL-extend-ℊ). It is the only such homomorphism
(FL-extend-unique): a homomorphism that agrees with
f on the generators agrees with FL-extend on
every term, by induction on the term. So FL X is freely
generated by X.
module _ {X : Type χ} (𝑳 : Lattice α ρ) (f : X → 𝕌[ proj₁ 𝑳 ]) where open Evaluation 𝑳 using ( ⟦_⟧ ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ) renaming ( refl to ≈refl ; trans to ≈trans ) FL-extend : Func 𝔻[ proj₁ (FL X) ] 𝔻[ proj₁ 𝑳 ] FL-extend = record { to = λ t → ⟦ t ⟧ f ; cong = λ s≈t → ≈ʷ-sound 𝑳 s≈t f } FL-extend-compatible : compatible-map (proj₁ (FL X)) (proj₁ 𝑳) FL-extend FL-extend-compatible {∧-Op} = interp-cong (proj₁ 𝑳) ∧-Op λ { 0F → ≈refl ; 1F → ≈refl } FL-extend-compatible {∨-Op} = interp-cong (proj₁ 𝑳) ∨-Op λ { 0F → ≈refl ; 1F → ≈refl } FL-extend-hom : hom (proj₁ (FL X)) (proj₁ 𝑳) FL-extend-hom = mkhom (proj₁ (FL X)) (proj₁ 𝑳) FL-extend FL-extend-compatible FL-extend-ℊ : (x : X) → FL-extend ⟨$⟩ ℊ x ≈ f x FL-extend-ℊ x = ≈refl
The uniqueness proof unfolds h ⟨$⟩ (s ∧̇ t) as h applied to the meet of
FL X at the argument tuple pair s t, moves h inside by its
compatibility with ∧-Op, and closes with the inductive hypotheses at the two
argument positions (args); a join is the same with ∨-Op.
FL-extend-unique : (h : hom (proj₁ (FL X)) (proj₁ 𝑳)) → (∀ x → proj₁ h ⟨$⟩ ℊ x ≈ f x) → (t : LatTerm X) → proj₁ h ⟨$⟩ t ≈ ⟦ t ⟧ f FL-extend-unique h hℊ (ℊ x) = hℊ x FL-extend-unique h hℊ (s ∧̇ t) = ≈trans (IsHom.compatible (proj₂ h) {∧-Op} {pair s t}) (interp-cong (proj₁ 𝑳) ∧-Op args) where args : ∀ i → proj₁ h ⟨$⟩ pair s t i ≈ pair (⟦ s ⟧ f) (⟦ t ⟧ f) i args 0F = FL-extend-unique h hℊ s args 1F = FL-extend-unique h hℊ t FL-extend-unique h hℊ (s ∨̇ t) = ≈trans (IsHom.compatible (proj₂ h) {∨-Op} {pair s t}) (interp-cong (proj₁ 𝑳) ∨-Op args) where args : ∀ i → proj₁ h ⟨$⟩ pair s t i ≈ pair (⟦ s ⟧ f) (⟦ t ⟧ f) i args 0F = FL-extend-unique h hℊ s args 1F = FL-extend-unique h hℊ t