↑ Top

Signatures

This is the Overture.Signatures module of the Agda Universal Algebra Library.


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

module Overture.Signatures where

-- Imports from the Agda (Builtin) and the Agda Standard Library -----------------------
open import Agda.Primitive  using () renaming ( Set to  Type )
open import Data.Product    using ( Ξ£-syntax )
open import Level           using ( Level ; suc ; _βŠ”_ )

variable π“ž π“₯ : Level

The variables π“ž and π“₯ are not private since, throughout the agda-algebras library, π“ž denotes the universe level of operation symbol types, while π“₯ denotes the universe level of arity types.

Theoretical background

In model theory, the signature 𝑆 = (𝐢, 𝐹, 𝑅, ρ) of a structure consists of three (possibly empty) sets 𝐢, 𝐹, and 𝑅—called constant symbols, function symbols, and relation symbols, respectivelyβ€”along with a function ρ : 𝐢 + 𝐹 + 𝑅 β†’ 𝑁 that assigns an arity to each symbol.

Often (but not always) 𝑁 = β„•, the natural numbers.

As our focus here is universal algebra, we are more concerned with the restricted notion of an algebraic signature (or signature for algebraic structures), by which we mean a pair 𝑆 = (𝐹, ρ) consisting of a collection 𝐹 of operation symbols and an arity function ρ : 𝐹 β†’ 𝑁 that maps each operation symbol to its arity; here, 𝑁 denotes the arity type.

Heuristically, the arity ρ 𝑓 of an operation symbol 𝑓 ∈ 𝐹 may be thought of as the β€œnumber of arguments” that 𝑓 takes as β€œinput”.

If the arity of 𝑓 is n, then we call 𝑓 an n-ary operation symbol. In case n is 0 (or 1 or 2 or 3, respectively) we call the function nullary (or unary or binary or ternary, respectively).

If A is a set and 𝑓 is a (ρ 𝑓)-ary operation on A, we often indicate this by writing 𝑓 : Aρ 𝑓 β†’ A. On the other hand, the arguments of such an operation form a (ρ 𝑓)-tuple, say, (a 0, a 1, …, a (ρf-1)), which may be viewed as the graph of the function a : ρ𝑓 β†’ A.

When the codomain of ρ is β„•, we may view ρ 𝑓 as the finite set {0, 1, …, ρ𝑓 - 1}.

Thus, by identifying the ρ𝑓-th power Aρ 𝑓 with the type ρ 𝑓 β†’ A of functions from {0, 1, …, ρ𝑓 - 1} to A, we identify the type Aρ f β†’ A with the function type (ρ𝑓 β†’ A) β†’ A.

Example.

Suppose 𝑔 : (m β†’ A) β†’ A is an m-ary operation on A.

Let a : m β†’ A be an m-tuple on A.

Then 𝑔 a may be viewed as 𝑔 (a 0, a 1, …, a (m-1)), which has type A.

Suppose further that 𝑓 : (ρ𝑓 β†’ B) β†’ B is a ρ𝑓-ary operation on B.

Let a : ρ𝑓 β†’ A be a ρ𝑓-tuple on A, and let h : A β†’ B be a function.

Then the following typing judgments obtain:

h ∘ a : ρ𝑓 β†’ B and 𝑓 (h ∘ a) : B.

The signature type

In the agda-algebras library we represent the signature of an algebraic structure using the following type.


Signature : (π“ž π“₯ : Level) β†’ Type (suc (π“ž βŠ” π“₯))
Signature π“ž π“₯ = Ξ£[ F ∈ Type π“ž ] (F β†’ Type π“₯)

Occasionally it is useful to obtain the universe level of a given signature.


Level-of-Signature : {π“ž π“₯ : Level} β†’ Signature π“ž π“₯ β†’ Level
Level-of-Signature {π“ž}{π“₯} _ = suc (π“ž βŠ” π“₯)

In the Base.Functions module of the agda-algebras library, special syntax is defined for the first and second projectionsβ€”namely, ∣_∣ and βˆ₯_βˆ₯, resp.

Consequently, if 𝑆 : Signature π“ž π“₯ is a signature, then

If 𝑓 : ∣ 𝑆 ∣ is an operation symbol in the signature 𝑆, then βˆ₯ 𝑆 βˆ₯ 𝑓 is the arity of 𝑓.

← Overture.Basic Overture.Operations β†’