---
layout: default
title : "Setoid.Terms.Basic module (The Agda Universal Algebra Library)"
date : "2021-09-18"
author: "agda-algebras development team"
---

### Basic definitions

This is the [Setoid.Terms.Basic][] module of the [Agda Universal Algebra Library][].

Terms themselves are inherited from [Overture.Terms][]; what this module adds is
everything needed to treat them *as a setoid algebra*.

`_≐_`{.AgdaDatatype} is the inductive equality of terms,
`TermSetoid`{.AgdaFunction} bundles it, and `𝑻`{.AgdaFunction} is the resulting
**term algebra**, whose operations are the term constructors themselves and so are
trivially compatible with `_≐_`{.AgdaDatatype}.

The rest is the machinery of interpretation.

+  `Sub`{.AgdaFunction} and `_[_]`{.AgdaFunction} are substitutions and their
   action on terms;
+  `Env`{.AgdaFunction} is the setoid of environments, that is, assignments of
   elements of an algebra to variables;
+  `⟦_⟧`{.AgdaFunction} is the value of a term in an environment, as a setoid
   function so that it respects equality of environments;
+  `Equal`{.AgdaFunction} with `isEquiv`{.AgdaFunction} is the resulting notion of
   two terms having the same value in a given algebra under every environment.

The `substitution`{.AgdaFunction} lemma, that interpreting a substituted term is
interpreting the original under a reinterpreted environment, is the workhorse of
the soundness proof in [Setoid.Varieties.SoundAndComplete][].

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Terms.Basic 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               using ( Func )
open import Level                  using ( Level ; _βŠ”_ )
open import Relation.Binary        using ( Setoid ; IsEquivalence )
                                   using ( Reflexive ; Symmetric ; Transitive )

open import Relation.Binary.PropositionalEquality using ( _≑_ ; refl ; sym ; trans )

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Overture         using ( π“ž ; π“₯ ; Signature ; 𝑆
                                   ; ArityOf ; OperationSymbolsOf )
open import Setoid.Algebras  using ( Algebra ; ov ; _^_ ; 𝔻[_] ; π•Œ[_] )
open import Overture.Terms   using ( Term )

open Func renaming ( to to _⟨$⟩_ )
open Term

private variable
  Ο‡ Ξ± β„“ : Level
  X Y : Type Ο‡
```
-->

#### Equality of terms

The approach we take to equality of terms uses setoids instead of quotient types.
That is, we will define the collection of terms in a signature as a setoid with a
particular equality-of-terms relation, which we must define.  Ultimately we will
use this to define the (absolutely free) term algebra as a `Algebra`{.AgdaRecord}
whose carrier is the setoid of terms.

```agda
module _ {𝑆 : Signature π“ž π“₯}{X : Type Ο‡ } where

  -- Equality of terms as an inductive datatype
  data _≐_ : Term {𝑆 = 𝑆} X β†’ Term {𝑆 = 𝑆} X β†’ Type (ov {𝑆 = 𝑆} Ο‡) where
    rfl :  {x y : X} β†’ x ≑ y β†’ β„Š x ≐ β„Š y
    gnl :  {f : OperationSymbolsOf 𝑆}{s t : ArityOf 𝑆 f β†’ Term {𝑆 = 𝑆} X}
           β†’ (βˆ€ i β†’ s i ≐ t i) β†’ node f s ≐ node f t

  infix 4 _≐_

  -- Equality of terms is an equivalence relation
  ≐-isRefl : Reflexive _≐_
  ≐-isRefl {β„Š _} = rfl refl
  ≐-isRefl {node _ _} = gnl Ξ» _ β†’ ≐-isRefl

  ≐-isSym : Symmetric _≐_
  ≐-isSym (rfl x) = rfl (sym x)
  ≐-isSym (gnl x) = gnl Ξ» i β†’ ≐-isSym (x i)

  ≐-isTrans : Transitive _≐_
  ≐-isTrans (rfl x) (rfl y) = rfl (trans x y)
  ≐-isTrans (gnl x) (gnl y) = gnl Ξ» i β†’ ≐-isTrans (x i) (y i)

  ≐-isEquiv : IsEquivalence _≐_
  ≐-isEquiv = record { refl = ≐-isRefl ; sym = ≐-isSym ; trans = ≐-isTrans }

