Agda UALib ↑

---

Term Operations

This section presents the Terms.Operations module of the Agda Universal Algebra Library.

Here we define term operations which are simply terms interpreted in a particular algebra, and we prove some compatibility properties of term operations.

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

open import Algebras.Signatures using (Signature; 𝓞; 𝓥)

module Terms.Operations {𝑆 : Signature 𝓞 𝓥} where

open import Terms.Basic{𝑆 = 𝑆} renaming (generator to ℊ) public

Notation. In the line above, we renamed for notational convenience the generator constructor of the Term type, so from now on we use ℊ in place of generator.

When we interpret a term in an algebra we call the resulting function a term operation. Given a term 𝑝 and an algebra 𝑨, we denote by 𝑝 ̇ 𝑨 the interpretation of 𝑝 in 𝑨. This is defined inductively as follows.

1. If 𝑝 is a variable symbol x : X and if 𝑎 : X → ∣ 𝑨 ∣ is a tuple of elements of ∣ 𝑨 ∣, then (𝑝 ̇ 𝑨) 𝑎 := 𝑎 x.

2. If 𝑝 = 𝑓 𝑡, where 𝑓 : ∣ 𝑆 ∣ is an operation symbol, if 𝑡 : ∥ 𝑆 ∥ 𝑓 → 𝑻 X is a tuple of terms, and if 𝑎 : X → ∣ 𝑨 ∣ is a tuple from 𝑨, then we define (𝑝 ̇ 𝑨) 𝑎 = (𝑓 𝑡 ̇ 𝑨) 𝑎 := (𝑓 ̂ 𝑨) (λ i → (𝑡 i ̇ 𝑨) 𝑎).

Thus the interpretation of a term is defined by induction on the structure of the term, and the definition is formally implemented in the UALib as follows.

module _ {𝓤 𝓧 : Universe}{X : 𝓧 ̇ }  where

 -- new notation

 _⟦_⟧ : (𝑨 : Algebra 𝓤 𝑆) → Term X → (X → ∣ 𝑨 ∣) → ∣ 𝑨 ∣

 𝑨 ⟦ ℊ x ⟧ = λ η → η x

 𝑨 ⟦ node 𝑓 𝑡 ⟧ = λ η → (𝑓 ̂ 𝑨) (λ i → (𝑨 ⟦ 𝑡 i ⟧) η)



 -- old notation:

 _̇_ : Term X → (𝑨 : Algebra 𝓤 𝑆) → (X → ∣ 𝑨 ∣) → ∣ 𝑨 ∣

 (ℊ x ̇ 𝑨) 𝑎 = 𝑎 x

 (node 𝑓 𝑡 ̇ 𝑨) 𝑎 = (𝑓 ̂ 𝑨) λ i → (𝑡 i ̇ 𝑨) 𝑎

It turns out that the intepretation of a term is the same as the free-lift (modulo argument order and assuming function extensionality).

 free-lift-interp : dfunext 𝓥 𝓤 → (𝑨 : Algebra 𝓤 𝑆)(η : X → ∣ 𝑨 ∣)(p : Term X)
  →                 (𝑨 ⟦ p ⟧) η ≡ (free-lift 𝑨 η) p

 free-lift-interp _ 𝑨 η (ℊ x) = refl
 free-lift-interp fe 𝑨 η (node 𝑓 𝑡) = ap (𝑓 ̂ 𝑨) (fe λ i → free-lift-interp fe 𝑨 η (𝑡 i))

 -- old version
 free-lift-interp' : dfunext 𝓥 𝓤 → (𝑨 : Algebra 𝓤 𝑆)(h : X → ∣ 𝑨 ∣)(p : Term X)
  →                 (p ̇ 𝑨) h ≡ (free-lift 𝑨 h) p

 free-lift-interp' _ 𝑨 h (ℊ x) = refl
 free-lift-interp' fe 𝑨 h (node 𝑓 𝑡) = ap (𝑓 ̂ 𝑨) (fe λ i → free-lift-interp' fe 𝑨 h (𝑡 i))

If the algebra 𝑨 happens to be 𝑻 X, then we expect that ∀ 𝑠 we have (p ̇ 𝑻 X) 𝑠 ≡ p 𝑠. But what is (𝑝 ̇ 𝑻 X) 𝑠 exactly? By definition, it depends on the form of 𝑝 as follows:

• if 𝑝 = ℊ x, then (𝑝 ̇ 𝑻 X) 𝑠 := (ℊ x ̇ 𝑻 X) 𝑠 ≡ 𝑠 x

• if 𝑝 = node 𝑓 𝑡, then (𝑝 ̇ 𝑻 X) 𝑠 := (node 𝑓 𝑡 ̇ 𝑻 X) 𝑠 = (𝑓 ̂ 𝑻 X) λ i → (𝑡 i ̇ 𝑻 X) 𝑠

Now, assume ϕ : hom 𝑻 𝑨. Then by comm-hom-term, we have ∣ ϕ ∣ (p ̇ 𝑻 X) 𝑠 = (p ̇ 𝑨) ∣ ϕ ∣ ∘ 𝑠.

• if p = ℊ x (and 𝑡 : X → ∣ 𝑻 X ∣), then

  ∣ ϕ ∣ p ≡ ∣ ϕ ∣ (ℊ x) ≡ ∣ ϕ ∣ (λ 𝑡 → h 𝑡) ≡ λ 𝑡 → (∣ ϕ ∣ ∘ 𝑡) x

• if p = node 𝑓 𝑡, then

  ∣ ϕ ∣ p ≡ ∣ ϕ ∣ (p ̇ 𝑻 X) 𝑠 = (node 𝑓 𝑡 ̇ 𝑻 X) 𝑠 = (𝑓 ̂ 𝑻 X) λ i → (𝑡 i ̇ 𝑻 X) 𝑠

We claim that for all p : Term X there exists q : Term X and 𝔱 : X → ∣ 𝑻 X ∣ such that p ≡ (q ̇ 𝑻 X) 𝔱. We prove this fact as follows.

term-interp : {𝓧 : Universe}{X : 𝓧 ̇} (𝑓 : ∣ 𝑆 ∣){𝑠 𝑡 : ∥ 𝑆 ∥ 𝑓 → Term X}
 →            𝑠 ≡ 𝑡 → node 𝑓 𝑠 ≡ (𝑓 ̂ 𝑻 X) 𝑡

term-interp 𝑓 {𝑠}{𝑡} st = ap (node 𝑓) st

