A signature Σ is a set of function symbols where each symbol f is associated to an integer called the arity of f. Intuively, functions represented by a symbol f can only be applied to arity(f) arguments.
Example : Σ = {f/2, g/3}
Let Σ be a signature. A Σ-algebra is made of :
- a set
A - a mapping between function symbols of Σ to a function
(fA : A^n → A)wherenis the arity of the symbolf.
My problem is that I have some troubles formalizing these concepts (especially the arity of function symbols). I think I have to use dependent types but I'm not really familiar with them yet.
What I've tried so far :
Definition function_symbol := ascii.
Definition signature : Type := (list function_symbol) * arity.
Inductive sigma_term (sigma:signature) : Type :=
| SigmaVar : variable -> sigma_term sigma
| SigmaFunc f :
let functions := fst sigma in
let arity := snd sigma in
In f functions -> ilist term (arity f) -> sigma_term sigma.
Definition sigma_algebra (sigma:signature) : Type :=
let arity := snd sigma in
{A : Type & forall f:function_symbol, nfun A (arity f) A}.
But it may be a bit over-complicated... I'm open to a better formalization.
References :
- ilist (CPDT)
- nfun (Coq Standard Library)
- Universal Algebra where Σ-algebras are simply called algebras