↑ 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 Base.Algebras.Basic using ( π“ž ; π“₯ ; Signature )

module Setoid.Terms.Operations {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library ---------------------
open import Agda.Primitive    using ( Level )  renaming ( Set to Type )
open import Data.Product      using ( _,_ )
open import Function.Base     using ( _∘_ )
open import Function.Bundles  using ()         renaming ( Func to _⟢_ )
open import Relation.Binary   using ( Setoid )
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Binary.PropositionalEquality as ≑ using ( _≑_ )

-- Imports from Agda Universal Algebra Library ----------------------------------------------
open import Base.Overture.Preliminaries          using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Base.Terms.Basic            {𝑆 = 𝑆}  using ( Term )

open import Setoid.Algebras.Basic       {𝑆 = 𝑆}  using ( Algebra ; _Μ‚_ ; ov )
open import Setoid.Algebras.Products    {𝑆 = 𝑆}  using ( β¨… )
open import Setoid.Homomorphisms.Basic  {𝑆 = 𝑆}  using ( hom ; IsHom )
open import Setoid.Terms.Basic          {𝑆 = 𝑆}  using ( module Environment ; 𝑻 ; _≐_ ; ≐-isRefl )
open import Setoid.Terms.Properties     {𝑆 = 𝑆}  using ( free-lift )

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 SetoidReasoning B

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

 open Environment 𝑨 using ( ) renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
 open Environment 𝑩 using ( ) renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
 open IsHom
 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.

_[_] : {Ο‡ : 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 )


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