Lattices.Free.Substitution¶
Substitutions and the homomorphisms they induce¶
This is the Lattices.Free.Substitution module of the agda-lattices library.
A substitution σ from generators X to generators Y assigns a lattice term
over Y to each generator in X. Applying it to a term t over X replaces
each generator x in t by σ x, and the result t [ σ ] is a term over Y.
Since FL(Y) is the set of terms over Y, a substitution is the same thing as a
map from X to FL(Y), and by the universal property of
Lattices.Free.Universal it extends to a unique
homomorphism FL(X) → FL(Y); this module shows that the extension is
substitution. Every homomorphism FL(X) → FL(Y) arises this way, from its
values on the generators, and the endomorphisms of FL(X) are the substitutions
from X to X.
Substitutions are the maps the rest of the library studies: the sublattice of
FL(Y) generated by n elements is the image of FL(n) under a substitution,
and an endomorphism of FL(n) is given by an n-tuple of its elements.
Lattices.Free.Generation and Lattices.Free.Embedding build on the
facts proved here: substitution is monotone, it commutes with
duality and with joins of lists, the value of a substituted term in any lattice
is the value of the original term under the substituted values (the evaluation
lemma), and an injective substitution reflects Whitman's order. The last
section is the generator inclusion of FL(k) in FL(n) for 0 < k ≤ n, which
reflects equality because it has a left inverse.
The argument order of Sub X Y follows the arrow of the induced
map, FL(X) → FL(Y). The generic substitutions of Setoid.Terms.Basic list
their arguments the other way round; the two never meet, since the free-lattice
development works over LatTerm rather than Term.
Substitutions¶
Sub X Y is the type of substitutions from X to Y, and
t [ σ ] applies σ to t by structural recursion: a generator
is replaced by its image, and the formal operations are kept.
Sub : Type χ → Type υ → Type (χ ⊔ υ) Sub X Y = X → LatTerm Y infixl 30 _[_] _[_] : LatTerm X → Sub X Y → LatTerm Y ℊ x [ σ ] = σ x (s ∧̇ t) [ σ ] = s [ σ ] ∧̇ t [ σ ] (s ∨̇ t) [ σ ] = s [ σ ] ∨̇ t [ σ ]
The generator embedding ℊ is the identity
substitution ([]-ℊ), and substitutions compose:
σ ⨟ τ applies σ and then τ, and applying the composite is
applying the two in turn ([]-⨟). Both equations hold up to
_≡_, by induction on the term.
[]-ℊ : (t : LatTerm X) → t [ ℊ ] ≡ t []-ℊ (ℊ x) = refl []-ℊ (s ∧̇ t) = cong₂ _∧̇_ ([]-ℊ s) ([]-ℊ t) []-ℊ (s ∨̇ t) = cong₂ _∨̇_ ([]-ℊ s) ([]-ℊ t) infixr 9 _⨟_ _⨟_ : Sub X Y → Sub Y Z → Sub X Z (σ ⨟ τ) x = σ x [ τ ] []-⨟ : (t : LatTerm X) (σ : Sub X Y) (τ : Sub Y Z) → t [ σ ⨟ τ ] ≡ t [ σ ] [ τ ] []-⨟ (ℊ x) σ τ = refl []-⨟ (s ∧̇ t) σ τ = cong₂ _∧̇_ ([]-⨟ s σ τ) ([]-⨟ t σ τ) []-⨟ (s ∨̇ t) σ τ = cong₂ _∨̇_ ([]-⨟ s σ τ) ([]-⨟ t σ τ)
Substitution preserves Whitman's order¶
A derivation of s ≤ʷ t by Whitman's rules is carried, rule by rule, to a
derivation of s [ σ ] ≤ʷ t [ σ ] ([]-mono). Substitution
keeps the formal operations, so rules 2, 3, and 6 survive with their own
constructors; rule 1 becomes reflexivity, since both sides become σ x; and
rules 4 and 5, whose generator may become any term, become the weakening lemmas
of Lattices.Free.Whitman that extend them to every
shape. Substitution therefore respects equality in the free lattice
([]-cong), which is what makes it a well-defined map out of
FL(X). (By soundness the same follows from evaluating in FL(Y); the direct
induction keeps the proof syntactic, as the rest of the development is.)
module _ (σ : Sub X Y) where []-mono : s ≤ʷ t → s [ σ ] ≤ʷ t [ σ ] []-mono (∨≤ p q) = ∨≤ ([]-mono p) ([]-mono q) []-mono (ℊ≤∧ p q) = ≤∧ ([]-mono p) ([]-mono q) []-mono (∧≤∧ p q) = ∧≤∧ ([]-mono p) ([]-mono q) []-mono (ℊ≤ℊ refl) = ≤ʷ-refl []-mono (ℊ≤∨ˡ p) = ≤∨ˡ ([]-mono p) []-mono (ℊ≤∨ʳ p) = ≤∨ʳ ([]-mono p) []-mono (∧ˡ≤ℊ p) = ∧ˡ≤ ([]-mono p) []-mono (∧ʳ≤ℊ p) = ∧ʳ≤ ([]-mono p) []-mono (∧ˡ≤∨ p) = ∧ˡ≤∨ ([]-mono p) []-mono (∧ʳ≤∨ p) = ∧ʳ≤∨ ([]-mono p) []-mono (∧≤∨ˡ p) = ∧≤∨ˡ ([]-mono p) []-mono (∧≤∨ʳ p) = ∧≤∨ʳ ([]-mono p) []-cong : s ≈ʷ t → s [ σ ] ≈ʷ t [ σ ] []-cong (p , q) = []-mono p , []-mono q
Substitution is also a congruence in the substitution: substitutions whose
values are pointwise equal in FL(Y) give equal results
([]-congʳ), by induction on the term with the congruence of
the formal operations.
[]-congʳ : (t : LatTerm X) {σ τ : Sub X Y} → (∀ x → σ x ≈ʷ τ x) → t [ σ ] ≈ʷ t [ τ ] []-congʳ (ℊ x) e = e x []-congʳ (s ∧̇ t) e = ∧̇-cong ([]-congʳ s e) ([]-congʳ t e) []-congʳ (s ∨̇ t) e = ∨̇-cong ([]-congʳ s e) ([]-congʳ t e)
Joins, meets, and duals¶
Substitution commutes with the join and the meet of a nonempty list
(⋁⁺-[], ⋀⁺-[]), and with the duality of
Lattices.Free.Duality: the dual of a substituted term is
the dual term under the dual substitution (dual-[]). The
second fact lets a theorem about joins of images be read for meets of images,
as the free generating sets of Lattices.Free.Generation
do.
⋁⁺-[] : (σ : Sub X Y) (u : LatTerm X) (us : List (LatTerm X)) → ⋁⁺ u us [ σ ] ≡ ⋁⁺ (u [ σ ]) (map (_[ σ ]) us) ⋁⁺-[] σ u [] = refl ⋁⁺-[] σ u (w ∷ ws) = cong (u [ σ ] ∨̇_) (⋁⁺-[] σ w ws) ⋀⁺-[] : (σ : Sub X Y) (u : LatTerm X) (us : List (LatTerm X)) → ⋀⁺ u us [ σ ] ≡ ⋀⁺ (u [ σ ]) (map (_[ σ ]) us) ⋀⁺-[] σ u [] = refl ⋀⁺-[] σ u (w ∷ ws) = cong (u [ σ ] ∧̇_) (⋀⁺-[] σ w ws) dual-[] : (t : LatTerm X) (σ : Sub X Y) → dual (t [ σ ]) ≡ dual t [ dual ∘ σ ] dual-[] (ℊ x) σ = refl dual-[] (s ∧̇ t) σ = cong₂ _∨̇_ (dual-[] s σ) (dual-[] t σ) dual-[] (s ∨̇ t) σ = cong₂ _∧̇_ (dual-[] s σ) (dual-[] t σ)
The evaluation lemma¶
In any lattice 𝑳, the value of a substituted term t [ σ ] under an
assignment η of the generators Y is the value of t under the
assignment that sends each x to the value of σ x under η
(⟦[]⟧). This is the lattice-term form of the
substitution lemma of Setoid.Terms.Basic. It holds up to
_≡_, not merely up to the equality of 𝑳, because
evaluation sends each formal operation to the operation of 𝑳
clause by clause.
module _ (𝑳 : Lattice α ρ) where open Evaluation 𝑳 using ( ⟦_⟧ ) open Lattice-Op 𝑳 using ( _∧_ ; _∨_ ) ⟦[]⟧ : (t : LatTerm X) (σ : Sub X Y) (η : Y → 𝕌[ proj₁ 𝑳 ]) → ⟦ t [ σ ] ⟧ η ≡ ⟦ t ⟧ (λ x → ⟦ σ x ⟧ η) ⟦[]⟧ (ℊ x) σ η = refl ⟦[]⟧ (s ∧̇ t) σ η = cong₂ _∧_ (⟦[]⟧ s σ η) (⟦[]⟧ t σ η) ⟦[]⟧ (s ∨̇ t) σ η = cong₂ _∨_ (⟦[]⟧ s σ η) (⟦[]⟧ t σ η)
In the free lattice FL(Y) itself, evaluating a term over X under the
assignment σ is substitution (⟦⟧-[]), because the operations
of FL(Y) are the formal ones. This is the form in which
Setoid.Varieties.SoundAndComplete states its evaluation lemma
for the relatively free algebra 𝔽[ X ], and the special case
σ = ℊ is ⟦⟧-ℊ of Lattices.Free.Universal.
module _ (σ : Sub X Y) where open Evaluation (FL Y) using ( ⟦_⟧ ) ⟦⟧-[] : (t : LatTerm X) → ⟦ t ⟧ σ ≡ t [ σ ] ⟦⟧-[] (ℊ x) = refl ⟦⟧-[] (s ∧̇ t) = cong₂ _∧̇_ (⟦⟧-[] s) (⟦⟧-[] t) ⟦⟧-[] (s ∨̇ t) = cong₂ _∨̇_ (⟦⟧-[] s) (⟦⟧-[] t)
The induced homomorphism¶
Substitution by σ is a setoid map FL(X) → FL(Y), by []-cong,
and a homomorphism (subst-hom): the meet of FL(X) applied to an
argument tuple is the formal meet of its two entries, and substitution sends a
formal meet to the formal meet of the substituted entries, so compatibility holds
by reflexivity, and likewise for joins. By ⟦⟧-[], this is the
homomorphism FL-extend (FL Y) σ of the universal property, with
substitution as its underlying map rather than evaluation. The endomorphisms of
FL(X) are the case Y = X.
module _ (σ : Sub X Y) where subst-hom : hom (proj₁ (FL X)) (proj₁ (FL Y)) subst-hom = mkhom (proj₁ (FL X)) (proj₁ (FL Y)) h (λ {f} → compatible {f}) where h : Func 𝔻[ proj₁ (FL X) ] 𝔻[ proj₁ (FL Y) ] h = record { to = _[ σ ] ; cong = []-cong σ } compatible : compatible-map (proj₁ (FL X)) (proj₁ (FL Y)) h compatible {∧-Op} = ≈ʷ-refl compatible {∨-Op} = ≈ʷ-refl
Every homomorphism is a substitution¶
A homomorphism h from FL(X) to FL(Y) is determined by its
values on the generators, its restriction, which is a
substitution: h agrees on every term with substitution by its
restriction (hom-induced). This is the uniqueness half of the
universal property, FL-extend-unique at 𝑳 = FL Y, read
through ⟦⟧-[].
module _ (h : hom (proj₁ (FL X)) (proj₁ (FL Y))) where restriction : Sub X Y restriction x = proj₁ h ⟨$⟩ ℊ x hom-induced : (t : LatTerm X) → proj₁ h ⟨$⟩ t ≈ʷ t [ restriction ] hom-induced t = subst (proj₁ h ⟨$⟩ t ≈ʷ_) (⟦⟧-[] restriction t) (FL-extend-unique (FL Y) restriction h (λ _ → ≈ʷ-refl) t)
Injective substitutions reflect the order¶
A lattice homomorphism that is injective reflects the order, because the order is
defined by the operations: if s [ σ ] ≤ t [ σ ], then (s ∧ t) [ σ ] and
s [ σ ] are equal, so s ∧ t and s are, and s ≤ t
(injective→reflects). Conversely a substitution that reflects
the order is injective (reflects→injective). Injectivity composes: the composite of
two substitutions whose induced homomorphisms are injective induces an
injective homomorphism (⨟-injective), since applying the
composite applies the two in turn ([]-⨟). An injective
homomorphism FL(X) → FL(Y) is a lattice embedding in the sense of
Freese, Ježek, and Nation (1995), Chapter IX, and these two lemmas let the
later modules use whichever form is convenient.
module _ (σ : Sub X Y) where injective→reflects : IsInjective (proj₁ (subst-hom σ)) → s [ σ ] ≤ʷ t [ σ ] → s ≤ʷ t injective→reflects {s = s} {t} inj p = ≤ʷ-trans (proj₂ (inj {s ∧̇ t} {s} (∧̇-lowerˡ , ≤∧ ≤ʷ-refl p))) ∧̇-lowerʳ reflects→injective : (∀ {s t : LatTerm X} → s [ σ ] ≤ʷ t [ σ ] → s ≤ʷ t) → IsInjective (proj₁ (subst-hom σ)) reflects→injective refl≤ (p , q) = refl≤ p , refl≤ q -- Injectivity composes. ⨟-injective : (σ : Sub X Y) (τ : Sub Y Z) → IsInjective (proj₁ (subst-hom σ)) → IsInjective (proj₁ (subst-hom τ)) → IsInjective (proj₁ (subst-hom (σ ⨟ τ))) ⨟-injective σ τ inj-σ inj-τ {s} {t} e = inj-σ (inj-τ (subst₂ _≈ʷ_ ([]-⨟ s σ τ) ([]-⨟ t σ τ) e))
The generator inclusion¶
For 0 < k ≤ n, the substitution inclusion sends the i-th
generator of FL(k) to the i-th generator of FL(n). It has a left
inverse, the substitution retraction that keeps the first k
generators of FL(n) and sends each of the others to the first one: the
composite fixes every generator of FL(k) (inclusion-⨟-retraction),
so it is the identity on every term, by []-congʳ and
[]-ℊ. The inclusion therefore reflects equality
(inclusion-reflects): FL(k) is a sublattice of FL(n). The
condition 0 < k is what gives the retraction somewhere to send the extra
generators; it is written suc k ≤ n, with Fin (suc k) the generators of
the smaller lattice.
module _ {k n : ℕ} (k<n : suc k ≤ n) where -- The i-th generator of FL(suc k) goes to the i-th generator of FL(n). inclusion : Sub (Fin (suc k)) (Fin n) inclusion i = ℊ (inject≤ i k<n) private -- A generator of FL(n) among the first suc k keeps its place; the others go to the first. shrink : Fin n → Fin (suc k) shrink x with toℕ x <? suc k ... | yes x<k = fromℕ< x<k ... | no _ = zero -- The retraction, a substitution from FL(n) back to FL(suc k). retraction : Sub (Fin n) (Fin (suc k)) retraction x = ℊ (shrink x) private -- Shrinking undoes the injection. shrink-inject≤ : (i : Fin (suc k)) → shrink (inject≤ i k<n) ≡ i shrink-inject≤ i with toℕ (inject≤ i k<n) <? suc k ... | yes p = toℕ-injective (trans (toℕ-fromℕ< p) (toℕ-inject≤ i k<n)) ... | no ¬p = ⊥-elim (¬p (subst (_< suc k) (sym (toℕ-inject≤ i k<n)) (toℕ<n i))) -- The inclusion followed by the retraction fixes every generator. inclusion-⨟-retraction : (i : Fin (suc k)) → (inclusion ⨟ retraction) i ≡ ℊ i inclusion-⨟-retraction i = cong ℊ (shrink-inject≤ i) -- The inclusion reflects equality. inclusion-reflects : {s t : LatTerm (Fin (suc k))} → s [ inclusion ] ≈ʷ t [ inclusion ] → s ≈ʷ t inclusion-reflects {s} {t} e = ≈ʷ-trans (≈ʷ-sym (back s)) (≈ʷ-trans ([]-cong retraction e) (back t)) where -- s [ inclusion ] [ retraction ] is s again. back : (u : LatTerm (Fin (suc k))) → u [ inclusion ] [ retraction ] ≈ʷ u back u = subst₂ _≈ʷ_ ([]-⨟ u inclusion retraction) ([]-ℊ u) ([]-congʳ u λ i → subst (_≈ʷ ℊ i) (sym (inclusion-⨟-retraction i)) ≈ʷ-refl)