TermSetoid : {𝑆 : Signature π“ž π“₯}(X : Type Ο‡) β†’ Setoid (ov {𝑆 = 𝑆} Ο‡) (ov {𝑆 = 𝑆} Ο‡)
TermSetoid {𝑆 = 𝑆} X = record { Carrier = Term {𝑆 = 𝑆} X ; _β‰ˆ_ = _≐_ ; isEquivalence = ≐-isEquiv }

open Algebra

-- The Term Algebra
𝑻 : {𝑆 : Signature π“ž π“₯}(X : Type Ο‡) β†’ Algebra {𝑆 = 𝑆} (ov {𝑆 = 𝑆} Ο‡) (ov {𝑆 = 𝑆} Ο‡)
Domain (𝑻 {𝑆 = 𝑆} X) = TermSetoid {𝑆 = 𝑆} X
Interp (𝑻 X) ⟨$⟩ (f , ts) = node f ts
cong (Interp (𝑻 X)) (refl , ss≐ts) = gnl ss≐ts
```

#### Interpretation of terms in setoid algebras

The approach to terms and their interpretation in this module was inspired by
[Andreas Abel's formal proof of Birkhoff's completeness theorem](http://www.cse.chalmers.se/~abela/agda/MultiSortedAlgebra.pdf).

A substitution from `Ξ”` to `Ξ“` associates a term in `Ξ“` with each variable in `Ξ”`.

```agda
-- Parallel substitutions.
Sub : {𝑆 : Signature π“ž π“₯} β†’ Type Ο‡ β†’ Type Ο‡ β†’ Type (ov {𝑆 = 𝑆} Ο‡)
Sub {𝑆 = 𝑆} X Y = (y : Y) β†’ Term {𝑆 = 𝑆} X

-- Application of a substitution.
_[_] : (t : Term {𝑆 = 𝑆} Y) (Οƒ : Sub {𝑆 = 𝑆} X Y) β†’ Term {𝑆 = 𝑆} X
(β„Š x) [ Οƒ ] = Οƒ x
(node f ts) [ Οƒ ] = node f (Ξ» i β†’ ts i [ Οƒ ])

infix 30 _[_]
```

An environment for `Ξ“` maps each variable `x : Ξ“` to an element of `A`, and equality
of environments is defined pointwise.

```agda
module Environment {𝑆 : Signature π“ž π“₯}(𝑨 : Algebra {𝑆 = 𝑆} Ξ± β„“) where
  open Algebra 𝑨 using() renaming(Interp  to InterpA )
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )
    renaming  ( refl to β‰ˆrefl ; sym to β‰ˆsym ; trans to β‰ˆtrans)

  Env : Type Ο‡ β†’ Setoid _ _
  Env X = record  { Carrier = X β†’ π•Œ[ 𝑨 ]
                  ; _β‰ˆ_ = Ξ» ρ ρ' β†’ (x : X) β†’ ρ x β‰ˆ ρ' x
                  ; isEquivalence = record  { refl = Ξ» _ β†’ β‰ˆrefl
                                            ; sym = Ξ» h x β†’ β‰ˆsym (h x)
                                            ; trans = Ξ» g h x β†’ β‰ˆtrans (g x) (h x)
                                            }
                  }

  open Algebra using ( Domain ; Interp )

  EnvAlgebra : Type Ο‡ β†’ Algebra {𝑆 = 𝑆} (Ξ± βŠ” Ο‡) (β„“ βŠ” Ο‡)
  Domain (EnvAlgebra X) = Env X
  Interp (EnvAlgebra X) ⟨$⟩ (f , aΟ•) = Ξ» x β†’ (f ^ 𝑨) Ξ» i β†’ aΟ• i x
  cong (Interp (EnvAlgebra X)) {f , a} {.f , b} (refl , aibi) x = cong InterpA (refl , Ξ» i β†’ aibi i x)
