[Agda] proof overhead

[Gabriel Scherer]

What about simply delaying the computation of the proofs by using

    record OrderList (xs : List Nat) : Set where
      field
        resList       : List Nat;
        ordProof      : IsOrdred resList;
        multisetProof : Unit -> multiset xs == multiset resList

The two types (evidence and delayed evidence) are isomorphic, you
should be able to do everything you want in such a setting, and the
dynamic semantics under a weak reduction strategy should make
multisetProof O(1), as long as you never need to compute on the proof.

There are more advanced strategies based on irrelevant types, squashed
types, or otherwise erasable values, but this is a simple first step
and I suppose it would work.

On Sat, Dec 22, 2012 at 10:57 AM, Serge D. Mechveliani <mechvel at botik.ru> wrote:
> People,
> I have certain beginner questions on the practice of the verified
> programming with dependent types.
>
> In DT programming, I see the two main new features for me:
> 1) a notion of a proof defined by each particular user program,
>    and even defining this individually for each statement,
> 2) evaluating proofs together with evaluating ordinary values.
>
> Consider the Agda function  orderList  for sorting  xs : List Nat
> non-decreasingly by `<'.  And let it return a record
>
> record OrderList (xs : List Nat) : Set where
>                        field
>                          resList       : List Nat;
>                          ordProof      : IsOrdred resList;
>                          multisetProof : multiset xs == multiset resList
>
> (for this letter I replace  \equiv  with  `=='),
>
> with  resList  standing for the resulting list,
> IsOrdered  and  multilset  reasonably defined
>
> I have programmed merge sorting, which evaluation cost is  O(n*(log n))
> -- together with  resList  and  ordProof.
> I can easily add the value for  multisetProof
> -- but with making the evaluation cost  O(n^2).
> To preserve  O(n*(log n))  looks like a certain problem.
> In particular, one also needs to think of a possible initial programmer's
> definition of a  multiset of a list  and of defining  the relation of
> multiset xs == multiset ys.
>
> I do not know, may be I manage to reasonably program this three fields,
> with preserving O(n*(log n)) -- may be, by using the AVL tree, or by
> other means.
> Still there may exist other problems, for which it is more difficult,
> -- may be impossible, -- to preserve the usual evaluation cost order.
>
> Question 1
> ----------
> Consider the two problem kinds.
> (I)  To solve algorithmically (say, in Agda) a given problem  P.
> (II) To solve P algorithmically (say, in Agda), with the algorithm
>      providing also the corresponding proof.
>
> For example,  (I):   to solve  P = sorting  as  resList  only,
>               (II):  to solve  P       with also returning the two proofs.
>
> Can you give a clear example of a simply formulated practical problem  P
> such that all known solutions for  P-II  have essentially greater
> evaluation cost order than for  P-I ?
> (O(n) -> O(n^2), O(n^3) -> O(2^n), and such).
>
> (Though, I doubt about correctness of this question, because, for example,
> the proof size depends on the constructor set which the programmer puts
> for representing a proof for P).
>
>
> Question 2
> ----------
> What do you think of the following way out?
>
> Step 1. Program the function   orderList   which
>         a) has evaluation cost  O(n*(log n)),
>         b) returns for  resList  the true value,
>         c) returns  p1 and p2  for the two proofs, with declaring
>            postulate p1 : IsOrdred resList,
>            postulate p2 : multiset xs == multiset resList.
>
> Step 2. Program  orderList-withProofs   which has evaluation cost  O(n^2)
>         and returns  a) resList,  b) ordProof,  c) multisetProof,
>                      d) the proof for  resList (orderList xs) == resList
>
> Step 3. Compile the whole program which includes the two sorting functions.
>
> Step 4. Use   orderList  instead of  orderList-withProofs  everywhere in
>         the program where the evaluation cost matters.
>
> To use this approach for all problems where the proof evaluation cost
> adds an essential overhead to evaluation-without-proof.
>
> It comes out that
> (1) the whole program with both sorting variants is veryfied
>     (because the types have been checked),
> (2) sorting has evaluation cost  O(n*(log n))  everywhere where the
>     programmer needed,
>
> (are (1) and (2) right?).
>
> But what to do with a client function which uses the result of  p2
> and also attempts to analyze the structure of the  p2  value,  to see
> its constructors?
> The programmer needs to estimate the cost: whether using the structure of
> p2  is essential for saving the total cost
> (for example, if  ys  is close to  xs,  then forming  p2 for ys  may be
> shorter when using the structure of  p2 for xs).
> If it worths, the programmer uses  orderList-withProofs,
> otherwise -- orderList.
>
> Are the above questions known?
> Am I missing something in this discourse?
>
> Thanks,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda