I was reading a book introducing formal verification algorithms with Haskell Discrete Mathematics with Haskell, and there I found a counter-example of inductively defined functions:
f91 :: Int -> Int
f91 x = if x > 100
then x - 10
else f91 . f91 $ x + 11
This recursive function is promised to return 91 if the argument ranges between 0 and 100: I hope somebody could explain to me how the algorithm of this recursive function works.
Have you seen McCarthy 91 function?
Suppose you start with a value x > 100
, then the result is simply x - 10
, so a value from 91
onwards.
Now suppose the value is from 90
to 100
. Then f91
takes the else
branch and x + 11
is between 101
and 111
. The first f91
application brings all the value to the range 91 - 101
; only 101
satisfies the then
branch of the second application of f91
, and for that the result (x - 10
) is 91
.
For all the other values we get the range 102 - 111
in the else
branch. However the else
branch applies f91 . f91
to that value; since all the values are > 100
, the first f91
brings the values down to 92 - 101
, of which only 101
passes the condition > 100
of the second f91
and becomes 91
.
The rest of the values go through the same cycle until all become 91
. Suppose you have a different interval of 11
values below 100
. The f91
first brings that interval above 100
and then keeps reducing the values to 91
starting from the higher end of the interval in the same manner. Please see the proof by induction linked in the wikipedia page.
Collected from the Internet
Please contact [email protected] to delete if infringement.
Comments