Skip to content

Overture.Terms.Translation

Translating terms along a signature morphism

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

A signature morphism Ο† : SigMorphism 𝑆₁ 𝑆₂ (Overture.Signatures.Morphisms) relabels operation symbols (ΞΉ Ο†, covariantly) and reindexes argument positions (ΞΊ Ο†, contravariantly). This module extends that relabelling from single symbols to whole terms: the translation Ο† ✢ t rewrites an 𝑆₁-term t into an 𝑆₂-term over the same variables, leaf by leaf and node by node.

The definition is exactly the structural recursion one would guess, and it is worth reading the node clause slowly because the contravariance of ΞΊ is where all the content lives. A node node f ts of an 𝑆₁-term carries one subterm ts i for each position i : ArityOf 𝑆₁ f. Its translation is a node labelled ΞΉ Ο† f, which must carry one subterm for each position j : ArityOf 𝑆₂ (ΞΉ Ο† f) β€” a position of the target symbol. The position map ΞΊ Ο† f converts such a j back into a source position ΞΊ Ο† f j, and the translated subterm at j is the translation of ts (ΞΊ Ο† f j):

   𝑆₁-term:  node f ts          with subterms    ts i , i : ArityOf 𝑆₁ f
                  β”‚
                  β”‚  Ο† ✢_
                  ↓
   𝑆₂-term:  node (ΞΉ Ο† f) tsβ€²   with subterms    tsβ€² j = Ο† ✢ ts (ΞΊ Ο† f j) , j : ArityOf 𝑆₂ (ΞΉ Ο† f)

In the typical case of a signature inclusion β€” ΞΉ injective, each ΞΊ Ο† f the identity, as in Sig-Magma β†ͺ Sig-Monoid β€” the translation simply re-reads a magma term such as (x βˆ™ y) βˆ™ z as the same expression in the monoid signature. That "same expression, richer signature" reading is what makes the translation the syntactic half of the reduct: reduct Ο† moves algebras from 𝑆₂ to 𝑆₁ (Setoid.Algebras.Reduct), Ο† ✢_ moves terms from 𝑆₁ to 𝑆₂, and the two are adjoint in the logical sense that satisfaction is invariant β€” reduct Ο† 𝑨 ⊧ s β‰ˆ t iff 𝑨 ⊧ Ο† ✢ s β‰ˆ Ο† ✢ t (Setoid.Varieties.Invariance). In the vocabulary of M4-5b, Ο† ✢_ is the unique extension of the natural transformation ⟦ Ο† ⟧ : ⟨ 𝑆₁ ⟩ ⟹ ⟨ 𝑆₂ ⟩ from single applications to free P_{𝑆₁}-algebras; in monad vocabulary it is a morphism of term monads, a fact recorded (up to _≐_) in Setoid.Terms.Translation.

Like Term itself, the translation presupposes only the signatures β€” no setoid, no equality on any carrier β€” so it lives in Overture/. Its laws (functoriality in Ο†, congruence, and the substitution square) require the equality-of-terms relation _≐_ and are therefore stated in Setoid.Terms.Translation, mirroring the Overture.Terms / Setoid.Terms.Basic split. M4-5f will generalize precisely this definition: a theory interpretation sends operation symbols to derived operations (terms) rather than to symbols, and its action on terms replaces the node clause's relabelling by substitution into the chosen derived term.

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

module Overture.Terms.Translation where

open import Agda.Primitive                 using () renaming ( Set to Type )
open import Level                          using ( Level )
open import Overture.Signatures            using ( π“ž ; π“₯ ; Signature )
open import Overture.Signatures.Morphisms  using ( SigMorphism ; ΞΉ ; ΞΊ )

import Overture.Terms.Basic as Terms

private variable
  Ο‡ : Level
  X : Type Ο‡

The translation

The two signatures are instantiated by module application; Term₁ X and Termβ‚‚ X are the term types over the same variable type X.1

module _ {𝑆₁ 𝑆₂ : Signature π“ž π“₯} where
  open Terms {𝑆 = 𝑆₁} using () renaming (β„Š to β„Šβ‚; node to node₁; Term to Term₁)
  open Terms {𝑆 = 𝑆₂} using () renaming (β„Š to β„Šβ‚‚; node to nodeβ‚‚; Term to Termβ‚‚)
  infix 15 _✢_

  _✢_ : SigMorphism 𝑆₁ 𝑆₂ β†’ Term₁ X β†’ Termβ‚‚ X
  Ο† ✢ β„Šβ‚ x = β„Šβ‚‚ x
  Ο† ✢ node₁ f ts = nodeβ‚‚ (ΞΉ Ο† f) (Ξ» j β†’ Ο† ✢ ts (ΞΊ Ο† f j))

Variables are fixed points of the translation (Ο† ✢ β„Š x is β„Š x, definitionally), which is what lets environments transfer across it unchanged: interpreting Ο† ✢ t needs values for exactly the variables that interpreting t needs. The reduct-invariance theorem leans on this directly.

  1. Unicode tip. Type \st and select ✢ to get the star. ↩