Skip to content

Setoid.Varieties.Interpretation

Theory interpretations and the interpretability quasi-order

This is the Setoid.Varieties.Interpretation module of the Agda Universal Algebra Library.

This module is to a theory interpretation what Setoid.Varieties.Invariance is to a signature morphism. Where the latter packages a SigMorphism as a reduct with respect to which satisfaction is an invariant, here we package an interpretation (Overture.Terms.Interpretation) as a reductα΄΅ and prove the generalized satisfaction condition; we then use it to define the interpretability quasi-order on equational theories and to record its reflexivity and transitivity.

The interpretation reduct

For an interpretation I : 𝑆₁ β†’ 𝑆₂ and an 𝑆₂-algebra 𝑩, the interpretation reduct reductα΄΅ I 𝑩 is the 𝑆₁-algebra on the same carrier in which each operation symbol o of 𝑆₁ is interpreted by the derived operation I o β€” that is, by evaluating the 𝑆₂-term I o in 𝑩, reading the arguments as the values of the argument positions of o.

When I = ⟨ Ο† ⟩ᴡ comes from a signature morphism, reductα΄΅ I 𝑩 is the ordinary reduct Ο† 𝑩 (reductα΄΅-⟨⟩ below, by refl), so this is the term-valued generalization of reduct.

The satisfaction condition

The pay-off is the generalized satisfaction condition: for 𝑆₁-terms s , t,

reductα΄΅ I 𝑩 ⊧ s β‰ˆ t   if and only if   𝑩 ⊧ (I ✦ s) β‰ˆ (I ✦ t).

To check an 𝑆₁-equation against the derived view of 𝑩 is to check the interpreted equation against 𝑩 itself. It is the shadow of one commuting triangle of interpretation maps β€” naturality of the fold along the interpretation β€” exactly as in Setoid.Varieties.Invariance, only now the node step grafts a derived term rather than relabelling a symbol, and the proof leans on the heterogeneous evaluation lemma graft-eval (evaluation commutes with graft) in place of the definitional reduct step. (As there, no clause matches a concrete Fin n, so the without-K unifier is never asked to invert anything.)

The quasi-order

An equational theory ℰ₁ of 𝑆₁ is interpretable in a theory β„°β‚‚ of 𝑆₂, written ℰ₁ β‰Ό β„°β‚‚, when some interpretation carries every model of β„°β‚‚ (via its reduct) to a model of ℰ₁. By the satisfaction condition this is the same as asking that every ℰ₁-equation, interpreted, be a consequence of β„°β‚‚.

This is the universal algebraist's notion of one variety interpreting another, whose order-reflection is the Garcia–Taylor lattice of interpretability types.1

Reflexivity is the identity interpretation and transitivity is composition _∘ᴡ_; the proofs are short because ✦-id and ✦-∘ (Setoid.Terms.Interpretation) already did the work, fed through the satisfaction condition.

This connects forward to planned formalizing work related to the Bodirsky–Pinsker program, where interpretability between (infinite-domain) clones is the governing relation.2

A worked Maltsev-term instance is in Classical.Interpretations.Maltsev.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Varieties.Interpretation where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive                 using () renaming ( Set to Type )
open import Data.Product                   using ( _,_ ; _Γ—_ ; Ξ£-syntax ; proj₁ ; projβ‚‚ )
open import Function                       using ( Func )
open import Level                          using ( Level )
open import Relation.Binary                using ( Setoid )

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

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Signatures            using  ( π“ž ; π“₯ ; Signature
                                                  ; OperationSymbolsOf )
open import Overture.Signatures.Morphisms  using  ( SigMorphism )
open import Overture.Terms                 using  ( Term ; β„Š ; node )
open import Overture.Terms.Interpretation  using  ( Interpretation ; graft ; _✦_
                                                  ; idᴡ ; _∘ᴡ_ ; ⟨_⟩ᴡ )
open import Setoid.Algebras.Basic          using  ( Algebra ; _^_ ; 𝔻[_] ; π•Œ[_] )
open import Setoid.Algebras.Reduct         using  ( reduct )
open import Setoid.Terms.Basic             using  ( _≐_ ; ≐-isSym ; module Environment )
open import Setoid.Terms.Interpretation    using  ( ✦-id ; ✦-∘ )

import Setoid.Varieties.EquationalLogic as EqLogic

open Func using ( cong ) renaming ( to to _⟨$⟩_ )

private variable
  Ξ± ρ Ο‡ ΞΉ : Level
  X : Type Ο‡
  𝑆 𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯
  χ₁ Ο‡β‚‚ χ₃ ι₁ ΞΉβ‚‚ ι₃ : Level

Two single-algebra lemmas

Everything in this block fixes one algebra 𝑨. First, satisfaction respects the term equality _≐_ on both sides. (This is the convenience lemma we anticipated consumers would want; the interpretability proofs are that consumer.)

module _ {𝑆 : Signature π“ž π“₯} (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) where
  open Environment 𝑨 using ( ⟦_⟧ ; ≐→Equal )
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ ) renaming ( refl to β‰ˆrefl ; sym to β‰ˆsym ; trans to β‰ˆtrans )
  open EqLogic using ( _⊧_β‰ˆ_ )

  ⊧-≐ : {s sβ€² t tβ€² : Term {𝑆 = 𝑆} X}
    β†’ s ≐ sβ€² β†’ t ≐ tβ€² β†’ 𝑨 ⊧ s β‰ˆ t β†’ 𝑨 ⊧ sβ€² β‰ˆ tβ€²
  ⊧-≐ {s = s} {sβ€²} {t} {tβ€²} s≐sβ€² t≐tβ€² A⊧ Ξ· =
    β‰ˆtrans (β‰ˆsym (≐→Equal s sβ€² s≐sβ€² Ξ·)) (β‰ˆtrans (A⊧ Ξ·) (≐→Equal t tβ€² t≐tβ€² Ξ·))

Second, term evaluation commutes with graft: evaluating a grafted term is evaluating the host term in the environment that first evaluates each grafted subtree. This is the heterogeneous-level analogue of the substitution lemma of Setoid.Terms.Basic, and it is the node step of the interpretation triangle below.

  graft-eval : {ΞΎ : Level} {U : Type ΞΎ}
    (u : Term {𝑆 = 𝑆} U) (Οƒ : U β†’ Term {𝑆 = 𝑆} X) (Ξ· : X β†’ π•Œ[ 𝑨 ])
    β†’ ⟦ graft u Οƒ ⟧ ⟨$⟩ Ξ· β‰ˆ ⟦ u ⟧ ⟨$⟩ (Ξ» y β†’ ⟦ Οƒ y ⟧ ⟨$⟩ Ξ·)
  graft-eval (β„Š y)       Οƒ Ξ· = β‰ˆrefl
  graft-eval (node f us) Οƒ Ξ· = cong (Algebra.Interp 𝑨) (refl , Ξ» i β†’ graft-eval (us i) Οƒ Ξ·)

The interpretation reduct and the satisfaction condition

Now fix an interpretation I and an 𝑆₂-algebra 𝑩. The reduct keeps the carrier and interprets each 𝑆₁-symbol o by evaluating I o (a derived operation), so its cong is the congruence of that evaluation.

module _
  {𝑆₁ 𝑆₂ : Signature π“ž π“₯}
  (𝑩 : Algebra {𝑆 = 𝑆₂} Ξ± ρ)
  where
  module _
    (I : Interpretation 𝑆₁ 𝑆₂)
    where
    private module EnvB = Environment 𝑩
    open EnvB using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
    open Algebra using (Domain ; Interp)

    reductα΄΅ : Algebra {𝑆 = 𝑆₁} Ξ± ρ
    reductα΄΅ .Domain = 𝔻[ 𝑩 ]
    reductα΄΅ .Interp ⟨$⟩ (o , args) = ⟦ I o βŸ§β‚‚ ⟨$⟩ args
    reductα΄΅ .Interp .cong {o , u} {.o , v} (refl , uβ‰ˆv) = cong ⟦ I o βŸ§β‚‚ uβ‰ˆv

    open Environment {𝑆 = 𝑆₁} reductα΄΅ using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
    open Setoid 𝔻[ 𝑩 ] using ( _β‰ˆ_ ) renaming ( refl to β‰ˆrefl ; sym to β‰ˆsym ; trans to β‰ˆtrans )
    open EqLogic using () renaming ( _⊧_β‰ˆ_ to _βŠ§β‚_β‰ˆ_ )
    open EqLogic using () renaming ( _⊧_β‰ˆ_ to _βŠ§β‚‚_β‰ˆ_ )

The interpretation triangle: evaluating an 𝑆₁-term in the reduct equals evaluating its interpretation in 𝑩. At a leaf both sides look up the variable. At a node, the reduct's interpretation is "evaluate the derived term I f", and the translation's node clause grafts the interpreted subterms into I f; graft-eval says those agree, and the inductive hypotheses match the arguments through cong.

    reductα΄΅-interp : (t : Term {𝑆 = 𝑆₁} X) (Ξ· : X β†’ π•Œ[ 𝑩 ]) β†’ ⟦ t βŸ§β‚ ⟨$⟩ Ξ· β‰ˆ ⟦ I ✦ t βŸ§β‚‚ ⟨$⟩ Ξ·
    reductα΄΅-interp (β„Š x) Ξ· = β‰ˆrefl
    reductα΄΅-interp (node f ts) Ξ· =
      β‰ˆtrans  (cong ⟦ I f βŸ§β‚‚ (Ξ» i β†’ reductα΄΅-interp (ts i) Ξ·))
              (β‰ˆsym (graft-eval 𝑩 (I f) (Ξ» i β†’ I ✦ ts i) Ξ·))

