Skip to content

Legacy.Base.Terms.Operations

Term Operations

This section presents the Legacy.Base.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 --cubical-compatible --exact-split --safe #-}

open import Overture using ( š“ž ; š“„ ; Signature )

module Legacy.Base.Terms.Operations {š‘† : Signature š“ž š“„} where

-- Imports from Agda and the Agda Standard Library ---------------------
open import Agda.Primitive  using ()  renaming ( Set to Type )
open import Data.Product    using ( _,_ ; Ī£-syntax ; Ī£ )
open import Function        using ( _āˆ˜_ )
open import Level           using ( Level ; _āŠ”_ )
open import Relation.Binary.PropositionalEquality as ā‰”
                            using ( _ā‰”_ ; module ā‰”-Reasoning )
open import Axiom.Extensionality.Propositional
                            using () renaming (Extensionality to funext)

-- Imports from Agda Universal Algebra Library ----------------------------------------------
open import Overture        using ( _āˆ™_ ; _ā»Ā¹ ; āˆ£_āˆ£ ; āˆ„_āˆ„ ; Ī  ; Ī -syntax ; _ā‰ˆ_ )
open import Legacy.Base.Relations  using ( _|:_ )
open import Legacy.Base.Equality   using ( swelldef )

open import Legacy.Base.Algebras          {š‘† = š‘†}  using ( Algebra ; _Ģ‚_ ; ov ; ā؅ )
                                            using ( IsCongruence ; Con )
open import Legacy.Base.Homomorphisms     {š‘† = š‘†}  using ( hom )
open import Legacy.Base.Terms.Basic       {š‘† = š‘†}  using ( Term ; š‘» )
open import Legacy.Base.Terms.Properties  {š‘† = š‘†}  using ( free-lift )

open Term
private variable Ī± Ī² Ī³ Ļ Ļ‡ : Level

When we interpret a term in an algebra we call the resulting function a term operation. Given a term p and an algebra š‘Ø, we denote by š‘Ø āŸ¦ p āŸ§ the interpretation of p in š‘Ø. This is defined inductively as follows.

  1. If p is a variable symbol x : X and if a : X ā†’ āˆ£ š‘Ø āˆ£ is a tuple of elements of āˆ£ š‘Ø āˆ£, then š‘Ø āŸ¦ p āŸ§ a := a x.

  2. If p = f t, where f : āˆ£ š‘† āˆ£ is an operation symbol, if t : āˆ„ š‘† āˆ„ f ā†’ š‘» X is a tuple of terms, and if a : X ā†’ āˆ£ š‘Ø āˆ£ is a tuple from š‘Ø, then we define š‘Ø āŸ¦ p āŸ§ a = š‘Ø āŸ¦ f t āŸ§ a := (f Ģ‚ š‘Ø) (Ī» i ā†’ š‘Ø āŸ¦ t i āŸ§ a).

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