module _ {𝓧 : Universe}{X : 𝓧 ̇}{fe : dfunext 𝓥 (ov 𝓧)} where

 term-gen : (p : ∣ 𝑻 X ∣) → Σ q ꞉ ∣ 𝑻 X ∣ , p ≡ (𝑻 X ⟦ q ⟧) ℊ
 term-gen (ℊ x) = (ℊ x) , refl
 term-gen (node 𝑓 𝑡) = node 𝑓 (λ i → ∣ term-gen (𝑡 i) ∣) , term-interp 𝑓 (fe λ i → ∥ term-gen (𝑡 i) ∥)


 term-gen-agreement : (p : ∣ 𝑻 X ∣) → (𝑻 X ⟦ p ⟧) ℊ ≡ (𝑻 X ⟦ ∣ term-gen p ∣ ⟧) ℊ
 term-gen-agreement (ℊ x) = refl
 term-gen-agreement (node f 𝑡) = ap (f ̂ 𝑻 X) (fe λ x → term-gen-agreement (𝑡 x))

 term-agreement : (p : ∣ 𝑻 X ∣) → p ≡  (𝑻 X ⟦ p ⟧) ℊ
 term-agreement p = snd (term-gen p) ∙ (term-gen-agreement p)⁻¹

 -- old version:
 term-gen' : (p : ∣ 𝑻 X ∣) → Σ q ꞉ ∣ 𝑻 X ∣ , p ≡ (q ̇ 𝑻 X) ℊ
 term-gen' (ℊ x) = (ℊ x) , refl
 term-gen' (node 𝑓 𝑡) = node 𝑓 (λ i → ∣ term-gen' (𝑡 i) ∣) , term-interp 𝑓 (fe λ i → ∥ term-gen' (𝑡 i) ∥)


 term-gen-agreement' : (p : ∣ 𝑻 X ∣) → (p ̇ 𝑻 X) ℊ ≡ (∣ term-gen' p ∣ ̇ 𝑻 X) ℊ
 term-gen-agreement' (ℊ x) = refl
 term-gen-agreement' (node f 𝑡) = ap (f ̂ 𝑻 X) (fe λ x → term-gen-agreement' (𝑡 x))

 term-agreement' : (p : ∣ 𝑻 X ∣) → p ≡ (p ̇ 𝑻 X) ℊ
 term-agreement' p = snd (term-gen' p) ∙ (term-gen-agreement' p)⁻¹

Interpretation of terms in product algebras

module _ {𝓤 𝓦 𝓧 : Universe}{X : 𝓧 ̇ }{I : 𝓦 ̇} where

 interp-prod : dfunext 𝓥 (𝓤 ⊔ 𝓦) → (p : Term X)(𝒜 : I → Algebra 𝓤 𝑆)(𝑎 : X → ∀ i → ∣ 𝒜 i ∣)
  →            (⨅ 𝒜 ⟦ p ⟧) 𝑎 ≡ λ i →  (𝒜 i ⟦ p ⟧) (λ j → 𝑎 j i)

 interp-prod _ (ℊ x₁) 𝒜 𝑎 = refl

 interp-prod fe (node 𝑓 𝑡) 𝒜 𝑎 = let IH = λ x → interp-prod fe (𝑡 x) 𝒜 𝑎
  in
  (𝑓 ̂ ⨅ 𝒜) (λ x → (⨅ 𝒜 ⟦ 𝑡 x ⟧) 𝑎)                     ≡⟨ ap (𝑓 ̂ ⨅ 𝒜)(fe IH) ⟩
  (𝑓 ̂ ⨅ 𝒜)(λ x → λ i →  (𝒜 i ⟦ 𝑡 x ⟧) λ j → 𝑎 j i)   ≡⟨ refl ⟩
  (λ i → (𝑓 ̂ 𝒜 i) (λ x → (𝒜 i ⟦ 𝑡 x ⟧) λ j → 𝑎 j i))  ∎

 -- inferred type: 𝑡 : X → ∣ ⨅ 𝒜 ∣
 interp-prod2 : dfunext (𝓤 ⊔ 𝓦 ⊔ 𝓧) (𝓤 ⊔ 𝓦) → dfunext 𝓥 (𝓤 ⊔ 𝓦) → (p : Term X)(𝒜 : I → Algebra 𝓤 𝑆)
  →             ⨅ 𝒜 ⟦ p ⟧ ≡ (λ 𝑡 → (λ i → (𝒜 i ⟦ p ⟧) λ x → 𝑡 x i))

 interp-prod2 _ _ (ℊ x₁) 𝒜 = refl

 interp-prod2 fe fev (node f t) 𝒜 = fe λ (tup : X → ∣ ⨅ 𝒜 ∣) →
  let IH = λ x → interp-prod fev (t x) 𝒜  in
  let tA = λ z →  ⨅ 𝒜 ⟦ t z ⟧ in
  (f ̂ ⨅ 𝒜)(λ s → tA s tup)                          ≡⟨ ap(f ̂ ⨅ 𝒜)(fev λ x → IH x tup)⟩
  (f ̂ ⨅ 𝒜)(λ s → λ j → (𝒜 j ⟦ t s ⟧) (λ ℓ → tup ℓ j))   ≡⟨ refl ⟩
  (λ i → (f ̂ 𝒜 i)(λ s →  (𝒜 i ⟦ t s ⟧) (λ ℓ → tup ℓ i))) ∎

module _ {𝓤 𝓧 : Universe}{X : 𝓧 ̇ } where

 interp-prod' : {𝓦 : Universe} → dfunext 𝓥 (𝓤 ⊔ 𝓦)
  →             (p : Term X){I : 𝓦 ̇}
                (𝒜 : I → Algebra 𝓤 𝑆)(𝑎 : X → ∀ i → ∣ 𝒜 i ∣)
                ---------------------------------------------------
  →             (p ̇ (⨅ 𝒜)) 𝑎 ≡ (λ i → (p ̇ 𝒜 i) (λ j → 𝑎 j i))

 interp-prod' _ (ℊ x₁) 𝒜 𝑎 = refl

 interp-prod' fe (node 𝑓 𝑡) 𝒜 𝑎 = let IH = λ x → interp-prod' fe (𝑡 x) 𝒜 𝑎
  in
  (𝑓 ̂ ⨅ 𝒜)(λ x → (𝑡 x ̇ ⨅ 𝒜) 𝑎)                      ≡⟨ ap (𝑓 ̂ ⨅ 𝒜)(fe IH) ⟩
  (𝑓 ̂ ⨅ 𝒜)(λ x → (λ i → (𝑡 x ̇ 𝒜 i)(λ j → 𝑎 j i)))   ≡⟨ refl ⟩
  (λ i → (𝑓 ̂ 𝒜 i) (λ x → (𝑡 x ̇ 𝒜 i)(λ j → 𝑎 j i)))  ∎


 interp-prod2' : dfunext (𝓤 ⊔ 𝓧) 𝓤 → dfunext 𝓥 𝓤
  →              (p : Term X){I : 𝓤 ̇ }(𝒜 : I → Algebra 𝓤 𝑆)
                 ------------------------------------------------------------------
  →              (p ̇ ⨅ 𝒜) ≡ λ(𝑡 : X → ∣ ⨅ 𝒜 ∣) → (λ i → (p ̇ 𝒜 i)(λ x → 𝑡 x i))

 interp-prod2' _ _ (ℊ x₁) 𝒜 = refl

 interp-prod2' fe fev (node f t) 𝒜 = fe λ (tup : X → ∣ ⨅ 𝒜 ∣) →
  let IH = λ x → interp-prod' fev (t x) 𝒜  in
  let tA = λ z → t z ̇ ⨅ 𝒜 in
  (f ̂ ⨅ 𝒜)(λ s → tA s tup)                          ≡⟨ ap(f ̂ ⨅ 𝒜)(fev λ x → IH x tup)⟩
  (f ̂ ⨅ 𝒜)(λ s → λ j → (t s ̇ 𝒜 j)(λ ℓ → tup ℓ j))   ≡⟨ refl ⟩
  (λ i → (f ̂ 𝒜 i)(λ s → (t s ̇ 𝒜 i)(λ ℓ → tup ℓ i))) ∎

Compatibility of terms

We now prove two important facts about term operations. The first of these, which is used very often in the sequel, asserts that every term commutes with every homomorphism.

module _ {𝓤 𝓦 𝓧 : Universe}{X : 𝓧 ̇} where

 comm-hom-term : dfunext 𝓥 𝓦 → {𝑨 : Algebra 𝓤 𝑆} (𝑩 : Algebra 𝓦 𝑆)
                 (h : hom 𝑨 𝑩) (t : Term X) (a : X → ∣ 𝑨 ∣)
                 -----------------------------------------
  →              ∣ h ∣ ((𝑨 ⟦ t ⟧) a) ≡ (𝑩 ⟦ t ⟧) (∣ h ∣ ∘ a)

 comm-hom-term _ 𝑩 h (ℊ x) a = refl

 comm-hom-term fe {𝑨} 𝑩 h (node 𝑓 𝑡) a = ∣ h ∣((𝑓 ̂ 𝑨) λ i →  (𝑨 ⟦ 𝑡 i ⟧) a)    ≡⟨ i  ⟩
                                     (𝑓 ̂ 𝑩)(λ i →  ∣ h ∣ ((𝑨 ⟦ 𝑡 i ⟧) a))  ≡⟨ ii ⟩
                                     (𝑓 ̂ 𝑩)(λ r → (𝑩 ⟦ 𝑡 r ⟧) (∣ h ∣ ∘ a)) ∎
  where
  i  = ∥ h ∥ 𝑓 λ r → (𝑨 ⟦ 𝑡 r ⟧) a
  ii = ap (𝑓 ̂ 𝑩)(fe (λ i → comm-hom-term fe 𝑩 h (𝑡 i) a))

 comm-hom-term' : dfunext 𝓥 𝓦 → {𝑨 : Algebra 𝓤 𝑆} (𝑩 : Algebra 𝓦 𝑆)
                  (h : hom 𝑨 𝑩) (t : Term X) (a : X → ∣ 𝑨 ∣)
                  -----------------------------------------
  →               ∣ h ∣ ((𝑨 ⟦ t ⟧) a) ≡ (𝑩 ⟦ t ⟧) (∣ h ∣ ∘ a)

 comm-hom-term' _ 𝑩 h (ℊ x) a = refl

 comm-hom-term' fe {𝑨} 𝑩 h (node 𝑓 𝑡) a = ∣ h ∣ ((𝑓 ̂ 𝑨)λ i → (𝑨 ⟦ 𝑡 i ⟧) a)    ≡⟨ i  ⟩
                                     (𝑓 ̂ 𝑩)(λ i →  ∣ h ∣ ((𝑨 ⟦ 𝑡 i ⟧) a))  ≡⟨ ii ⟩
                                     (𝑓 ̂ 𝑩)(λ r → (𝑩 ⟦ 𝑡 r ⟧) (∣ h ∣ ∘ a)) ∎
  where
  i  = ∥ h ∥ 𝑓 λ r → (𝑨 ⟦ 𝑡 r ⟧) a
  ii = ap (𝑓 ̂ 𝑩)(fe (λ i → comm-hom-term' fe 𝑩 h (𝑡 i) a))

To conclude this module, we prove that every term is compatible with every congruence relation. That is, if t : Term X and θ : Con 𝑨, then a θ b → t(a) θ t(b). (Recall, the compatibility relation |: was defined in Relations.Discrete.)

module _ {𝓦 𝓤 : Universe}{X : 𝓤 ̇} where

 open IsCongruence

 _∣:_ : {𝑨 : Algebra 𝓤 𝑆}(t : Term X)(θ : Con{𝓦} 𝑨)
        -----------------------------------------
  →     (𝑨 ⟦ t ⟧) |: ∣ θ ∣

 ((ℊ x) ∣: θ) p = p x

 ((node 𝑓 𝑡) ∣: θ) p = (is-compatible ∥ θ ∥) 𝑓 λ x → ((𝑡 x) ∣: θ) p

For the sake of comparison, here is the analogous theorem using compatible-fun.

 compatible-term : {𝑨 : Algebra 𝓤 𝑆}(t : Term X)(θ : Con{𝓦} 𝑨)
                   -----------------------------------------
  →                compatible-fun (𝑨 ⟦ t ⟧) ∣ θ ∣

 compatible-term (ℊ x) θ p = λ y z → z x

 compatible-term (node 𝑓 𝑡) θ u v p = (is-compatible ∥ θ ∥) 𝑓 λ x → ((compatible-term (𝑡 x) θ) u v) p

 compatible-term' : {𝑨 : Algebra 𝓤 𝑆}(t : Term X)(θ : Con{𝓦} 𝑨)
                   -----------------------------------------
  →                compatible-fun (t ̇ 𝑨) ∣ θ ∣

 compatible-term' (ℊ x) θ p = λ y z → z x

 compatible-term' (node 𝑓 𝑡) θ u v p = (is-compatible ∥ θ ∥) 𝑓 λ x → ((compatible-term' (𝑡 x) θ) u v) p

---

¹We plan to resolve this before the next major release of the Agda UALib.

← Terms.Basic Subalgebras →