[Agda] proof overhead
Serge D. Mechveliani
mechvel at botik.ru
Sat Dec 22 10:57:42 CET 2012
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
More information about the Agda
mailing list