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.
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.
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 ?
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.)
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.
(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