Setoid.Terms.Basic¶
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.
_≐_ is the inductive equality of terms,
TermSetoid bundles it, and 𝑻 is the resulting
term algebra, whose operations are the term constructors themselves and so are
trivially compatible with _≐_.
The rest is the machinery of interpretation.
Suband_[_]are substitutions and their action on terms;Envis the setoid of environments, that is, assignments of elements of an algebra to variables;⟦_⟧is the value of a term in an environment, as a setoid function so that it respects equality of environments;EqualwithisEquivis the resulting notion of two terms having the same value in a given algebra under every environment.
The substitution 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.
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
whose carrier is the setoid of terms.
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.
A substitution from Δ to Γ associates a term in Γ with each variable in Δ.
-- 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.
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.
⟦_⟧ : {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) σ ρ)