Понимание семантики за кодом

Question

У меня есть код 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 

Это треска e:

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, это мне очень поможет.

Answer 1

Кажется, что он принимает многочлен от векторного пространства и вычисляет сумму всех (транспонированных) (матричных) коэффициентов, приложенных к каждой переменной. args - массив, такой, что args.(i) представляет собой сумму всех коэффициентов на i -й переменной и const сумму постоянных скаляров.

Я не знаю, в чем смысл этой операции, но я подозреваю, что это не имеет большого значения в общем случае (работа над произвольными произведениями сумм продуктов ..., что приведет к странным не- линейное/однородное поведение). Я полагаю, что существуют неявные ограничения на то, что форма фактических значений этого типа полинома, например, может быть линейной по всем переменным.