Satisfaction is the triangle quantified over environments, so each direction is a trans-sandwich around the given satisfaction proof β€” verbatim the shape of ⊧-reduct / ⊧-expand. The equation sides are pinned ({s}/{t}), as the handoff records, since s is not recoverable from I ✦ s.

    ⊧-interp : {s t : Term {𝑆 = 𝑆₁} X} β†’ 𝑩 βŠ§β‚‚ (I ✦ s) β‰ˆ (I ✦ t) β†’ reductα΄΅ βŠ§β‚ s β‰ˆ t
    ⊧-interp {s = s} {t} B⊧ η =
      β‰ˆtrans (reductα΄΅-interp s Ξ·) (β‰ˆtrans (B⊧ Ξ·) (β‰ˆsym (reductα΄΅-interp t Ξ·)))

    ⊧-uninterp : {s t : Term {𝑆 = 𝑆₁} X} β†’ reductα΄΅ βŠ§β‚ s β‰ˆ t β†’ 𝑩 βŠ§β‚‚ (I ✦ s) β‰ˆ (I ✦ t)
    ⊧-uninterp {s = s} {t} R⊧ η =
      β‰ˆtrans (β‰ˆsym (reductα΄΅-interp s Ξ·)) (β‰ˆtrans (R⊧ Ξ·) (reductα΄΅-interp t Ξ·))

reductα΄΅ generalizes reduct

When the interpretation is the one induced by a signature morphism, its reduct is the ordinary signature reduct, operation by operation, by refl β€” the algebra-level witness that _✦_ (and hence this whole development) extends to derived operations.

  reductα΄΅-⟨⟩ : {Ο† : SigMorphism 𝑆₁ 𝑆₂} {o : OperationSymbolsOf 𝑆₁}
    β†’ o ^ reductα΄΅ ⟨ Ο† ⟩ᴡ ≑ o ^ reduct Ο† 𝑩
  reductᴡ-⟨⟩ = refl

The interpretability quasi-order

A theory is an indexed family of equations. 𝑨 βŠ¨β‚‘ β„° is the assertion that 𝑨 models every equation in β„°.

module _ {𝑆 : Signature π“ž π“₯} where
  open EqLogic using ( _⊧_β‰ˆ_ )

  infix 4 _βŠ¨β‚‘_
  _βŠ¨β‚‘_ : {Idx : Type ΞΉ} β†’ Algebra {𝑆 = 𝑆} Ξ± ρ β†’ (Idx β†’ Term {𝑆 = 𝑆} X Γ— Term {𝑆 = 𝑆} X) β†’ Type _
  𝑨 βŠ¨β‚‘ β„° = βˆ€ k β†’ 𝑨 ⊧ proj₁ (β„° k) β‰ˆ projβ‚‚ (β„° k)

Composition of interpretations carries through satisfaction. This is the reduct-level shadow of ✦-∘: a (J ∘ᴡ I)-reduct satisfies exactly what the iterated reduct reductα΄΅ I (reductα΄΅ J π‘ͺ) satisfies, by two applications of the satisfaction condition and one ✦-∘ rewrite. It is the engine of transitivity below.

module _
  {𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯}
  (I : Interpretation 𝑆₁ 𝑆₂)
  (J : Interpretation 𝑆₂ 𝑆₃)
  (π‘ͺ : Algebra {𝑆 = 𝑆₃} Ξ± ρ)
  where
  open EqLogic using ( _⊧_β‰ˆ_ )

  reductα΄΅-∘-⊧ : {s t : Term {𝑆 = 𝑆₁} X}
    β†’ reductα΄΅ (reductα΄΅ π‘ͺ J) I ⊧ s β‰ˆ t β†’ reductα΄΅ π‘ͺ (J ∘ᴡ I) ⊧ s β‰ˆ t
  reductᴡ-∘-⊧ {s = s} {t} hyp =
    ⊧-interp π‘ͺ (J ∘ᴡ I) {s = s} {t}
      (⊧-≐ π‘ͺ (≐-isSym (✦-∘ s)) (≐-isSym (✦-∘ t))
        (⊧-uninterp π‘ͺ J {s = I ✦ s} {t = I ✦ t}
          (⊧-uninterp (reductα΄΅ π‘ͺ J) I {s = s} {t = t} hyp)))

ℰ₁ β‰Ό β„°β‚‚ says ℰ₁ (a theory of 𝑆₁) is interpretable in β„°β‚‚ (a theory of 𝑆₂): some interpretation's reduct sends every β„°β‚‚-model to an ℰ₁-model. The relation is indexed by the algebra-level pair (Ξ± , ρ) at which models are tested, exactly as the satisfaction relations are.

