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

{-# OPTIONS --without-K --exact-split --safe #-} open import Algebras.Basic module Terms.Basic {š : Signature š š„} where -- Imports from Agda and the Agda Standard Library ---------------- open import Agda.Primitive using ( Level ) renaming ( Set to Type ) open import Data.Product using ( _,_ ) -- Imports from the Agda Universal Algebra Library ---------------- open import Overture.Preliminaries using ( ā£_ā£ ; ā„_ā„ ) open import Algebras.Products {š = š} using ( ov ) private variable Ļ : Level

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

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 `š ā š„ ā lsuc Ļ`

.

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