The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Thanks for the replies and the links of the papers. 

Best,

Mukesh 

On Wed, 13 Jul 2022 at 02:56, Yao Li <liyao AT seas.upenn.edu> wrote:

Dear Mukesh,

You first definition is essentially using a writer monad. You can use monadic operations such as bind, ret, etc., so that the costs are hidden and you would not need to explicitly deal with them.

You might be interested in our paper “Reasoning about the Garden of Forking Paths” (https://dl.acm.org/doi/10.1145/3473585), which is essentially using a writer monad transformer to count computation costs. What we reason about in the paper is a lazy semantics, but call-by-value and call-by-need can also be reasoned about using similar methods.

Best,

Yao

On Jul 12, 2022, at 3:41 PM, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Hi everyone,

What are some nice ways to reason about the complexity/cost of Coq functions?

In more detail:

I want to reason about the complexity/cost of simple programs so the easiest way is to count the number of primitive instructions, during the execution of the program, and return it as an extra value. For example, the 'repeat_op_ntimes_rec' returns an extra argument, the number of steps it takes to execute for input n.

Fixpoint repeat_op_ntimes_rec (e : T) (n : positive) : T * N :=
      match n with
      | xH => (e, N0)
      | xO p =>
        let (ret, w) := repeat_op_ntimes_rec e p
        in (ret * ret, N.add 1 w)
      | xI p =>
        let (ret, w) := repeat_op_ntimes_rec e p
        in (e * (ret * ret), N.add 1 w)
      end.

Now, I can prove that the number of steps is bounded by a logarithm of n.

Lemma repeat_op_ntimes_rec_bound :
  forall n e, (snd (repeat_op_ntimes_rec e n) <= N.log2 (N.pos n))%N.

It is nice because if I compose two such functions, I can return the combined cost of functions. But now I am stuck with an extra return value just because I want to reason about the cost, so I can take another approach and write the same function in a normal way, without any counter:

(* Function without counter *)
 Fixpoint repeat_op_ntimes_rec_w (e : T) (n : positive) : T :=
      match n with
      | xH => e
      | xO p =>
        let ret := repeat_op_ntimes_rec_w e p
        in ret * ret
      | xI p =>
        let ret := repeat_op_ntimes_rec_w e p
        in e * (ret * ret)
      end.

Then I write an inductive data type to capture the cost

 (* Inducive Type to capture the complexity of  *)

Inductive complexity_repeat_op_ntimes_rec (e : T) :

     positive -> T -> N -> Prop :=

 | xH_case : complexity_repeat_op_ntimes_rec e xH e N0
 | xO_case p ret w : complexity_repeat_op_ntimes_rec e p ret w ->
      complexity_repeat_op_ntimes_rec e (xO p) (ret * ret) (N.succ w)
 | xI_case p ret w : complexity_repeat_op_ntimes_rec e p ret w ->
      complexity_repeat_op_ntimes_rec e (xI p) (e * (ret * ret)) (N.succ w).

Finally, I can prove that the execution of 'repeat_op_ntimes_rec' is bounded by logarithm of input by the following lemma

Lemma correct_complexity_repeat_op_ntimes_rec :
      forall n e,  complexity_repeat_op_ntimes_rec e n
        (repeat_op_ntimes_rec_w e n)  (N.log2 (N.pos n)).

This is nice because my function is free from an extra return value, but unfortunately, it does not, as I understand, compose. (I don't think I can compose two inductive datatypes to reason about combined cost).  Therefore, what is the best middle way to do this?

Best,

Mukesh