Induction proof of correctness of fibonacci function

Haskell implementation of the familiar Fibonacci function

fibSlow n

| n == 0 = 1 --fib.1

| n == 1 = 1 --fib.2

| otherwise = fibSlow(n-1) + fibSlow(n-2) --fib.3 开发者_C百科

What is the induction proof of correctness for fibSlow?

To prove correctness of a function on the natural numbers by induction, you would show that it's correct for certain base cases, and then that it's correct for higher values of the parameter given the assumption that it's correct for lower ones. So you'd verify first that fibSlow 0 = 1, and then that fibSlow 1 = 1, and then that for n > 1, fibSlow n is equal to the (n-1)th fibonacci number plus the (n-2)th fibonacci number. Here you get to assume that those numbers are fibSlow (n-1) and fibSlow (n-2), since fibSlow is correct for all inputs less than n by the inductive hypothesis.

This might seem all rather trivial... because it is! The whole point of such an example in Haskell is that you can write code that's obviously correct. When you go to prove it correct, the proof just writes itself and amounts to looking at the code and noting that it clearly says exactly what you're trying to prove. This is one of the nice properties of a declarative language like Haskell.

Apologies I haven't formally seen this kind of material for a while, so you're probably best looking at other sources if this is homework.

I think you want to show the existence of a monotone function which describes the "progress" of the recursion. This case should be pretty simple: the argument itself is monotonically decreasing. For a nonnegative n, the recursive call will be made with a lesser n', and that n' will never be less than zero.

You can also use power induction to argue the function is defined on all n. You have declared it defined on 0 and 1, and it suffices to say that if it's defined on n and n+1, then it's defined on n+2. This is obvious by the definition of the recursive call.

I think you might be able to read up on some formalities in Jech's Set Theory book, in the Ordinals chapter.