A signature Σ is a set of functional characters, where each character fis associated with an integer called arity f. Intuitively, functions represented by a symbol fcan only be applied to arguments arity(f).
Example: Σ = {f / 2, g / 3}
Let Σ be a signature. A Σ-algebra consists of:
- set
A - mapping between functional symbols Σ on a function
(fA : A^n → A), where nis the arity of the symbol f.
My problem is that I have some problems formalizing these concepts (especially the arity of function symbols). I think I should use dependent types, but I am not familiar with them yet.
What I have 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}.
... .
: