---
layout: default
title : "Legacy.Base.Terms.Basic module (The Agda Universal Algebra Library)"
date : "2021-01-14"
author: "the agda-algebras development team"
---

### <a id="basic-definitions">Basic Definitions</a>

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


```agda


{-# 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
```


#### <a id="the-type-of-terms">The type of terms</a>

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.


```agda


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 Ļ‡`.


#### <a id="the-term-algebra">The term algebra</a>

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.


```agda


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