Classical.Structures.Lattice.Free.Term¶
Lattice terms¶
This is the Classical.Structures.Lattice.Free.Term module of the Agda Universal Algebra Library.
A lattice term over a set X of generators is a generator, a formal meet of two
lattice terms, or a formal join of two lattice terms. The free lattice FL(X) is
the set of lattice terms modulo the equations that hold in every lattice, and
Whitman's solution to the word problem (Freese, Ježek, and Nation (1995), Theorem
1.11) decides those equations by a structural recursion on pairs of terms. This
module supplies the terms that recursion runs on.
The library already has terms over any signature: Term X of
Overture.Terms.Basic, whose internal nodes carry an operation symbol and a
function from the symbol's arity to the children. Over
Sig-Lattice a meet is node ∧-Op (pair s t), and two such terms
with pointwise-equal children are equal only up to _≐_, since
identifying the two child functions would take function extensionality. That is
the right representation for equational logic, and the wrong one for a recursion
that compares terms by shape. So the free-lattice development works over a
dedicated inductive type, LatTerm X, whose binary constructors
take their children directly, and translates to and from Term X
at the one place the two meet: the bridge to derivability of
Classical.Structures.Lattice.Free.Derivability.
The module provides the type, its rank, its evaluation in any
Lattice, and the two translations with their round trips.
The type of lattice terms¶
LatTerm X has three constructors: ℊ
embeds a generator (the same symbol Term uses for its leaves),
and _∧̇_ and _∨̇_ form
the meet and the join of two terms. The dot over the symbol marks the formal
operation, as the dot in _≈̇_ of
Setoid.Varieties.SoundAndComplete marks a formal equation; the undotted _∧_
and _∨_ remain the operations of a lattice. The two formal operations share
the precedence of the lattice operations of Lattice-Op.
data LatTerm (X : Type χ) : Type χ where ℊ : X → LatTerm X _∧̇_ : LatTerm X → LatTerm X → LatTerm X _∨̇_ : LatTerm X → LatTerm X → LatTerm X infixl 7 _∧̇_ _∨̇_
Rank¶
Freese, Ježek, and Nation (1995), Section I.2, measure a term by its rank: a
generator has rank 1, and a meet or join of k terms has rank one more than the
sum of their ranks, so the rank counts the occurrences of generators plus the
pairs of parentheses. rank is that measure on binary terms. The
book's terms are n-ary and prefer x ∨ y ∨ z (rank 4) to x ∨ (y ∨ z) (rank 5);
a binary term always carries the second form, so its rank is that of the fully
parenthesized reading. The canonical forms of Section I.3, which flatten
iterated joins and meets, live on a type of their own.
rank : LatTerm X → ℕ rank (ℊ x) = 1 rank (s ∧̇ t) = suc (rank s + rank t) rank (s ∨̇ t) = suc (rank s + rank t)
Evaluation in a lattice¶
Given a lattice 𝑳 and an assignment η of elements of
𝑳 to the generators, ⟦ t ⟧ η is the value of t
in 𝑳: generators go to their values under η, and the
formal operations to the curried operations of Lattice-Op.
Evaluation is collected in the module Evaluation, parameterized by
the lattice, in the way Environment of Setoid.Terms.Basic
collects the evaluation of Term; a consumer opens it at the
lattice it works in. ⟦⟧-cong says that evaluation respects
pointwise equality of assignments.
module Evaluation (𝑳 : Lattice α ρ) where open Lattice-Op 𝑳 using ( _∧_ ; _∨_ ; ∧-cong ; ∨-cong ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ) ⟦_⟧ : LatTerm X → (X → 𝕌[ proj₁ 𝑳 ]) → 𝕌[ proj₁ 𝑳 ] ⟦ ℊ x ⟧ η = η x ⟦ s ∧̇ t ⟧ η = ⟦ s ⟧ η ∧ ⟦ t ⟧ η ⟦ s ∨̇ t ⟧ η = ⟦ s ⟧ η ∨ ⟦ t ⟧ η ⟦⟧-cong : (t : LatTerm X) {η η' : X → 𝕌[ proj₁ 𝑳 ]} → (∀ x → η x ≈ η' x) → ⟦ t ⟧ η ≈ ⟦ t ⟧ η' ⟦⟧-cong (ℊ x) η≈η' = η≈η' x ⟦⟧-cong (s ∧̇ t) η≈η' = ∧-cong (⟦⟧-cong s η≈η') (⟦⟧-cong t η≈η') ⟦⟧-cong (s ∨̇ t) η≈η' = ∨-cong (⟦⟧-cong s η≈η') (⟦⟧-cong t η≈η')
Translation to and from Term¶
toTerm sends a lattice term to the Term over
Sig-Lattice with the same shape, packing the two children of each
node with pair; fromTerm reads the children of a
node back at the two positions 0F and 1F of its
arity Fin 2.
toTerm : LatTerm X → Term X toTerm (ℊ x) = ℊ x toTerm (s ∧̇ t) = node ∧-Op (pair (toTerm s) (toTerm t)) toTerm (s ∨̇ t) = node ∨-Op (pair (toTerm s) (toTerm t)) fromTerm : Term X → LatTerm X fromTerm (ℊ x) = ℊ x fromTerm (node ∧-Op ts) = fromTerm (ts 0F) ∧̇ fromTerm (ts 1F) fromTerm (node ∨-Op ts) = fromTerm (ts 0F) ∨̇ fromTerm (ts 1F)
The round trips differ in strength, and the difference is the reason
LatTerm exists. Reading a translated lattice term back gives the
term itself, up to _≡_, by induction (fromTerm-toTerm).
Translating a read-back Term gives a term whose child functions
are pair(ts 0F) (ts 1F) rather than ts; these
agree at every position without being equal functions, so the round trip holds up
to the inductive term equality _≐_ of Setoid.Terms.Basic
(toTerm-fromTerm).
fromTerm-toTerm : (t : LatTerm X) → fromTerm (toTerm t) ≡ t fromTerm-toTerm (ℊ x) = refl fromTerm-toTerm (s ∧̇ t) = cong₂ _∧̇_ (fromTerm-toTerm s) (fromTerm-toTerm t) fromTerm-toTerm (s ∨̇ t) = cong₂ _∨̇_ (fromTerm-toTerm s) (fromTerm-toTerm t) toTerm-fromTerm : (p : Term X) → toTerm (fromTerm p) ≐ p toTerm-fromTerm (ℊ x) = rfl refl toTerm-fromTerm (node ∧-Op ts) = gnl λ { 0F → toTerm-fromTerm (ts 0F) ; 1F → toTerm-fromTerm (ts 1F) } toTerm-fromTerm (node ∨-Op ts) = gnl λ { 0F → toTerm-fromTerm (ts 0F) ; 1F → toTerm-fromTerm (ts 1F) }
The translations preserve values¶
In every lattice the two translations preserve the value of a term under every
assignment, where a Term is evaluated by the generic
Environment of Setoid.Terms.Basic (here renamed ⟦_⟧ᵀ to keep
it apart from the evaluation of lattice terms). Each proof is an induction that,
at a node, feeds the two inductive hypotheses at positions 0F and 1F to
interp-cong. These two lemmas are what let a theorem about
LatTerm speak about Term, and conversely.
module _ (𝑳 : Lattice α ρ) where open Environment (proj₁ 𝑳) using () renaming ( ⟦_⟧ to ⟦_⟧ᵀ ) open Evaluation 𝑳 using ( ⟦_⟧ ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ) renaming ( refl to ≈refl ) ⟦toTerm⟧ : (t : LatTerm X) (η : X → 𝕌[ proj₁ 𝑳 ]) → ⟦ toTerm t ⟧ᵀ ⟨$⟩ η ≈ ⟦ t ⟧ η ⟦toTerm⟧ (ℊ x) η = ≈refl ⟦toTerm⟧ (s ∧̇ t) η = interp-cong (proj₁ 𝑳) ∧-Op λ { 0F → ⟦toTerm⟧ s η ; 1F → ⟦toTerm⟧ t η } ⟦toTerm⟧ (s ∨̇ t) η = interp-cong (proj₁ 𝑳) ∨-Op λ { 0F → ⟦toTerm⟧ s η ; 1F → ⟦toTerm⟧ t η } ⟦fromTerm⟧ : (p : Term X) (η : X → 𝕌[ proj₁ 𝑳 ]) → ⟦ p ⟧ᵀ ⟨$⟩ η ≈ ⟦ fromTerm p ⟧ η ⟦fromTerm⟧ (ℊ x) η = ≈refl ⟦fromTerm⟧ (node ∧-Op ts) η = interp-cong (proj₁ 𝑳) ∧-Op λ { 0F → ⟦fromTerm⟧ (ts 0F) η ; 1F → ⟦fromTerm⟧ (ts 1F) η } ⟦fromTerm⟧ (node ∨-Op ts) η = interp-cong (proj₁ 𝑳) ∨-Op λ { 0F → ⟦fromTerm⟧ (ts 0F) η ; 1F → ⟦fromTerm⟧ (ts 1F) η }