↑ Top

Basic definitions

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


{-# OPTIONS --without-K --exact-split --safe #-}

open import Overture using (π“ž ; π“₯ ; Signature)

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

-- imports from Agda and the Agda Standard Library -------------------------------
open import Agda.Primitive         using () renaming ( Set to Type )
open import Data.Empty.Polymorphic using ( βŠ₯ )
open import Data.Product           using ( _,_ )
open import Data.Sum               using ( _⊎_ )
                                   renaming ( inj₁ to inl ; injβ‚‚ to inr )
open import Function               using ( Func )
open import Level                  using ( Level ; Lift ; _βŠ”_ )
open import Relation.Binary        using ( Setoid ; IsEquivalence )
                                   using ( Reflexive ; Symmetric ; Transitive )

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

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Overture using ( βˆ₯_βˆ₯ )
open import Setoid.Algebras  {𝑆 = 𝑆}  using ( Algebra ; ov ; _Μ‚_)
open import Base.Terms       {𝑆 = 𝑆}  using ( Term )

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

private variable
 Ο‡ Ξ± β„“ : Level
 X Y : Type Ο‡
Equality of terms

We take a different approach here, using 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 whose carrier is the setoid of terms.


module _ {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}{s t : βˆ₯ 𝑆 βˆ₯ f β†’ Term X} β†’ (βˆ€ i β†’ (s i) ≐ (t i)) β†’ (node f s) ≐ (node f t)

 -- Equality of terms is an equivalence relation
 open Level
 ≐-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 : (X : Type Ο‡) β†’ Setoid (ov Ο‡) (ov Ο‡)
TermSetoid X = record { Carrier = Term X ; _β‰ˆ_ = _≐_ ; isEquivalence = ≐-isEquiv }

open Algebra

-- The Term Algebra
𝑻 : (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.

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


-- Parallel substitutions.
Sub : 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 [ Οƒ ])

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


module Environment (𝑨 : Algebra Ξ± β„“) where
 open Algebra 𝑨  renaming( Domain to A ; Interp  to InterpA )  using()
 open Setoid A   renaming( _β‰ˆ_ to _β‰ˆβ‚_ ; Carrier to ∣A∣ )      using( refl ; sym ; trans )

 Env : Type Ο‡ β†’ Setoid _ _
 Env X = record  { Carrier = X β†’ ∣A∣
                 ; _β‰ˆ_ = Ξ» ρ ρ' β†’ (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.


 ⟦_⟧ : {X : Type Ο‡}(t : Term X) β†’ Func (Env X) A
 ⟦ β„Š 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 () renaming ( Carrier to ∣_∣ )

 -- 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 = βˆ€ (ρ : ∣ 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 = Ξ“})
 IsEquivalence.refl   isEquiv = Ξ» _ β†’ refl
 IsEquivalence.sym    isEquiv = Ξ» x=y ρ β†’ sym (x=y ρ)
 IsEquivalence.trans  isEquiv = Ξ» ij jk ρ β†’ trans (ij ρ) (jk ρ)

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

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

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

↑ Setoid.Terms Setoid.Terms.Properties β†’