Expressions Algebras

(* Definition of the algebra of expressions over a signature. *)
(* Venanzio Capretta, January 1999                            *)
(* Coq version 6.2.3                                          *)

Require Export Algebras.
Require Export General_Trees.

(* The definition is similar to the one of (closed) open terms.    The only difference is that we extend every sort with an infinite    set of variables indexed on the natural numbers. *)

Implicit Arguments On.

Section Expressions_Algebras_Sets.

Variable sigma : Signature.

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

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

(* A variable is represented  by a pair (a,m) where    a is the index of the sort and m a natural number. *)
Definition Var := A*nat.

(* Sort of a variable. *)
Definition var_sort : Var -> A :=
[v](Fst v).

(* Type of indexes for functions and variables. *)
Local B := (Finite m) + Var.

(* (C b) is the type index for the arguments of the function with index b.    Variables are treated like constants: they don't have arguments. *)
Local C : B -> Set :=
[b:B]Cases b of
    (inl f) => (Finite (function_type_arity (nth_function f)))
  | (inr v) => (Finite O)
end.

(* Index of the sort of the result of the function with index b.    In the case of a variable it is just the sort of the variable. *)
Local f : B -> A :=
[b:B]Cases b of
    (inl f) => (function_type_result (nth_function f))
  | (inr v) => (var_sort v)
end.

(* Index of the sort of the argument of index c    of the function with index b.    In case of a variable it is a default value. *)
Local g : (b:B)(C b) -> A :=
[b:B]<[b:B](C b) -> A>
Cases b of
    (inl f) => [c](function_type_arg c)
  | (inr v) => [c](empty_finite_O A c)
end.

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

(* Immersion of the variables into Expressions. *)
Definition var_ex : (v:Var)(Expression (fst ? ? v)) :=
  [v:Var]
  Cases v of
    (s, x) => (!g_tree A B C f g
                      (inr (Finite m) Var v)
                      [z](empty_finite_O ? z)
              )
  end.

Local Sorts : (Sorts_interpretation n) := Expression.

(* Definition of the interpretation of the functions on the expressions    algebra. (fun i) will be the interpretation of the function    (nth_function sigma i). *)

Section Expression_Fun_Setoid.

Variable i : (Finite m).
Local b : B := (inl ? ? i).

Local n0 : nat := (nth_arity i).
Local A0 : (Finite n0) -> Setoid := [c:(C b)](Expression (g c)).
Local B0 : Setoid := (FF_setoid n0 A0).
(* B0 is the setoid of admissible arguments (in functional form)    for the i-th function. *)

Local C0 : Setoid := (Expression (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 fi := (nth_function i).

Definition function_i :
  (Function_type_interpretation Sorts fi)
:=
  (setoid_function f_b_well_defined).

End Expression_Fun_Setoid.

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

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

End Expressions_Algebras_Sets.

Implicit Arguments Off.

25/02/99, 14:36