Email Gateway (Aug 22 2022 at 18:49): Email Gateway (Aug 22 2022 at 18:49):From: Christian Sternagel <c.sternagel@gmail.com>
Dear José,
I am guessing your question is how to speed up computations?
First of all, your Isabelle/HOL implementation of "Fib" below is
unnecessarily inefficient (that is, quadratic) as is, due to the nested
use of "(@)". For lists it is only efficient to traverse them from left
to right, so iterated appending is one of the worst things you can do
with them ;)
(I don't know SAGE, but I it might use arrays rather than lists
internally? Otherwise, it should also be really slow.)
A possible implementation of Fibonacci numbers with linear complexity
would be:
fun fibacc :: "nat ⇒ nat ⇒ nat ⇒ nat list"
where
"fibacc x y 0 = []"
| "fibacc x y (Suc 0) = [x]"
| "fibacc x y (Suc n) = x # fibacc y (x + y) n"
definition "fib = fibacc 0 1"
where "fibacc" uses two accumulating variables "x" and "y" (hence the
name) to maintain a "window" on the current and next Fibonacci number.
At this point 'value "fib 40"' will probably still be too slow. But now
the problem is the default implementation of natural numbers (in unary
representation). So
import "~~/src/HOL/Library/Code_Binary_Nat"
should do the trick.
hope this helps,
chris
Email Gateway (Aug 22 2022 at 18:49):From: Dominique Unruh <unruh@ut.ee>
Hi,
one thing that might help is to import the theory HOL.Code_Target_Numeral
(see https://isabelle.in.tum.de/dist/Isabelle2018/doc/codegen.pdf, p.40.)
to speed up integer operations.
Additionally, I am noticing that you are using random access to your list
in SumLast2, each of those has O(n) complexity, so has the @. So your
routine is unnecessarily slow. Of course, the same problem might occur in
Python, but Python implements lists differently, and possibly with O(1)
lookups (not sure). At least for the Isabelle code generation, it would
much much faster to just generate the reversed list (i.e., (λ L. SumLast2 L
square-root of the time.
Finally, I think there is some overhead when calling "value" because a lot
of code is compiled at this moment (for all functions that are indirectly
used by your command). This won't matter so match for complex computations
but is probably in the way when computing very fast computations.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:50):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi José,
the hints already given should help you to get a reasonable speedup for
casual evaluation. What to do if this is not enough depends on your
application. The tutorial on code generation gives some hints on that.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 18:50):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Thank you all for the proposals in order to improve the speed of
computation in Isabelle. The only strange experience that I have not
understood yet is that the exponential algorithm
fun fib :: ‹nat ⇒ nat› where
‹fib 0 = 0›
| ‹fib (Suc 0) = 1›
| ‹fib (Suc (Suc n)) = fib (Suc n) + fib n›
value ‹fib 25›
seems to be faster in Isabelle than the linear algorithm
fun fibL :: ‹nat ⇒ nat*nat› where
‹fibL 0 = (1,0)›
| ‹fibL (Suc n) = (λ x. (snd x, snd x + fst x)) (fibL n)›
value ‹fibL 25›
By the way, in SAGE the above-mentioned exponential algorithm runs in
exponential time and the above-mentioned linear algorithm runs in linear
time. On the other hand, both algorithms in Isabelle run as if they were
both exponentials, the linear one is even worst. I know that I am doing
something that I think is linear, but Isabelle interpreted it as
exponential in the case of fibL. Is there a way to fix the definition of
fibL to make it linear as it should be?
Link: https://github.com/josephcmac/miscellany/blob/master/FiboSum.thy
Kind Regards,
José M.
El mié., 19 dic. 2018 a las 8:37, Florian Haftmann (<
florian.haftmann@informatik.tu-muenchen.de>) escribió:
Email Gateway (Aug 22 2022 at 18:50):From: Dominique Unruh <unruh@ut.ee>
Hi,
your fibL does indeed look linear. Perhaps it's not exponential, but the
overhead for compilation is big? How about value "fib 0"? One thing that
can help to understand what's going on is the command *declare
[[ML-source-trace]]* which shows you what ML code Isabelle is actually
executing.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:50):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear José,
Isabelle beta-reduces all definitions before they executed. So your fibL actually looks
like this:
fun fibL :: ‹nat ⇒ nat*nat› where
‹fibL 0 = (1,0)›
| ‹fibL (Suc n) = (snd (fibL n), snd (fibL n) + fst (fibL n))›
And clearly, this is even worse than the plain fib.
If you want to share results, you must use explict let bindings:
fun fibL :: ‹nat ⇒ nat*nat› where
‹fibL 0 = (1,0)›
| ‹fibL (Suc n) = (let x = fibL n in (snd x, snd x + fst x))›
Best,
Andreas
Email Gateway (Aug 22 2022 at 18:50):From: Dominic Mulligan <Dominic.Mulligan@arm.com>
Hi Jose,
The following appears to be faster than your original:
theory Scratch
imports Main "HOL-Library.Code_Target_Nat"
begin
text‹I have included the @{theory "HOL-Library.Code_Target_Nat"} theory above which maps HOL's
@{type nat} type onto machine integers in the code generator target languages. Try removing
the inclusion of this theory above to see the effect it has on @{command value}'s performance,
below.}›
text‹Computes the nth Fibonacci number›
fun fib :: ‹nat ⇒ nat› where
‹fib 0 = 0› |
‹fib (Suc 0) = 1› |
‹fib (Suc (Suc m)) = fib (Suc m) + fib m›
text‹Computes the sequence of Fibonacci numbers upto a limit›
definition fibs :: ‹nat ⇒ nat list› where
‹fibs limit ≡ map fib (upt 0 limit)›
text‹@{command value} takes an optional command telling it which evaluator to use. By default it
uses the code simplifier. You can also try the code evaluation evaluator (the normalization by
evaluation evaluator does not terminate, here):›
value ‹fib 40›
value [code] ‹fib 40›
value ‹fibs 40›
value [code] ‹fibs 40›
end
Without SAGE on my machine it's hard to say whether this is "as fast" as SAGE.
Thanks,
Dominic
Email Gateway (Aug 22 2022 at 18:51):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Thank you. Problem solved using "led" in place of "lambda". Right now, the
algorithm is running really fast.
Kind Regards,
José M.
El jue., 20 dic. 2018 a las 1:52, Andreas Lochbihler (<
mail@andreas-lochbihler.de>) escribió:
Last updated: Apr 24 2024 at 04:17 UTC