Algebras

(*        UNIVERSAL ALGEBRA         *)
(* Definition of a sigma-algebra.   *)
(* Venanzio Capretta, January 1999  *)
(* Coq version 6.2.3                *)

Require Export Signatures.
Require Export Setoids.
Require Export Type_Constructions.
Require Export Finite_Sets.
Require Export Type_Products.
Require Export Parametric_Arity_Functions.

Implicit Arguments On.

Section Signature_Interpretations.

Variable n : nat.

(* Definition of the interpretation of the sorts.  *)
Definition Sorts_interpretation := (Finite n) -> Setoid.

Variable sorts : Sorts_interpretation.

(* Interpretation of a function type. The function takes its arguments    in the form of a function. *)

Definition Fun_type_int : (list (Finite n)) -> (Finite n) -> Setoid :=
[args][res]
(Fun_arg_function (length args)
                  [i](sorts (Fin_proj args i))
                  (sorts res)
).

Definition Function_type_interpretation : (Function_type n) -> Setoid :=
[f](Fun_type_int (function_type_arguments f)
                 (function_type_result f)
   ).

Definition Function_list_interpretation :
  (list (Function_type n)) -> Setoid :=
[fs]
(FF_setoid (length fs)
           [i](Function_type_interpretation (Fin_proj fs i))
).

End Signature_Interpretations.

Record Algebra [sign : Signature] : Type := algebra
  { sorts :> (Sorts_interpretation (sorts_num sign));
    functions : (Function_list_interpretation sorts (function_types sign))
  }.

(* The selector functions gives the family of curried functions. *)
(* For some purposes it is desirable to have them in a different    form where the arguments are given as a function on a finite set.    We already defined the commuting operator in Parametric_Arity_Functions.    Now we use it to obtain the desired representation of the functions. *)

Section Fun_Arg_Functions.

Variable sigma : Signature.
Variable A : (Algebra sigma).

Local As := (sorts A).

Local n := (sorts_num sigma).
Local m := (fun_num sigma).

Variable i : (Finite m). (* we consider the i-th function *)

Local fi := (nth_function i).
Local r := (nth_arity i).
Local a := (nth_arg 2!i).
Local h := (nth_result i).

Local fiA := (functions A i).

(* The family of indexes of sorts of the arguments of fi. *)
Definition Function_arguments_sorts := [j : (Finite r)](As (a j)).

(* Now from fiA we define the corresponding function that takes    a function argument. *)
Definition curry_functions :
  (Curry_setoid_function r Function_arguments_sorts (As h))
:=
  ((fun_arg_to_curry r Function_arguments_sorts (As h)) fiA).

(* In general it will be also useful to have the type of argument for    such a function. *)
Definition Fun_arg_arguments :=
  (FF_setoid r Function_arguments_sorts).

End Fun_Arg_Functions.

Implicit Arguments Off.

25/02/99, 14:36