Term Algebras

(* Definition of the term algebra associated to a signature. *)
(* Venanzio Capretta, January 1999                           *)
(* Coq version 6.2.3                                         *)

Require Export PolyList.
Require Export Signatures.
Require Export Algebras.
Require Export General_Trees.
Require Export Lists_Projections.
Require Export Parametric_Arity_Functions.

Implicit Arguments On.

(* We define the underline sets of a term algebras as inductive  *)
(* trees, using the type constructor for general trees.          *)

Section Term_Algebras_Sets.

Variable sigma : Signature.

Local n := (sorts_num sigma).
Local fs := (function_types sigma).

Local A := (Finite n). (* type of indexes for sorts *)

Local m := (fun_num sigma).
Local B := (Finite m). (* type of indexes for functions *)

Local C : B -> Set :=
[b:B](Finite (function_type_arity (Fin_proj fs b))).
   (* (C b) is the type of indexes for the arguments  *)
   (* of the function with index b                    *)

Local f : B -> A :=
[b:B](function_type_result (Fin_proj fs b)).
  (* index of the sort of the result of the function with index b *)

Local g : (b:B)(C b) -> A :=
[b:B][c:(C b)](function_type_arg c).
  (* index of the sort of the argument of index c *)
  (* of the function of index b                   *)

Local Term : A -> Setoid :=
  (General_Tree_Setoid f g).

Local Sorts : (Sorts_interpretation n) := Term.

(* Definition of the interpretation of the functions on the term algebra. *)
(* (fun b) will be the interpretation of the function (Fin_proj fs b).    *)

Section Term_Fun_Setoid.

Variable b : B.

Local n0 := (nth_arity b) : nat.
Local A0 : (Finite n0) -> Setoid := [c:(C b)](Term (g c)).
Local B0 : Setoid := (FF_setoid n0 A0).
Local C0 : Setoid := (Term (f b)).

Local f_b' : B0 -> C0 :=
[h : B0](!g_tree A B C f g b h).

Remark f_b_well_defined : (fun_well_defined f_b').

Local fb := (nth_function b) : (Function_type n).

Definition function_b :
  (Function_type_interpretation Sorts fb)
:=
  (setoid_function f_b_well_defined).

End Term_Fun_Setoid.

Local functions_interpretation :
  (Function_list_interpretation Sorts fs)
:=
  function_b.

Definition Term_algebra : (Algebra sigma) :=
  (algebra functions_interpretation).

(* We now prove that the components of the tree obtained by an application    or one of the functions are exactly the function index and the arguments. *)

Section Term_Components.

Variable b : B.

Local fb := (nth_function b).
Local r := (nth_arity b).
Local a := (nth_arg 2!b).
Local h := (nth_result b).

Variable args : (Fun_arg_arguments Term_algebra b).

Local Arg := (Function_arguments_sorts Term_algebra 3!b).
Local Res := (sorts Term_algebra h).

Local fbT : (Fun_arg_function r Arg Res)
          := (functions Term_algebra b).

Local t := (fbT args).

Local b' := (g_node t).
Local args' : (Fun_arg_arguments Term_algebra b')
            := (g_sub_trees 7!t).

Lemma term_fun_eq : b=b'.

Lemma term_args_eq : args = args'.

End Term_Components.

End Term_Algebras_Sets.

Implicit Arguments Off.

25/02/99, 14:36