Email Gateway (Aug 22 2022 at 18:52): Email Gateway (Aug 22 2022 at 18:52):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
All my research in elementary number theory was motivated by empirical
data obtained in SAGE (a library of Python). It is more comfortable for me,
and maybe for other people looking for theorems from empirical data, to do
the computation directly in Isabelle/HOL, in order to combine both
algorithms with proofs. Nevertheless, it seems to me that computations in
SAGE are faster than in Isabelle/HOL. Is there a way to make computations
in Isabelle/HOL as fast as the computations in SAGE?
For example, in order to compute the list of Fibonacci numbers in
Isabelle/HOL I use the function:
fun SumLast2 :: ‹nat list ⇒ nat› where
‹SumLast2 L = (if length L < 2 then 0 else L!(length L - 1) + L!(length L -
2) )›
(* OEIS A000045 *)
fun Fib :: ‹nat ⇒ nat list› where
‹Fib 0 = [0]›
| ‹Fib (Suc 0) = [0, 1]›
| ‹Fib (Suc (Suc n)) = (λ L. L @ [(SumLast2 L)] ) ( Fib (Suc n) )›
value ‹Fib 40›
Link:
https://raw.githubusercontent.com/josephcmac/miscellany/master/FiboElem.thy
On the other hand, the corresponding function in SAGE is:
def SumLast2(X):
return X+[X[len(X)-1]+X[len(X)-2]]
def Fib(n):
return [0] if n == 0 else ([0,1] if n == 1 else SumLast2(Fib(n-1)))
print Fib(40)
Link: https://raw.githubusercontent.com/josephcmac/miscellany/master/Fib.py
Kind Regards,
José M.
Last updated: Apr 23 2024 at 16:19 UTC