理解語義的代碼

我有一個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";;

任何幫助是非常感激。如果你的代碼可以爲mi_pol，它會對我很有幫助。

來源

2013-05-06 Quyen

這個問題非常嚴重的問。你承認甚至沒有理解代碼，但你想要正式化它？我想你在馬前面有車。 – 2013-05-06 05:50:01

投票結果爲「太局部」 - 不可能幫助未來的訪問者。 – 2013-05-06 14:49:36

似乎在向量空間上取一個多項式，並計算附加到每個變量的所有（轉置）（矩陣）係數的和。 args是一個數組，這樣args.(i)是i變量上的所有係數的總和，而const是常量標量的總和。

我不知道這個操作有什麼意義，但是我懷疑它在一般情況下並沒有多大意義（工作在任意產品總和......的產品總和上;這會導致奇怪的，線性/同質行爲）。我想對這個多項式類型的實際值的形狀有什麼隱含的限制，例如它可能對所有變量都是線性的。

來源

2013-05-06 06:19:59 gasche

理解語義的代碼

回答

相關問題