ā†‘ Top

Basic Definitions

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

{-# OPTIONS --without-K --exact-split --safe #-}

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

module 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 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

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

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.

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

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

ā†‘ Base.Terms Base.Terms.Properties ā†’