Give the fool's fibonacci sequence
Recently I asked for tips on improving some code-golf of mine. The code was supposed to output every third value of the Fibonacci sequence starting with 2:
2,8,34,144,610,2584,10946,46368,196418,832040
However, I made a mistake in deriving my formula, and my code output a different sequence which is accurate for the first couple terms and then begins to diverge:
2,8,34,140,578,2384,9834,40564,167322,690184
My sequence is defined by:
\begin{array}{rcl} f(0) &=& 0 \\ f(1) &=& 2 \\ f(n) &=&\displaystyle 2 + 3f(n-1) + 4f(n-2) + 2\sum_{0}^{n-3}f\\ \end{array}or in terms of my original Haskell code:
z=zipWith(+)
g=z((*2)<$>0:0:g)$z(0:g)$(*2)<$>scanl(+)1g
Your task is to implement a sequence of integers, which has my incorrect sequence as every third value. The other values can be whatever you want them to be, it simply must have the above sequence as every third value. The sequence can begin at the 0th, 1st, or 2nd index, whichever you please.
This is code-golf so the goal is to minimize the size of your program as measured in bytes.
2 answers
Lean 4, 115 109 104 89 bytes
Note: had to update bytecount to take into account non-printable characters.
For anyone who isn't familiar with Lean, it's basically an interactive theorem prover that can also be used for regular math computation. Those who are familiar with Haskell would probably be able to recognize some of the syntax used, such as the <$> functor that represents the mapping of a function onto a range.
Also you can shove most functions on one line for whatever reason, and you only need to import Mathlib if you are using List.Ico, whereas I can just use List.range for the same effect. xD
Something else to mention is that I forgot until now that I could simply omit the case where the input is 1. This is because since I am defining the function on Nat -> Nat, that means when I compute g(1), I actually compute$$\begin{align}g(1)&=2+3*g(1-1)+4*g(1-2)+2\sum_{n=0}^{1-2}g(n)\\&=2+3*g(0)+4*g(0)+2*\sum_{n=0}^0g(n)\\&=2+0+0+0=2\end{align}$$Since on the natural numbers, Lean defines $a-b=0$ when $a\le b$.
def g:Nat→Nat|0=>0|n=>2+(g (n-1))*3+(g (n-2))*4+2*((λx=>g x)<$>(List.range (n-2))).sum
Try it online! (ungolfed version) Link leads to the test case g(24) = 284925519302420. Not using TIO as that only supports Lean 3.
Hexdump:
00000000 64 65 66 20 67 3a 4e 61 74 e2 86 92 4e 61 74 7c |def g:Nat...Nat||
00000010 30 3d 3e 30 7c 6e 3d 3e 32 2b 28 67 20 28 6e 2d |0=>0|n=>2+(g (n-|
00000020 31 29 29 2a 33 2b 28 67 20 28 6e 2d 32 29 29 2a |1))*3+(g (n-2))*|
00000030 34 2b 32 2a 28 28 ce bb 78 3d 3e 67 20 78 29 3c |4+2*((..x=>g x)<|
00000040 24 3e 28 4c 69 73 74 2e 72 61 6e 67 65 20 28 6e |$>(List.range (n|
00000050 2d 32 29 29 29 2e 73 75 6d |-2))).sum|
Something to clarify about this: While I did not prove that this eventually terminates, or set a recursion depth using set_option diagnostics.threshold, neither of those things are actually needed.
This is because I can simply use #eval! instead of #eval to evaluate the function without needing to do either of those things.
0 comment threads
Python 3, 131 75 62 bytes
f=lambda n:n>0and 2+3*f(n-1)+4*f(n-2)+2*sum(map(f,range(n-2)))
I know, a one-liner is boring. This is because I apparently didn't need a separate function/lambda to compute the sum of something. So there you have it, a 56 69 (nice) byte save in total. :D
0 comment threads
1 comment thread