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

ベクトル空間で多項式を取り、各変数に付加されたすべての (転置) (行列) 係数の合計を計算するように見えます。は、 -th 変数のすべての係数の合計、および定数スカラーの合計であるargsような配列です。args.(i)iconst

この操作の意味はわかりませんが、一般的なケースではあまり意味がないと思います（...の積の和の任意の積を処理すると、奇妙な非線形/同次の動作が発生します）。この多項式型の実際の値の形状には暗黙の制約があると思います。たとえば、すべての変数で線形である可能性があります。

于 2013-05-06T06:19:59.920 に答える