---
layout: default
file: "src/Overture/Terms/Interpretation.lagda.md"
title: "Overture.Terms.Interpretation module"
date: "2026-06-15"
author: "the agda-algebras development team"
---

### 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`{.AgdaFunction} 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`{.AgdaFunction} / `_[_]`{.AgdaFunction} 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`{.AgdaDatatype} and `Ο† ✢_` do.
The laws of `_✦_`{.AgdaFunction} (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`.

<!--
```agda
{-# 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.

```agda
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 `_[_]`{.AgdaFunction} 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.

```agda
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`.

```agda
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`{.AgdaFunction} and
`✦-∘`{.AgdaFunction} in [Setoid.Terms.Interpretation][].)

```agda
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 `✦-⟨⟩`{.AgdaFunction}
([Setoid.Terms.Interpretation][]) checks that the embedded interpretation acts on terms
exactly as `Ο† ✢_` does, so theory interpretations strictly generalize signature
morphisms.

```agda
⟨_⟩ᴡ : 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.