Skip to content

Setoid.Terms.Operations

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 --cubical-compatible --exact-split --safe #-}

module Setoid.Terms.Operations where

-- Imports from Agda and the Agda Standard Library ---------------------
open import Agda.Primitive    using ()  renaming ( Set to Type )
open import Data.Product      using ( _,_ ; proj₁ ; projβ‚‚ )
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  ( OperationSymbolsOf ; ArityOf
                                             ; π“ž ; π“₯ ; Signature ; 𝑆 )
open  import Overture.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 ( to 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 )
  open Setoid 𝔻[ 𝑨 ]   using ( _β‰ˆ_ ; refl )
  open Environment 𝑨   using ( ⟦_⟧ )

  free-lift-interp :  (Ξ· : X β†’ π•Œ[ 𝑨 ])(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 _ {𝑆 : Signature π“ž π“₯}{X : Type Ο‡} where
  open Algebra (𝑻 {𝑆 = 𝑆} X)      using ( Interp ) renaming (Domain to TX )
  open Setoid TX          using ( _β‰ˆ_ ; refl )
  open Environment (𝑻 {𝑆 = 𝑆} X)  using ( ⟦_⟧ ; ≐→Equal )
  open SetoidReasoning TX

  term-interp :  (f : OperationSymbolsOf 𝑆){s t : ArityOf 𝑆 f β†’ Term {𝑆 = 𝑆} X} β†’ (βˆ€ i β†’ s i ≐ t i)
   β†’ βˆ€ Ξ· β†’ ⟦ node f s ⟧ ⟨$⟩ Ξ· β‰ˆ ⟦ node f 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

interp-prod says that interpreting a term in a product is the same as interpreting it in each factor and collecting the results: for every term p and every environment ρ, the value of p in β¨… π’œ under ρ agrees, at each coordinate i, with the value of p in π’œ i under the i-th component of ρ.

This is the term-level counterpart of the way β¨… of Setoid.Algebras.Products interprets operation symbols in the first place, and the proof is the induction that says so: the variable case is reflexivity, and the operation case pushes the induction hypothesis through the product's Interp.

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 the most important fact about term operations (comm-hom-term): every term commutes with every homomorphism.

module _
  {𝑆 : Signature π“ž π“₯}
  {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}
  {𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ}
  ((h , hhom) : hom 𝑨 𝑩)
  where

  open Algebra 𝑩       using (Interp)
  open Setoid 𝔻[ 𝑩 ]  using ( _β‰ˆ_ ; refl )
  open Environment 𝑨   using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
  open Environment 𝑩   using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
  open SetoidReasoning 𝔻[ 𝑩 ]
  open IsHom

  comm-hom-term : (t : Term {𝑆 = 𝑆} X) (a : X β†’ π•Œ[ 𝑨 ])
    β†’ h ⟨$⟩ (⟦ t βŸ§β‚ ⟨$⟩ a) β‰ˆ ⟦ t βŸ§β‚‚ ⟨$⟩ Ξ» i β†’ h ⟨$⟩ a i

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

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 : {𝑆 : Signature π“ž π“₯}(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