[Agda] proof run time cost
Andreas Abel
andreas.abel at ifi.lmu.de
Sat Oct 6 23:06:07 CEST 2012
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/
More information about the Agda
mailing list