From 5f67db56d8b13c4da00540780977bdeae283e179 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Fri, 8 Apr 2011 14:09:13 +0200 Subject: [PATCH] fibonacci: documentation --- examples/programs/fibonacci.mlw | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/examples/programs/fibonacci.mlw b/examples/programs/fibonacci.mlw index 97cc74085..97f5ce456 100644 --- a/examples/programs/fibonacci.mlw +++ b/examples/programs/fibonacci.mlw @@ -86,6 +86,11 @@ module FibonacciLogarithmic logic m1110 : t = {| a11 = 1; a12 = 1; 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 = { n >= 0 } if n = 0 then @@ -101,6 +106,14 @@ module FibonacciLogarithmic { let a, b = result in 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) = let p = power m1110 n in isfib (n+1) p.a11 and isfib n p.a21 -- GitLab