```

Interpretation of terms is iteration on the W-type.  The standard library offers
`iter' (on sets), but we need this to be a setoid function.

```agda
  ⟦_⟧ : {X : Type Ο‡}(t : Term {𝑆 = 𝑆} X) β†’ Func (Env X) 𝔻[ 𝑨 ]
  ⟦ β„Š x ⟧          ⟨$⟩ ρ = ρ x
  ⟦ node f args ⟧  ⟨$⟩ ρ = InterpA ⟨$⟩ (f , Ξ» i β†’ ⟦ args i ⟧ ⟨$⟩ ρ)
  cong ⟦ β„Š x ⟧          uβ‰ˆv = uβ‰ˆv x
  cong ⟦ node f args ⟧  xβ‰ˆy = cong InterpA (refl , Ξ» i β†’ cong ⟦ args i ⟧ xβ‰ˆy )

  open Setoid using ( Carrier )

  -- An equality between two terms holds in a model if the two terms
  -- are equal under all valuations of their free variables.
  Equal : βˆ€ {X : Type Ο‡} (s t : Term {𝑆 = 𝑆} X) β†’ Type _
  Equal {X = X} s t = βˆ€ (ρ : Carrier (Env X)) β†’ ⟦ s ⟧ ⟨$⟩ ρ β‰ˆ ⟦ t ⟧ ⟨$⟩ ρ

  ≐→Equal : {X : Type Ο‡}(s t : Term {𝑆 = 𝑆} X) β†’ s ≐ t β†’ Equal s t
  ≐→Equal .(β„Š _) .(β„Š _) (rfl refl) = Ξ» _ β†’ β‰ˆrefl
  ≐→Equal (node _ s) (node _ t) (gnl x) =
    Ξ» ρ β†’ cong InterpA (refl , Ξ» i β†’ ≐→Equal (s i) (t i) (x i) ρ)

  -- Equal is an equivalence relation.
  isEquiv : {Ξ“ : Type Ο‡} β†’ IsEquivalence (Equal {X = Ξ“})
  isEquiv .IsEquivalence.refl = Ξ» _ β†’ β‰ˆrefl
  isEquiv .IsEquivalence.sym = Ξ» x=y ρ β†’ β‰ˆsym (x=y ρ)
  isEquiv .IsEquivalence.trans = Ξ» ij jk ρ β†’ β‰ˆtrans (ij ρ) (jk ρ)

  -- Evaluation of a substitution gives an environment.
  ⟦_⟧s : {X Y : Type Ο‡} β†’ Sub {𝑆 = 𝑆} X Y β†’ Carrier (Env X) β†’ Carrier (Env Y)
  ⟦ Οƒ ⟧s ρ x = ⟦ Οƒ x ⟧ ⟨$⟩ ρ

  -- Substitution lemma: ⟦t[Οƒ]⟧ρ ≃ ⟦tβŸ§βŸ¦ΟƒβŸ§Ο
  substitution :  {X Y : Type Ο‡} β†’ (t : Term {𝑆 = 𝑆} Y) (Οƒ : Sub {𝑆 = 𝑆} X Y) (ρ : Carrier (Env X))
    β†’ ⟦ t [ Οƒ ] ⟧ ⟨$⟩ ρ  β‰ˆ  ⟦ t ⟧ ⟨$⟩ (⟦ Οƒ ⟧s ρ)

  substitution (β„Š x) Οƒ ρ = β‰ˆrefl
  substitution (node f ts) Οƒ ρ = cong InterpA (refl , Ξ» i β†’ substitution (ts i) Οƒ ρ)
```