On 26/08/04 10:43, Philip Clayton wrote:
Rob and others who are interested in efficiency,

For v_%exists%_intro the manual states
"If the functionality is sufficient, this is superior in efficiency to
both %exists%_intro and simple_%exists%_intro."

However this doesn't seem to be the case anymore - see test below. It
looks like simple_%exists%_intro has undergone an enhancement but no
corresponding modification was made to v_%exists%_intro.
(v_%exists%_intro follows precisely the `old style imlementation' of
simple_%exists%_intro without the costly initial term_match but with a
more general %beta%_conv for pair quantification.)

Well, nearly 7 years on, v_%exists%_intro is still slower than simple_%exists%_intro, though not as much as it was.

It looks to be a simple fix to base v_%exists%_intro on the new
implementation of simple_%exists%_intro - see attachment - given the
availability of simple_%exists%_intro_thm from imp007. Any improvement
would have knock-on effects in some other functions e.g.

A patch for this is attached. It is relative to 2.9.1w2.rda.110226 rather than the latest working release 2.9.1w2 to make it easier to apply. Most of the changes relate to exposing the theorem simple_%exists%_intro_thm, which I renamed to %exists%_intro_thm as it is not limited to simple quantification.

See following tests for performance improvement.

(* test values *)
val tm = %<%%exists% b c x y %spot% f (x + y + z) (y * 234 - a) %or% g b (c - 100)%>%;
val v = %<%a : %bbN%%>%;
val thm = asm_rule tm;
val %exists%_tm = mk_%exists% (v, tm);

PolyML.timing true;

(* test simple_%exists%_intro *)
val c = ref 500000;
while !c > 0 do (
   simple_%exists%_intro %exists%_tm thm;
   c := !c - 1
(* ~3.5s *)

(* test v_%exists%_intro *)
val c = ref 500000;
while !c > 0 do (
   v_%exists%_intro v thm;
   c := !c - 1
(* ProofPower 2.9.1w2.rda.110226:            ~5.0s *)
(* ProofPower 2.9.1w2.rda.110226.pbc.110704: ~1.1s *)

Note that my computer is just over 10 times faster than the one I was using 7 years ago for the above tests! More interestingly, that is significantly less than 2^(7/1.5) times... I suppose that begs the question: where does concurrency feature on the ProofPower roadmap?


Attachment: patch-2.9.1w2.rda.110226.pbc.110704.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to