[Agda] proof run time cost

[Andreas Abel]

Hi Serge,

you can make your stuff work if you avoid matching on the proof of (n <= 
m).  Here is your program where I do not match on p, but use an 
inversion lemma (inv<=) in the recursive call.  Since evaluation is 
lazy, your postulate is never evaluated.

   module ProofIrrelevance where

   open import Prelude
   open import Data.Nat using (_≤_; z≤n; s≤s)

   inv≤ : ∀ {m n} → suc m ≤ suc n → m ≤ n
   inv≤ (s≤s p) = p

   proofLength : (n : ℕ) -> (m : ℕ) -> n ≤ m -> ℕ
   proofLength 0       _       p  = 1
   proofLength (suc n) 0       ()
   proofLength (suc n) (suc m) p  = suc (proofLength n m (inv≤ p))

   f : ℕ -> ℕ
   f n = proofLength (n ⊓ 4) 4 p
         where
         postulate p : (n ⊓ 4) ≤ 4

   main : _
   main = run $ putStrLn $ show $ f 5

You can go one step further and make the proof argument to proofLength 
irrelevant, changing the type signature to

   proofLength : (n : ℕ) -> (m : ℕ) -> .(n ≤ m) -> ℕ

This will allow the code generator to perform extra optimizations.

Cheers,
Andreas

On 06.10.12 2:59 PM, Serge D. Mechveliani wrote:
> People,
> I have a beginner question about usage of `postulate' and about a
> particular run time cost of proofs.
> I am trying to find out what cost may present a verified programming.
> It is actually about using Agda, about what it is for.
>
> First, consider a contrived program
>
>    lemma4 : (n : Nat) -> (min n 4) <= 4
>    lemma4 n =  some silly implementation which running cost is O(n^4).
>
>    proofLength : (n : Nat) -> (m : Nat) -> n <= m -> Nat
>    proofLength 0       _       z<=n     = 1
>    proofLength (suc n) 0       ()
>    proofLength (suc n) (suc m) (s<=s p) = suc $ proofLength n m p
>
>    f : Nat -> Nat
>    f n = proofLength (min n 4) 4 p
>          where
>          postulate p : (min n 4) <= 4
>
>    main : IO Unit
>    main = putStrLn $ toCostring $ show $ f 5
>
>
> (for this letter, I replace the math symbols:
>                              \bn -> Nat,  \<=  ->  <=,  \sqcap -> min ).
>
> The idea is as follows.
> Imagine that  lemma4  is difficult to implement for a small enough run
> time cost.
> (For example, sorting a list costs  O(n*(log n)),  and some proofs
> related to this sorting cost  O(n^2),  and I do not see how to make it
> smaller).
>
> f  does not use  lemma4,  because its running cost is not appropriate.
>
> Still  lemma4  is used as a verification for  f.
> Because as everything  is compiled,  it is verified by this that in  f,
> the type   (min n 4) <= 4   is not empty. So, f  is verified, despite its
> `postulate' clause.
> Right?
>
> Further,  f  boldly tries to analyse possible values of  p,  because it
> knows of which constructors are built the members of  (min n 4) <= 4.
> The compiler allows this.
> But at the run time Agda reports
>             MAlonzo Runtime Error: postulate evaluated: OrdListTest._.p
>
> I think, this is because the pattern required a concrete value of  p.
>
> So, if  f  somehow transmits  p,  whithout pattern matching against  p,
> everything must work.
> Right?
> And to analyse a value of  p,  f  needs to call  lemma4  and to spend
> O(n^4).
> Right?
>
> And my real example is sorting a list:
>
>    orderList : (xs : List Nat) -> OrderList xs       -- returns a record
>                                                      -- including proofs
>    orderList xs =  merge sort method of the cost  O(n*(log n)) where
>                    n = length  xs.
>                    Halve  xs,  order the halfs,  merge the results,
>                    process the proof parts respectively.
>
> The proof part for  ordered $ orderList xs  :  OrderedList? xs
> costs  O(n*(log n)).
> But for a full verification, one needs to add a proof for that  xs  and
> orderList xs  have the same multiset, that is the same element
> multiplicities. As  xs  is not ordered, the simplest definition for
> a multiplicity list check in it costs  O(n^2).
>
> With using the approach of the above code for  f,  I am going to add to
> orderList  a certain  multiplicityLemma  function. So  orderList  will
> be fully verified by just compiling the program.
> But if a client function needs to  analyse a proof  for the multiset
> part, one needs to call  multiplicityLemma  and thus to spend  O(n^2)
> at run time.
>
> The subject is totally new for me.
> Can you comment, please? Am I missing something?
>
> Thanks,
>
> -------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/