CODEWITHSUNDEEP
ocamlcoq
Quyen
Quyen

Reputation: 1373

Understanding the semantics behind the code

I have an OCaml code, and I have a hard time to formalize the function mi_pol into Coq because I am not understand clearly what exactly this code working, for example at the 

aux (vec_add add const (vector ci v)) args ps

and

args.(i-1) <- mat_add add args.(i-1) (matrix ci m); aux const args ps

and

aux (vec_0 z dim) (Array.make n (mat_0 z dim)) ps

This is the code:

let vector = List.map;;

let clist x =
  let rec aux k = if k <= 0 then [] else x :: aux (k-1) in aux;;

let vec_add add v1 v2 =
  try List.map2 add v1 v2
  with Invalid_argument _ ->
    error_fmt "sum of two vectors of different size";;

let mat_add add m1 m2 =
  try List.map2 (vec_add add) m1 m2
  with Invalid_argument _ ->
    error_fmt "sum of two matrices of different size";;

(*vector zero *)
let vec_0 z dim = clist z dim;;  

(* matrix zero *)
let mat_0 z dim = clist (vec_0 z dim) dim;;
let comp f g x = f (g x);;

(* matrix transpose *)
let transpose ci =
  let rec aux = function
    | [] | [] :: _ -> []
    | cs -> List.map (comp ci List.hd) cs :: aux (List.map List.tl cs)
  in aux;;  

(* matrix *)
let matrix ci m =
  try transpose ci m
  with Failure _ -> error_fmt "ill-formed matrix";;

let mi_pol z add ci =
  let rec aux const args = function
    | [] -> { mi_const = const; mi_args = Array.to_list args }
    | Polynomial_sum qs :: ps -> aux const args (qs @ ps)
    | Polynomial_coefficient (Coefficient_matrix [v]) :: ps
    | Polynomial_coefficient (Coefficient_vector v) :: ps ->
      aux (vec_add add const (vector ci v)) args ps
    | Polynomial_product [p] :: ps -> aux const args (p :: ps)
    | Polynomial_product [Polynomial_coefficient (Coefficient_matrix m); 
                          Polynomial_variable i] :: ps ->
      args.(i-1) <- mat_add add args.(i-1) (matrix ci m);
      aux const args ps
    | _ -> not_supported "todo"
  in fun dim n -> function
    | Polynomial_sum ps -> aux (vec_0 z dim) (Array.make n (mat_0 z dim)) ps
    | _ -> not_supported
      "todo";;

Any help is very appreciate. If you can have a Coq code for mi_pol it will help me a lot.

Upvotes: 0

Views: 110

Answers (1)

gasche
gasche

Reputation: 31459

It appears to take a polynomial on a vector space, and compute the sum of all the (transpose of) (matrix) coefficients attached to each variable. args is an array such that args.(i) is the sum of all coefficients on the i-th variable, and const the sum of constant scalars.

I don't know what's the meaning of this operation, but I suspect it doesn't mean much in the general case (working over arbitrary products of sums of products of ...; that would lead to strange non-linear/homogeneous behaviors). I suppose there are implicit constraints on what the shape of actual values of this polynomial type are, for example it may be linear in all variables.

Upvotes: 3

Related Questions