Skip to content

Legacy.Base.Terms.Basic

Basic Definitions

This is the Legacy.Base.Terms.Basic module of the Agda Universal Algebra Library.


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

open import Overture using (Signature ; š“ž ; š“„ )

module Legacy.Base.Terms.Basic {š‘† : Signature š“ž š“„} where

-- Imports from Agda and the Agda Standard Library ----------------
open import Agda.Primitive         using () renaming ( Set to Type )
open import Data.Product           using ( _,_ )
open import Level                  using ( Level )

-- Imports from the Agda Universal Algebra Library ----------------
open import Overture          using ( āˆ£_āˆ£ ; āˆ„_āˆ„ )
open import Legacy.Base.Algebras {š‘† = š‘†}  using ( Algebra ; ov )

private variable Ļ‡ : Level

The type of terms

Fix a signature š‘† and let X denote an arbitrary nonempty collection of variable symbols. Assume the symbols in X are distinct from the operation symbols of š‘†, that is X āˆ© āˆ£ š‘† āˆ£ = āˆ….

By a word in the language of š‘†, we mean a nonempty, finite sequence of members of X āˆŖ āˆ£ š‘† āˆ£. We denote the concatenation of such sequences by simple juxtaposition.

Let Sā‚€ denote the set of nullary operation symbols of š‘†. We define by induction on n the sets š‘‡ā‚™ of words over X āˆŖ āˆ£ š‘† āˆ£ as follows (cf. Bergman (2012) Def. 4.19):

š‘‡ā‚€ := X āˆŖ Sā‚€ and š‘‡ā‚™ā‚Šā‚ := š‘‡ā‚™ āˆŖ š’Æā‚™

where š’Æā‚™ is the collection of all f t such that f : āˆ£ š‘† āˆ£ and t : āˆ„ š‘† āˆ„ f ā†’ š‘‡ā‚™. (Recall, āˆ„ š‘† āˆ„ f is the arity of the operation symbol f.)

We define the collection of terms in the signature š‘† over X by Term X := ā‹ƒā‚™ š‘‡ā‚™. By an š‘†-term we mean a term in the language of š‘†.

The definition of Term X is recursive, indicating that an inductive type could be used to represent the semantic notion of terms in type theory. Indeed, such a representation is given by the following inductive type.


data Term (X : Type Ļ‡ ) : Type (ov Ļ‡)  where
 ā„Š : X ā†’ Term X    -- (ā„Š for "generator")
 node : (f : āˆ£ š‘† āˆ£)(t : āˆ„ š‘† āˆ„ f ā†’ Term X) ā†’ Term X

open Term

{-# WARNING_ON_USAGE Term
"Use Overture.Terms.Term instead.  Legacy.Base.Terms.Term is deprecated and will be removed one minor version after #303 lands."
#-}
{-# WARNING_ON_USAGE ā„Š
"Use Overture.Terms.ā„Š instead.  Legacy.Base.Terms.ā„Š is deprecated and will be removed one minor version after #303 lands."
#-}
{-# WARNING_ON_USAGE node
"Use Overture.Terms.node instead.  Legacy.Base.Terms.node is deprecated and will be removed one minor version after #303 lands."
#-}

This is a very basic inductive type that represents each term as a tree with an operation symbol at each node and a variable symbol at each leaf (generator).

Notation. As usual, the type X represents an arbitrary collection of variable symbols. Recall, ov Ļ‡ is our shorthand notation for the universe level š“ž āŠ” š“„ āŠ” suc Ļ‡.

The term algebra

For a given signature š‘†, if the type Term X is nonempty (equivalently, if X or āˆ£ š‘† āˆ£ is nonempty), then we can define an algebraic structure, denoted by š‘» X and called the term algebra in the signature š‘† over X. Terms are viewed as acting on other terms, so both the domain and basic operations of the algebra are the terms themselves.

  • For each operation symbol f : āˆ£ š‘† āˆ£, denote by f Ģ‚ (š‘» X) the operation on Term X that maps a tuple t : āˆ„ š‘† āˆ„ f ā†’ āˆ£ š‘» X āˆ£ to the formal term f t.
  • Define š‘» X to be the algebra with universe āˆ£ š‘» X āˆ£ := Term X and operations f Ģ‚ (š‘» X), one for each symbol f in āˆ£ š‘† āˆ£.

In Agda the term algebra can be defined as simply as one could hope.


š‘» : (X : Type Ļ‡ ) ā†’ Algebra (ov Ļ‡)
š‘» X = Term X , node