How to write a non-recursive fibonacci function, and satisfying the specification

Learn
#1

Hello, community.

I have the following specification:

problem nonRecursiveFibonacci (in n: ℤ) : ℤ {
  requires: {n ≥ 0}
  ensures: {(∃l : seq(ℤ))(length l = n + 1 ∧ isFibonacciSequence(l) ∧ l !! (length (n-1)) = result)
}

predicate isFibonacciSequence (l: seq(ℤ)) {
  (length l > 0 ⇒ l !! 0 = 0) ∧ 
  (length l > 1 ⇒ l !! 1 = 1) ∧ 
  (∀i : ℤ)(2 ≤ i < length l ⇒ l !! i = l !! (i - 1) + l !! (i - 2))
}

In the specification, I can reference the output value with the name **result, **and : means “is of type”.

Then, I would have to implelment the function:

nonRecursiveFibonacci :: Int -> Int

In my attempts, any route I choose goes into recursion; any hints regarding a non-recursive definition ?

Is there any standard reference, of course perhaps not using that same notation, but using other kind of formalism, where I can see how can I derive a Haskell definition from a specification, or hints about using this one to think about the problem ?

As I do not have any experience so far with this kind of stuff, guidance would be greatly appreciated.

#2

I’ve made some progress; I could implement the predicate:

isFibonacciSequence :: [Int] -> Bool
isFibonacciSequence = go 0
    where 
      go 0 xs = xs !! 0 == 0
      go 1 xs = xs !! 1 == 1
      go i xs = xs !! i == xs !! (i - 1) + xs !! (i - 2)
#3

You can’t really implement this function without using recursion at some point. Haskell does not have a built-in notion of loops like many imperative languages do.

What is the reason that you don’t want to use recursion? If it is just about performance, then you probably want to use tail recursion with an accumulating parameter.

P.S. there is a bug in your isFibonacciSequence do test it with some inputs.

2 Likes
#4

Thank you so much, @jaror !

It’s an exercise a person is doing an used it as a challenge to learn. And with a list comprehension ? Filtering every list which is a fibonacci sequence ?

Thank you ! This is a false positive:

isFibonacciSequence [0,200]

gives True with my implementation…

#5

Is this better ?

isFibonacciSequence :: [Int] -> Bool
isFibonacciSequence xs = go (length xs - 1) xs
    where 
      go 0 xs = xs !! 0 == 0
      go 1 xs = xs !! 0 == 0 && xs !! 1 == 1
      go i xs = xs !! i == xs !! (i - 1) + xs !! (i - 2) && go (i - 1) xs
#6

I haven’t understood exactly what you want, but you could use $φ^n = φ ⋅ F_{n} + F_{n-1}$. The recursion is implicit in ^. (It would be necessary to define $ℤ[φ]$ and the prove that it’s a ring.)

#7

Thank you all for the help. I see now that it’s not possible to define without recursion. The person who gave me the exercise said that it wasn’t intended to be done in Haskell… so, it was his mistake.

But I learned from your suggestions.

#8

How about this, based on https://en.wikipedia.org/wiki/Fibonacci_sequence#Computation_by_rounding:

nonRecursiveFibonacci :: Int -> Int
nonRecursiveFibonacci n = round (phi ^ n / sqrt 5)
  where phi = (1 + sqrt 5)/2

Probably not what was asked for, but :man_shrugging:

1 Like
#9

Wow, Joachim. That’s impressive. That person’s mistake lead to this wonderful discovery for me :slight_smile:

Thank you very much.

And thanks to @JordGil too for the input.

#10

Note that this will give incorrect results:

> nonRecursiveFibonacci 80
23416728348467676

That should be 23416728348467685.

2 Likes
#11

Quite right, 64 bits are just too few.

I tried to use a arbitrary precision library like aern2-real to show off, but couldn’t quickly figure out how to round to Integer there.

#12 
data ℤφ = ℤφ !Integer !Integer
atφ (ℤφ aφ _) = aφ
instance Num ℤφ where
  (ℤφ aφ a1) * (ℤφ bφ b1) = ℤφ (aφ * bφ + aφ * b1 + a1 * bφ)
                               (aφ * bφ + a1 * b1)
  fromInteger a1 = ℤφ 0 a1
fib :: Int -> Integer
fib n
  | n >= 0    = atφ (ℤφ 1 0    ^ n)
  | otherwise = atφ (ℤφ 1 (-1) ^ (-n))
2 Likes
#13

I think it’s better to use Semigroup:

import Data.Semigroup

data ℤφ = ℤφ !Integer !Integer

atφ (ℤφ aφ _) = aφ

instance Semigroup ℤφ where
  ℤφ aφ a1 <> ℤφ bφ b1 = ℤφ (aφ * bφ + aφ * b1 + a1 * bφ)
                            (aφ * bφ + a1 * b1)

fib :: Int -> Integer
fib n = atφ (stimes n (ℤφ 1 0))
1 Like
#14

(I’ll assume you wrote fib n = atφ (stimes (n+1) (ℤφ 1 0)), so that it’s defined for n = 0 as well.).

That’s neat, but it’s a bit strange to define a complicated operation (here (<>)) and then only ever apply it only to the same argument. Let’s do some Bird-style derivation to specialize it to that argument

ℤφ aφ a1 <> ℤφ 1 0
  = ℤφ (aφ * 1 + aφ * 0 + a1 * 1) (aφ * 1 + a1 * 0)
  = ℤφ (aφ + a1) (aφ)

so we conclude

(<> (ℤφ 1 0)) = (\ (ℤφ x y) -> ℤφ (x + y) x)

And based on the the identity

stimes (n+1) x = iterate (<> x) x !! n

(it’s unfortunate that we don’t have a function iteration function that doesn’t go through lists) we can rewrite this as (using plain tuples)

fib :: Int -> Integer
fib n = fst (iterate (\(x,y) -> (x + y, x)) (1,0) !! n)

Not saying that it’s better, but it may be interesting to see the connection between the two.

#15

stimes is implemented more efficiently. It does the exponentiation by squaring trick.

#16

Excellent point, thanks!