_āŸ¦_āŸ§ : (š‘Ø : Algebra Ī±){X : Type Ļ‡ } ā†’ Term X ā†’ (X ā†’ āˆ£ š‘Ø āˆ£) ā†’ āˆ£ š‘Ø āˆ£
š‘Ø āŸ¦ ā„Š x āŸ§ = Ī» Ī· ā†’ Ī· x
š‘Ø āŸ¦ node f t āŸ§ = Ī» Ī· ā†’ (f Ģ‚ š‘Ø) (Ī» i ā†’ (š‘Ø āŸ¦ t 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 :  swelldef š“„ Ī± ā†’ (š‘Ø : Algebra Ī±){X : Type Ļ‡ }
                    (Ī· : X ā†’ āˆ£ š‘Ø āˆ£)(p : Term X) ā†’ (š‘Ø āŸ¦ p āŸ§) Ī· ā‰” (free-lift š‘Ø Ī·) p

free-lift-interp _ š‘Ø Ī· (ā„Š x) = ā‰”.refl
free-lift-interp wd š‘Ø Ī· (node f t) =
 wd (f Ģ‚ š‘Ø) (Ī» z ā†’ (š‘Ø āŸ¦ t z āŸ§) Ī·)
 ((free-lift š‘Ø Ī·) āˆ˜ t)((free-lift-interp wd š‘Ø Ī·) āˆ˜ t)

If the algebra in question happens to be š‘» X, then we expect that āˆ€ s we have (š‘» X)āŸ¦ p āŸ§ s ā‰” p s. But what is (š‘» X)āŸ¦ p āŸ§ s exactly? By definition, it depends on the form of p as follows:

  • if p = ā„Š x, then (š‘» X)āŸ¦ p āŸ§ s := (š‘» X)āŸ¦ ā„Š x āŸ§ s ā‰” s x

  • if p = node f t, then (š‘» X)āŸ¦ p āŸ§ s := (š‘» X)āŸ¦ node f t āŸ§ s = (f Ģ‚ š‘» X) Ī» i ā†’ (š‘» X)āŸ¦ t i āŸ§ s

Now, assume Ļ• : hom š‘» š‘Ø. Then by comm-hom-term, we have āˆ£ Ļ• āˆ£ (š‘» X)āŸ¦ p āŸ§ s = š‘Ø āŸ¦ p āŸ§ āˆ£ Ļ• āˆ£ āˆ˜ s.

  • if p = ā„Š x (and t : X ā†’ āˆ£ š‘» X āˆ£), then

āˆ£ Ļ• āˆ£ p ā‰” āˆ£ Ļ• āˆ£ (ā„Š x) ā‰” āˆ£ Ļ• āˆ£ (Ī» t ā†’ h t) ā‰” Ī» t ā†’ (āˆ£ Ļ• āˆ£ āˆ˜ t) x

  • if p = node f t, then

āˆ£ Ļ• āˆ£ p ā‰” āˆ£ Ļ• āˆ£ (š‘» X)āŸ¦ p āŸ§ s = (š‘» X)āŸ¦ node f t āŸ§ s = (f Ģ‚ š‘» X) Ī» i ā†’ (š‘» X)āŸ¦ t i āŸ§ s

We claim that for all p : Term X there exists q : Term X and t : X ā†’ āˆ£ š‘» X āˆ£ such that p ā‰” (š‘» X)āŸ¦ q āŸ§ t. We prove this fact as follows.


term-interp :  {X : Type Ļ‡} (f : āˆ£ š‘† āˆ£){s t : āˆ„ š‘† āˆ„ f ā†’ Term X}
 ā†’             s ā‰” t ā†’ node f s ā‰” (f Ģ‚ š‘» X) t

term-interp f {s}{t} st = ā‰”.cong (node f) st


term-interp' :  swelldef š“„ (ov Ļ‡) ā†’ {X : Type Ļ‡} (f : āˆ£ š‘† āˆ£){s t : āˆ„ š‘† āˆ„ f ā†’ Term X}
 ā†’              (āˆ€ i ā†’ s i ā‰” t i) ā†’ node f s ā‰” (f Ģ‚ š‘» X) t

term-interp' wd f {s}{t} st = wd (node f) s t st


term-gen :  swelldef š“„ (ov Ļ‡) ā†’ {X : Type Ļ‡}(p : āˆ£ š‘» X āˆ£)
 ā†’          Ī£[ q āˆˆ āˆ£ š‘» X āˆ£ ] p ā‰” (š‘» X āŸ¦ q āŸ§) ā„Š

term-gen _ (ā„Š x) = (ā„Š x) , ā‰”.refl
term-gen wd (node f t) =  (node f (Ī» i ā†’ āˆ£ term-gen wd (t i) āˆ£)) ,
                          term-interp' wd f Ī» i ā†’ āˆ„ term-gen wd (t i) āˆ„

term-gen-agreement :  (wd : swelldef š“„ (ov Ļ‡)){X : Type Ļ‡}(p : āˆ£ š‘» X āˆ£)
 ā†’                    (š‘» X āŸ¦ p āŸ§) ā„Š ā‰” (š‘» X āŸ¦ āˆ£ term-gen wd p āˆ£ āŸ§) ā„Š
term-gen-agreement _ (ā„Š x) = ā‰”.refl
term-gen-agreement wd {X} (node f t) = wd  ( f Ģ‚ š‘» X) (Ī» x ā†’ (š‘» X āŸ¦ t x āŸ§) ā„Š)
                                           (Ī» x ā†’ (š‘» X āŸ¦ āˆ£ term-gen wd (t x) āˆ£ āŸ§) ā„Š)
                                           Ī» i ā†’ term-gen-agreement wd (t i)

term-agreement : swelldef š“„ (ov Ļ‡) ā†’ {X : Type Ļ‡}(p : āˆ£ š‘» X āˆ£) ā†’ p ā‰”  (š‘» X āŸ¦ p āŸ§) ā„Š
term-agreement wd {X} p = āˆ„ term-gen wd p āˆ„ āˆ™ (term-gen-agreement wd p)ā»Ā¹

Interpretation of terms in product algebras


module _ (wd : swelldef š“„ (Ī² āŠ” Ī±)){X : Type Ļ‡ }{I : Type Ī²} where

 interp-prod :  (p : Term X)(š’œ : I ā†’ Algebra Ī±)(a : X ā†’ Ī [ i āˆˆ I ] āˆ£ š’œ i āˆ£)
  ā†’             (ā؅ š’œ āŸ¦ p āŸ§) a ā‰” Ī» i ā†’ (š’œ i āŸ¦ p āŸ§)(Ī» x ā†’ (a x) i)

 interp-prod (ā„Š _) š’œ a = ā‰”.refl
 interp-prod (node f t) š’œ a = wd ((f Ģ‚ ā؅ š’œ)) u v IH
  where
  u : āˆ€ x ā†’ āˆ£ ā؅ š’œ āˆ£
  u = Ī» x ā†’ (ā؅ š’œ āŸ¦ t x āŸ§) a
  v : āˆ€ x i ā†’ āˆ£ š’œ i āˆ£
  v = Ī» x i ā†’ (š’œ i āŸ¦ t x āŸ§)(Ī» j ā†’ a j i)
  IH : āˆ€ i ā†’ u i ā‰” v i
  IH = Ī» x ā†’ interp-prod (t x) š’œ a

 interp-prod2 :  funext (Ī± āŠ” Ī² āŠ” Ļ‡) (Ī± āŠ” Ī²) ā†’ (p : Term X)(š’œ : I ā†’ Algebra Ī±)
  ā†’              ā؅ š’œ āŸ¦ p āŸ§ ā‰” (Ī» a i ā†’ (š’œ i āŸ¦ p āŸ§) Ī» x ā†’ a x i)

 interp-prod2 _ (ā„Š xā‚) š’œ = ā‰”.refl
 interp-prod2 fe (node f t) š’œ = fe Ī» a ā†’ wd (f Ģ‚ ā؅ š’œ)(u a) (v a) (IH a)
  where
  u : āˆ€ a x ā†’ āˆ£ ā؅ š’œ āˆ£
  u a = Ī» x ā†’ (ā؅ š’œ āŸ¦ t x āŸ§) a
  v : āˆ€ (a : X ā†’ āˆ£ ā؅ š’œ āˆ£) ā†’ āˆ€ x i ā†’ āˆ£ š’œ i āˆ£
  v a = Ī» x i ā†’ (š’œ i āŸ¦ t x āŸ§)(Ī» z ā†’ (a z) i)
  IH : āˆ€ a x ā†’ (ā؅ š’œ āŸ¦ t x āŸ§) a ā‰” Ī» i ā†’ (š’œ i āŸ¦ t x āŸ§)(Ī» z ā†’ (a z) i)
  IH a = Ī» x ā†’ interp-prod (t x) š’œ a

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.


open ā‰”-Reasoning

comm-hom-term :  swelldef š“„ Ī² ā†’ {š‘Ø : Algebra Ī±} (š‘© : Algebra Ī²)
                 (h : hom š‘Ø š‘©){X : Type Ļ‡}(t : Term X)(a : X ā†’ āˆ£ š‘Ø āˆ£)
                 ------------------------------------------------------
  ā†’              āˆ£ h āˆ£ ((š‘Ø āŸ¦ t āŸ§) a) ā‰” (š‘© āŸ¦ t āŸ§) (āˆ£ h āˆ£ āˆ˜ a)

comm-hom-term _ š‘© h (ā„Š x) a = ā‰”.refl
comm-hom-term wd {š‘Ø} š‘© h (node f t) a =
 āˆ£ h āˆ£((f Ģ‚ š‘Ø) Ī» i ā†’  (š‘Ø āŸ¦ t i āŸ§) a)      ā‰”āŸØ i  āŸ©
 (f Ģ‚ š‘©)(Ī» i ā†’  āˆ£ h āˆ£ ((š‘Ø āŸ¦ t i āŸ§) a))   ā‰”āŸØ ii āŸ©
 (f Ģ‚ š‘©)(Ī» r ā†’ (š‘© āŸ¦ t r āŸ§) (āˆ£ h āˆ£ āˆ˜ a))  āˆŽ
 where i  = āˆ„ h āˆ„ f Ī» r ā†’ (š‘Ø āŸ¦ t r āŸ§) a
       ii = wd (f Ģ‚ š‘©)  ( Ī» iā‚ ā†’ āˆ£ h āˆ£ ((š‘Ø āŸ¦ t iā‚ āŸ§) a) )
                       ( Ī» r ā†’ (š‘© āŸ¦ t r āŸ§) (Ī» x ā†’ āˆ£ h āˆ£ (a x)) )
                       Ī» j ā†’ comm-hom-term wd š‘© h (t j) 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 _ {Ī± Ī² : Level}{X : Type Ī±} where

 open IsCongruence

 _āˆ£:_ : {š‘Ø : Algebra Ī±}(t : Term X)(Īø : Con{Ī±}{Ī²} š‘Ø) ā†’ (š‘Ø āŸ¦ t āŸ§) |: āˆ£ Īø āˆ£
 ((ā„Š x) āˆ£: Īø) p = p x
 ((node f t) āˆ£: Īø) p = (is-compatible āˆ„ Īø āˆ„) f Ī» x ā†’ ((t x) āˆ£: Īø) p

WARNING! The compatibility relation for terms āˆ£: is typed as |:, whereas the compatibility type for functions |: (defined in the Legacy.Base.Relations.Discrete module) is typed as |:.

Substitution

A substitution from Y to X is simply a function from Y to X, and the application of a substitution is represented as follows.


_[_] : {Ļ‡ : Level}{X Y : Type Ļ‡} ā†’ Term Y ā†’ (Y ā†’ X) ā†’ Term X
(ā„Š y) [ Ļƒ ] = ā„Š (Ļƒ y)
(node f t)  [ Ļƒ ] = node f Ī» i ā†’ t i [ Ļƒ ]

Alternatively, we may want a substitution that replaces each variable symbol in Y, not with an element of X, but with a term from Term X.


-- Substerm X Y, an inhabitant of which replaces each variable symbol in Y
-- with a term from Term X.
Substerm : (X Y : Type Ļ‡) ā†’ Type (ov Ļ‡)
Substerm X Y = (y : Y) ā†’ Term X

-- Application of a Substerm.
_[_]t : {X Y : Type Ļ‡ } ā†’ Term Y ā†’ Substerm X Y ā†’ Term X
(ā„Š y) [ Ļƒ ]t = Ļƒ y
(node f t) [ Ļƒ ]t = node f (Ī» z ā†’ (t z) [ Ļƒ ]t )

Next we prove the important Substitution Theorem which asserts that an identity p ā‰ˆ q holds in an algebra š‘Ø iff it holds in š‘Ø after applying any substitution.


subst-lemma :  swelldef š“„ Ī± ā†’ {X Y : Type Ļ‡ }(p : Term Y)(Ļƒ : Y ā†’ X)
               (š‘Ø : Algebra Ī±)(Ī· : X ā†’ āˆ£ š‘Ø āˆ£)
 ā†’             (š‘Ø āŸ¦ p [ Ļƒ ] āŸ§) Ī· ā‰” (š‘Ø āŸ¦ p āŸ§) (Ī· āˆ˜ Ļƒ)

subst-lemma _ (ā„Š x) Ļƒ š‘Ø Ī· = ā‰”.refl
subst-lemma wd (node f t) Ļƒ š‘Ø Ī· = wd (f Ģ‚ š‘Ø)  ( Ī» i ā†’ (š‘Ø āŸ¦ (t i) [ Ļƒ ] āŸ§) Ī· )
                                             ( Ī» i ā†’ (š‘Ø āŸ¦ t i āŸ§) (Ī· āˆ˜ Ļƒ) )
                                             Ī» i ā†’ subst-lemma wd (t i) Ļƒ š‘Ø Ī·

subst-theorem :  swelldef š“„ Ī± ā†’ {X Y : Type Ļ‡ }
                 (p q : Term Y)(Ļƒ : Y ā†’ X)(š‘Ø : Algebra Ī±)
 ā†’               š‘Ø āŸ¦ p āŸ§ ā‰ˆ š‘Ø āŸ¦ q āŸ§ ā†’ š‘Ø āŸ¦ p [ Ļƒ ] āŸ§ ā‰ˆ š‘Ø āŸ¦ q [ Ļƒ ] āŸ§

subst-theorem wd p q Ļƒ š‘Ø Apq Ī· =
 (š‘Ø āŸ¦ p [ Ļƒ ] āŸ§) Ī·  ā‰”āŸØ subst-lemma wd p Ļƒ š‘Ø Ī· āŸ©
 (š‘Ø āŸ¦ p āŸ§) (Ī· āˆ˜ Ļƒ)  ā‰”āŸØ Apq (Ī· āˆ˜ Ļƒ) āŸ©
 (š‘Ø āŸ¦ q āŸ§) (Ī· āˆ˜ Ļƒ)  ā‰”āŸØ ā‰”.sym (subst-lemma wd q Ļƒ š‘Ø Ī·) āŸ©
 (š‘Ø āŸ¦ q [ Ļƒ ] āŸ§) Ī·  āˆŽ