The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Tue, Apr 16, 2024 at 6:34 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Hi everyone,

I am wondering if the performance of an OCaml code --extracted from a Coq formalisation-- would be different if a matrix data structure is modelled as a function type compared to a list of lists?

For OCaml-related questions, I suggest using https://discuss.ocaml.org/ , there's a lot of experts there willing to help.

 

During formalisations if it involves matrices, I assume them as a function type (A -> B -> C for finite type A and B) than a list of lists. Function type is nice for reasoning about correctness proofs, but when I extract OCaml code from the formlisation and need to call an OCaml function from main.ml, I create a function type (see the definition of mat below) at main.ml and pass it to the OCaml function. Another way I can achieve the same functionality is to create the matrix as a list of lists in main.ml and then use a search function that turns the list of lists into a function type (see the example fnmat). Below I have provided an OCaml code but it can also be implemented in Coq, although it may require some effort. Now the question is does it matter to the OCaml compiler?  I would also appreciate it if you know of any formalisations about matrix multiplication in Coq and could post them here.

For a n * n matrix, the List.assoc based solution takes time O(n) for each access, and the pattern-matching-based solution is constant-time.

However, if n >= 100 or so, the OCaml pattern-matching compiler may take a very long time, or run out of space, to compile your code.

A third solution is to use OCaml matrixes (arrays of arrays):

let rank (n : coq_Node) : int =

  match n with A -> 0 | B -> 1 | ...

let matrix : coq_RR array array =
  [| [| oneRR; (Left 3, Left 5); (Left 5, Left 4) |];
     [| ... |];
     ...
  |]

let mat (x : coq_Node) (y : coq_Node) : coq_RR = 
  matrix.(rank y).(rank x)

Note, however, that your source OCaml code still has size quadratic in n, so for large enough n it can fail to type-check and compile. At this point you should consider reading the matrix off a file in order to fill the "matrix" array of arrays.

Hope this helps,

- Xavier Leroy

Best,

Mukesh

(* function type *)
let mat (x : coq_Node) (y : coq_Node) : coq_RR = 
  match x, y with
  | A, A -> oneRR
  | A, B -> (Left 3, Left 5) 
  | B, A -> zeroRR 
  | A, C -> (Left 5, Left 4)
  | C, A -> zeroRR 
  | B, B -> oneRR
  | B, C -> (Left 2, Left 10) 
  | C, B -> zeroRR 
  | C, C -> oneRR  

(* Another way to encode the matrix mat *)
let listmat : (coq_Node * ((coq_Node * coq_RR) list)) list =
  [(A, [(A, oneRR); (B, (Left 3, Left 5)); (C, (Left 5, Left 4))]);
   (B, [(A, zeroRR); (B, oneRR); (C,  (Left 2, Left 10))]);
   (C, [(A, zeroRR); (B, zeroRR); (C, oneRR)])]

(* turn it into a function type *)
let fnmat : coq_Node -> coq_Node -> coq_RR = 
  fun (x : coq_Node) -> fun (y : coq_Node) -> List.assoc y (List.assoc x listmat)