0

我有一个 OCaml 代码，我很难将函数形式化mi_pol为 Coq，因为我不清楚这段代码到底是什么工作，例如在

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

和

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

和

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

这是代码：

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";;

任何帮助都非常感谢。如果你有一个 Coq 代码，对mi_pol我有很大帮助。

4

1 回答 1

3

它似乎在向量空间上采用多项式，并计算附加到每个变量的所有（转置）（矩阵）系数的总和。args是一个数组，它是第 -th 变量args.(i)上所有系数的总和，以及常数标量的总和。iconst

我不知道这个操作的含义是什么，但我怀疑它在一般情况下并没有多大意义（处理......乘积之和的任意乘积；这会导致奇怪的非线性/同质行为）。我想对于这种多项式类型的实际值的形状存在隐式约束，例如它可能在所有变量中都是线性的。

于 2013-05-06T06:19:59.920 回答