Skip to content

Overture.Terms.Interpretation

Theory interpretations: sending operation symbols to derived terms

This is the Overture.Terms.Interpretation module of the Agda Universal Algebra Library.

A signature morphism Ο† : SigMorphism 𝑆₁ 𝑆₂ (Overture.Signatures.Morphisms) relabels each operation symbol of 𝑆₁ to an operation symbol of 𝑆₂. A theory interpretation generalizes this one decisive step: it sends each operation symbol o of 𝑆₁ to a term of 𝑆₂ β€” a derived operation of 𝑆₂, an 𝑆₂-term in the argument positions ArityOf 𝑆₁ o of o.

This is the term-valued generalization of a signature morphism, and it is exactly the data with which universal algebra defines one variety's operations inside another (Garcia–Taylor's "definitions"1): a Maltsev term, a majority term, or a near-unanimity term is such an assignment of one fresh symbol to a derived term.

signature morphism Ο† :   o ↦ ΞΉ Ο† o                            (one symbol)
interpretation     I :   o ↦ (an 𝑆₂-term over ArityOf 𝑆₁ o)   (a derived operation)

Like the signature-morphism translation Ο† ✢_ (Overture.Terms.Translation), an interpretation acts on whole terms: I ✦ t rewrites an 𝑆₁-term t into an 𝑆₂-term over the same variables. The leaf clause fixes variables; the node clause is where the generalization lives β€” where Ο† ✢_ relabels the node node f ts to node (ΞΉ Ο† f) …, the interpretation substitutes the translated subterms into the chosen derived term I f.

Substitution into a term β€” grafting one tree onto the leaves of another β€” is the operation we call graft below; it is the term monad's bind, stated at heterogeneous variable levels (the positions ArityOf 𝑆₁ f live at level π“₯, the term's variables at an arbitrary level Ο‡), which the level-homogeneous Sub / _[_] of Setoid.Terms.Basic cannot express.

Everything here presupposes only the signatures β€” no setoid, no equality on any carrier β€” so it lives in Overture/, exactly as Term and Ο† ✢_ do. The laws of _✦_ (congruence, functoriality, the substitution square) compare functions on positions and so require the equality-of-terms relation _≐_; they are proved in Setoid.Terms.Interpretation. The equation-preserving half of a theory interpretation β€” that it carries one theory's laws into another's β€” needs satisfaction and lives in Setoid.Varieties.Interpretation, the analogue of Setoid.Varieties.Invariance for reduct.

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

module Overture.Terms.Interpretation where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Level           using ( Level ; suc ; _βŠ”_ )
open import Function        using ( _∘_ )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Signatures            using  ( π“ž ; π“₯ ; Signature
                                                  ; OperationSymbolsOf ; ArityOf )
open import Overture.Signatures.Morphisms  using  ( SigMorphism ; ΞΉ ; ΞΊ )
open import Overture.Terms.Basic           using  ( Term ; β„Š ; node )

private variable
  Ο‡ ΞΎ : Level
  X : Type Ο‡
  Y : Type ΞΎ
  𝑆 𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯

Interpretations

An Interpretation 𝑆₁ 𝑆₂ assigns to each operation symbol o in 𝑆₁ an 𝑆₂-term over argument positions ArityOf 𝑆₁ o. Reading position i : ArityOf 𝑆₁ o as the variable "the i-th argument of o", the assigned term I o is the recipe for computing o from its arguments using only 𝑆₂-operations.

Interpretation : (𝑆₁ 𝑆₂ : Signature π“ž π“₯) β†’ Type (π“ž βŠ” suc π“₯)
Interpretation 𝑆₁ 𝑆₂ = (o : OperationSymbolsOf 𝑆₁) β†’ Term {𝑆 = 𝑆₂} (ArityOf 𝑆₁ o)

Grafting: substitution at heterogeneous levels

Given a term t and a map Οƒ : Y β†’ Term {𝑆 = 𝑆} X, the application graft t Οƒ replaces each leaf β„Š y of the term t by the term Οƒ y, recursing through nodes (the term monad's bind). This is _[_] of Setoid.Terms.Basic, but stated for variable types Y and X at independent universe levels, which is what the interpretation action below needs: it grafts an 𝑆₂-term over the positions ArityOf 𝑆₁ f (level π“₯) into one over the term's own variables.

graft : Term {𝑆 = 𝑆} Y β†’ (Y β†’ Term {𝑆 = 𝑆} X) β†’ Term {𝑆 = 𝑆} X
graft (β„Š y) Οƒ = Οƒ y
graft (node f ts) Οƒ = node f (Ξ» i β†’ graft (ts i) Οƒ)

The interpretation action on terms

Given an 𝑆₁-𝑆₂-interpretation I, and an 𝑆₁-term t, I ✦ t translates t to an 𝑆₂-term over the same variables.2

Variables are fixed points (I ✦ β„Š x is β„Š x, definitionally), so environments transfer across the action unchanged. At a node, the subterms are translated and then grafted into the chosen derived term I f.

infix 15 _✦_

_✦_ : Interpretation 𝑆₁ 𝑆₂ β†’ Term {𝑆 = 𝑆₁} X β†’ Term {𝑆 = 𝑆₂} X
I ✦ β„Š x = β„Š x
I ✦ node f ts = graft (I f) (Ξ» i β†’ I ✦ ts i)

Identity, composition, and the embedding of signature morphisms

Interpretations are the morphisms of a category whose objects are signatures β€” the clone category of algebraic theories. The identity interpretation sends each symbol to itself, applied to its own argument variables; composition runs an interpretation's derived terms through a second interpretation. (That these satisfy the category laws β€” I ✦_ is functorial in I β€” is the content of ✦-id and ✦-∘ in Setoid.Terms.Interpretation.)

idα΄΅ : Interpretation 𝑆 𝑆
idα΄΅ o = node o β„Š

infixr 9 _∘ᴡ_

_∘ᴡ_ : Interpretation 𝑆₂ 𝑆₃ β†’ Interpretation 𝑆₁ 𝑆₂ β†’ Interpretation 𝑆₁ 𝑆₃
(J ∘ᴡ I) o = J ✦ I o

Every signature morphism is an interpretation: send o to the single-application derived term node (ΞΉ Ο† o) (Ξ» j β†’ β„Š (ΞΊ Ο† o j)) β€” apply the relabelled symbol ΞΉ Ο† o to its arguments, reindexed back through ΞΊ Ο† o. This is the inclusion of Sig (Overture.Signatures.Morphisms) into the clone category, and ✦-⟨⟩ (Setoid.Terms.Interpretation) checks that the embedded interpretation acts on terms exactly as Ο† ✢_ does, so theory interpretations strictly generalize signature morphisms.

⟨_⟩ᴡ : SigMorphism 𝑆₁ 𝑆₂ β†’ Interpretation 𝑆₁ 𝑆₂
⟨ Ο† ⟩ᴡ o = node (ΞΉ Ο† o) (β„Š ∘ (ΞΊ Ο† o))

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

  2. Unicode tip. Type \st and select ✦ to get the four-pointed star; it is the _✢_ of Overture.Terms.Translation "thickened", since _✦_ generalizes _✢_ from one application to an arbitrary derived term. ↩