↑ Top

Term Operations for Setoid Algebras

This section presents the Setoid.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 Overture using (π“ž ; π“₯ ; Signature)

module Setoid.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 ( _,_ )
open import Function.Base     using ( _∘_ )
open import Function.Bundles  using ()         renaming ( Func to _⟢_ )
open import Level             using ( Level )
open import Relation.Binary   using ( Setoid )

open import Relation.Binary.PropositionalEquality as ≑ using ( _≑_ )

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from Agda Universal Algebra Library -----------------------------------
open  import Overture                         using ( ∣_∣ ; βˆ₯_βˆ₯ )
open  import Base.Terms               {𝑆 = 𝑆} using ( Term )
open  import Setoid.Algebras          {𝑆 = 𝑆} using ( Algebra ; _Μ‚_ ; ov ; β¨… )
open  import Setoid.Homomorphisms     {𝑆 = 𝑆} using ( hom ; IsHom )
open  import Setoid.Terms.Properties  {𝑆 = 𝑆} using ( free-lift )
open  import Setoid.Terms.Basic       {𝑆 = 𝑆}
      using ( module Environment ; 𝑻 ; _≐_ ; ≐-isRefl )

open Term
open _⟢_ using ( cong ) renaming ( f to _⟨$⟩_ )

private variable
 Ξ± ρᡃ Ξ² ρᡇ ρ Ο‡ ΞΉ : Level
 X : Type Ο‡

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


module _ {𝑨 : Algebra Ξ± ρᡃ} where
 open Algebra 𝑨      using ( Interp )      renaming (Domain to A )
 open Setoid A       using ( _β‰ˆ_ ; refl )  renaming ( Carrier to ∣A∣ )
 open Environment 𝑨  using ( ⟦_⟧ )

 free-lift-interp :  (Ξ· : X β†’ ∣A∣)(p : Term X)
  β†’                  ⟦ p ⟧ ⟨$⟩ Ξ· β‰ˆ (free-lift{𝑨 = 𝑨} Ξ·) p

 free-lift-interp Ξ· (β„Š x) = refl
 free-lift-interp Ξ· (node f t) = cong Interp (≑.refl , (free-lift-interp Ξ·) ∘ t)

module _ {X : Type Ο‡} where
 open Algebra (𝑻 X)      using ( Interp )      renaming (Domain to TX )
 open Setoid TX          using ( _β‰ˆ_ ; refl )  renaming ( Carrier to ∣TX∣ )
 open Environment (𝑻 X)  using ( ⟦_⟧ ; ≐→Equal )
 open SetoidReasoning TX

 term-interp :  (f : ∣ 𝑆 ∣){s t : βˆ₯ 𝑆 βˆ₯ f β†’ Term X} β†’ (βˆ€ i β†’ s i ≐ t i)
  β†’             βˆ€ Ξ· β†’ ⟦ node f s ⟧ ⟨$⟩ Ξ· β‰ˆ ⟦ node f t ⟧ ⟨$⟩ Ξ· -- (f Μ‚ 𝑻 X) t

 term-interp f {s}{t} st Ξ· = cong Interp (≑.refl , Ξ» i β†’ ≐→Equal (s i) (t i) (st i) Ξ· )

 term-agreement : (p : Term X) β†’ p β‰ˆ ⟦ p ⟧ ⟨$⟩ β„Š
 term-agreement (β„Š x) = refl
 term-agreement (node f t) = cong Interp (≑.refl , (Ξ» i β†’ term-agreement (t i)))

Interpretation of terms in product algebras


module _ {X : Type Ο‡ }{I : Type ΞΉ}(π’œ : I β†’ Algebra Ξ± ρᡃ) where
 open Algebra (β¨… π’œ)      using (Interp)  renaming ( Domain to β¨…A )
 open Setoid β¨…A          using ( _β‰ˆ_ ; refl )
 open Environment (β¨… π’œ)  using ()        renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
 open Environment        using ( ⟦_⟧ ; ≐→Equal )

 interp-prod :  (p : Term X)
  β†’             βˆ€ ρ β†’ ⟦ p βŸ§β‚ ⟨$⟩ ρ β‰ˆ (Ξ» i β†’ (⟦ π’œ i ⟧ p) ⟨$⟩ (Ξ» x β†’ (ρ x) i))

 interp-prod (β„Š x) = Ξ» ρ i β†’ ≐→Equal (π’œ i) (β„Š x) (β„Š x) ≐-isRefl Ξ» x' β†’ (ρ x) i
 interp-prod (node f t) = Ξ» ρ i β†’ cong Interp (≑.refl , (Ξ» j k β†’ interp-prod (t j) ρ k)) 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 _ {𝑨 : Algebra Ξ± ρᡃ}{𝑩 : Algebra Ξ² ρᡇ}(hh : hom 𝑨 𝑩) where
 open Algebra 𝑨      using () renaming (Domain to A ; Interp to Interp₁ )
 open Setoid A       using () renaming ( _β‰ˆ_ to _β‰ˆβ‚_ ; Carrier to ∣A∣ )
 open Algebra 𝑩      using () renaming (Domain to B ; Interp to Interpβ‚‚ )
 open Setoid B       using ( _β‰ˆ_ ; sym ; refl )
 open Environment 𝑨  using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
 open Environment 𝑩  using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
 open SetoidReasoning B
 open IsHom

 private
  hfunc = ∣ hh ∣
  h = _⟨$⟩_ hfunc

 comm-hom-term :  (t : Term X) (a : X β†’ ∣A∣)
  β†’               h (⟦ t βŸ§β‚ ⟨$⟩ a) β‰ˆ ⟦ t βŸ§β‚‚ ⟨$⟩ (h ∘ a)

 comm-hom-term (β„Š x) a = refl
 comm-hom-term (node f t) a = goal
  where
  goal : h (⟦ node f t βŸ§β‚ ⟨$⟩ a) β‰ˆ (⟦ node f t βŸ§β‚‚ ⟨$⟩ (h ∘ a))
  goal = begin
   h (⟦ node f t βŸ§β‚ ⟨$⟩ a)             β‰ˆβŸ¨ (compatible βˆ₯ hh βˆ₯) ⟩
   (f Μ‚ 𝑩)(Ξ» i β†’ h (⟦ t i βŸ§β‚ ⟨$⟩ a))    β‰ˆβŸ¨ cong Interpβ‚‚ (≑.refl , Ξ» i β†’ comm-hom-term (t i) a) ⟩
   (f Μ‚ 𝑩)(Ξ» i β†’ ⟦ t i βŸ§β‚‚ ⟨$⟩ (h ∘ a))  β‰ˆβŸ¨ refl ⟩
   (⟦ node f t βŸ§β‚‚ ⟨$⟩ (h ∘ a))         ∎

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.


_[_]s : {Ο‡ : Level}{X Y : Type Ο‡} β†’ Term Y β†’ (Y β†’ X) β†’ Term X
(β„Š y) [ Οƒ ]s = β„Š (Οƒ y)
(node f t)  [ Οƒ ]s = node f Ξ» i β†’ t i [ Οƒ ]s

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 )

← Setoid.Terms.Properties Setoid.Subalgebras β†’