module Interpret (α ρ : Level) where

  _β‰Ό_ : {𝑆₁ 𝑆₂ : Signature π“ž π“₯}
    {X₁ : Type χ₁} {Xβ‚‚ : Type Ο‡β‚‚} {Idx₁ : Type ι₁} {Idxβ‚‚ : Type ΞΉβ‚‚}
    β†’ (Idx₁ β†’ Term {𝑆 = 𝑆₁} X₁ Γ— Term {𝑆 = 𝑆₁} X₁)
    β†’ (Idxβ‚‚ β†’ Term {𝑆 = 𝑆₂} Xβ‚‚ Γ— Term {𝑆 = 𝑆₂} Xβ‚‚) β†’ Type _
  _β‰Ό_ {𝑆₁ = 𝑆₁} {𝑆₂ = 𝑆₂} ℰ₁ β„°β‚‚ =
    Ξ£[ I ∈ Interpretation 𝑆₁ 𝑆₂ ]
      ((𝑩 : Algebra {𝑆 = 𝑆₂} Ξ± ρ) β†’ 𝑩 βŠ¨β‚‘ β„°β‚‚ β†’ reductα΄΅ 𝑩 I βŠ¨β‚‘ ℰ₁)

  infix 4 _β‰Ό_

Reflexivity: the identity interpretation works, because idα΄΅ ✦_ is the identity up to _≐_ (✦-id) and satisfaction respects _≐_.

module _ α ρ where

  open Interpret α ρ

  β‰Ό-refl : {𝑆 : Signature π“ž π“₯} {X : Type Ο‡} {Idx : Type ΞΉ}
    (β„° : Idx β†’ Term X Γ— Term X) β†’ β„° β‰Ό β„°
  β‰Ό-refl {𝑆 = 𝑆} β„° = idα΄΅ , red
    where
    red : (𝑩 : Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ 𝑩 βŠ¨β‚‘ β„° β†’ reductα΄΅ 𝑩 idα΄΅ βŠ¨β‚‘ β„°
    red 𝑩 B⊨ k =
      ⊧-interp 𝑩 idα΄΅ {s = proj₁ (β„° k)} {t = projβ‚‚ (β„° k)}
        (⊧-≐ 𝑩 (≐-isSym (✦-id (β„° k .proj₁))) (≐-isSym (✦-id (β„° k .projβ‚‚))) (B⊨ k))

Transitivity: compose the interpretations with _∘ᴡ_, chain the two reduct implications, and re-fold the iterated reduct into the composite reduct with reductᴡ-∘-⊧.

  β‰Ό-trans : {𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯}
    {X₁ : Type χ₁} {Xβ‚‚ : Type Ο‡β‚‚} {X₃ : Type χ₃}
    {Idx₁ : Type ι₁} {Idxβ‚‚ : Type ΞΉβ‚‚} {Idx₃ : Type ι₃}
    (ℰ₁ : Idx₁ β†’ Term {𝑆 = 𝑆₁} X₁ Γ— Term {𝑆 = 𝑆₁} X₁)
    (β„°β‚‚ : Idxβ‚‚ β†’ Term {𝑆 = 𝑆₂} Xβ‚‚ Γ— Term {𝑆 = 𝑆₂} Xβ‚‚)
    (ℰ₃ : Idx₃ β†’ Term {𝑆 = 𝑆₃} X₃ Γ— Term {𝑆 = 𝑆₃} X₃)
    β†’ ℰ₁ β‰Ό β„°β‚‚ β†’ β„°β‚‚ β‰Ό ℰ₃ β†’ ℰ₁ β‰Ό ℰ₃

  β‰Ό-trans {𝑆₃ = 𝑆₃} ℰ₁ β„°β‚‚ ℰ₃ (I , Ihyp) (J , Jhyp) = J ∘ᴡ I , red
    where
    red : (π‘ͺ : Algebra {𝑆 = 𝑆₃} Ξ± ρ) β†’ π‘ͺ βŠ¨β‚‘ ℰ₃ β†’ reductα΄΅ π‘ͺ (J ∘ᴡ I) βŠ¨β‚‘ ℰ₁
    red π‘ͺ C⊨ k =
      reductα΄΅-∘-⊧ I J π‘ͺ {s = proj₁ (ℰ₁ k)} {t = projβ‚‚ (ℰ₁ k)}
        (Ihyp (reductα΄΅ π‘ͺ J) (Jhyp π‘ͺ C⊨) k)

  1. O. C. GarcΓ­a and W. Taylor, The Lattice of Interpretability Types of Varieties, Mem. Amer. Math. Soc. 50 (1984), no. 305. ↩

  2. Infinitary CSP over Ο‰-categorical templates. ↩