Commit 5f67db56 by Jean-Christophe Filliâtre

fibonacci: documentation

parent e424e301
 ... @@ -86,6 +86,11 @@ module FibonacciLogarithmic ... @@ -86,6 +86,11 @@ module FibonacciLogarithmic logic m1110 : t = {| a11 = 1; a12 = 1; logic m1110 : t = {| a11 = 1; a12 = 1; a21 = 1; a22 = 0 |} a21 = 1; a22 = 0 |} (* computes ((1 1) (1 0))^n in O(log(n)) time since it is a matrix of the shape ((a+b b) (b a)), we only return the pair (a, b) *) let rec logfib n = let rec logfib n = { n >= 0 } { n >= 0 } if n = 0 then if n = 0 then ... @@ -101,6 +106,14 @@ module FibonacciLogarithmic ... @@ -101,6 +106,14 @@ module FibonacciLogarithmic { let a, b = result in { let a, b = result in power m1110 n = {| a11 = a+b; a12 = b; a21 = b; a22 = a |} } power m1110 n = {| a11 = a+b; a12 = b; a21 = b; a22 = a |} } (* by induction, we easily prove that (1 1)^n = (F(n+1) F(n) ) (1 0) (F(n) F(n-1)) thus, we can compute F(n) in O(log(n)) using funtion logfib above *) logic p (n:int) = logic p (n:int) = let p = power m1110 n in let p = power m1110 n in isfib (n+1) p.a11 and isfib n p.a21 isfib (n+1) p.a11 and isfib n p.a21 ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!