How to use equational reasoning to reduce this expression-CodePudding

I have the following definitions:

fibs = 1 : scanl ( ) 1 fibs

scanl :: (a -> b -> a) -> a -> [b] -> [a] 
scanl f q ls =
    q : (case ls of 
            [] ->[]
            x:xs -> scanl f (f q x) xs
        )

take                   :: Int -> [a] -> [a]
take n _      | n <= 0 =  []
take _ []              =  []
take n (x:xs)          =  x : take (n-1) xs

I would like to reduce the following expression:

take 3 (fibs)

So, I would proceed:

take 3 (fibs)
= 
take 3 (1 : scanl ( ) 1 fibs)
= 
1 : take 2 (scanl ( ) 1 fibs)
= 
1 : take 2 (scanl ( ) 1 (1 : (scanl ( ) 1 fibs)))
=
...

How can I continue reasoning ?

EDIT: I continued my reasoning but the last line is incorrect, because the next computed Fibonacci number should be 5. How can I solve this problem ?

take 3 (fibs)
= 
take 3 (1 : scanl ( ) 1 fibs)
= 
1 : take 2 (scanl ( ) 1 fibs)
= 
1 : take 2 (scanl ( ) 1 (1 : (scanl ( ) 1 fibs)))
= 
1 : take 2 (1 : scanl ( ) 2 (scanl ( ) 1 fibs))
= 
1 : 1 : take 1 (scanl ( ) 2 (scanl ( ) 1 fibs))
= 
1 : 1 : take 1 (scanl ( ) 2 (1 : scanl ( ) 1 fibs))
= 
1 : 1 : take 1 (2 : scanl ( ) 3 (scanl ( ) 1 fibs))
= 
1 : 1 : 2 : take 0 (scanl ( ) 3 (1 : scanl ( ) 1 fibs))
= 
1 : 1 : 2 : take 0 (3 : scanl ( ) 4 (1 : scanl ( ) 1 fibs))
= 
...

CodePudding user response：

With equational reasoning, you can typically expand terms in any order you want, and it will usually result in the same result. You've found the exception -- if you pick a particularly bad order of expansion, like continually expanding the fibs term while ignoring the scanl term, your solution may appear to loop indefinitely without producing any results, whereas Haskell has no problem evaluating it.

If you want to expand your program the same way Haskell actually evaluates it, you need to understand that terms are evaluated when and only when the evaluation is required for pattern matching, either in an explicit case statement or in the implicit case statement of a function definition with patterns.

So, when Haskell evaluates take 3 fibs the reason it needs to evaluate/expand the fibs term is because the pattern matches in the definition of take require pattern matching on the second argument whenever the first argument is positive. In detail, Haskell first tries to match the pattern:

take n _ | n <= 0 = ...

This requires evaluation of n, which is already evaluated as 3. Because the guard fails, Haskell next tries to match the pattern:

take _ [] = ...

and this requires evaluating the second argument because that's the only way Haskell can tell if it is or isn't an empty list.

In your (pre-edit) expansion, you actually followed this rule -- even if you didn't realize you were following it -- up to this term.

1 : take 2 (scanl ( ) 1 fibs)

When Haskell tries to evaluate the take here, because 2 is positive, it needs to evaluate the second argument. But evaluation of the second argument doesn't immediately start by expanding fibs. That's only going to happen if scanl pattern matches on its third argument, so we need to see what scanl is doing first. From the code, the definition:

scanl f q ls = ...

can be applied with no pattern matching at all, so the correct expansion (meaning the expansion that matches how Haskell would actually try to evaluate it) is:

1 : take 2 (scanl ( ) 1 fibs)
=
1 : take 2 (1 : (case fibs of { [] -> []; x:xs -> scanl ( ) (( ) 1 x) xs }))

Now, take has enough information about its second argument to continue so the expansion would continue by applying the definition of take:

1 : 1 : take 1 (case fibs of { [] -> []; x:xs -> scanl ( ) (( ) 1 x) xs })

This next take also needs to expand its second argument to make progress. The case statement needs to expand fibs to pattern match, so the next part of the expansion should be:

1 : 1 : take 1 (case (1 : scanl ( ) 1 fibs) of { [] -> []; x:xs -> scanl ( ) (( ) 1 x) xs })

which is enough information for the case to proceed (by applying the second case with x=1 and xs=scanl ( ) 1 fibs):

1 : 1 : take 1 (scanl ( ) (( ) 1 1) (scanl ( ) 1 fibs))

For take to progress, it needs to inspect its second argument, which is a scanl. This scanl can proceed without further evaluation by direct application of the definition:

1 : 1 : take 1 ((( ) 1 1) : case scanl ( ) 1 fibs of { [] -> []; x:xs -> scanl ( ) (( ) (( ) 1 1) x) xs })

Now, take as enough information to proceed:

1 : 1 : (( ) 1 1) : take 0 (case scanl ( ) 1 fibs of { [] -> []; x:xs -> scanl ( ) (( ) (( ) 1 1) x) xs })

At this point, assuming all list elements have been demanded in order, Haskell's next order of business will be to evaluate the third element:

1 : 1 : 2 : take 0 (case scanl ( ) 1 fibs of { [] -> []; x:xs -> scanl ( ) (( ) (( ) 1 1) x) xs })

and the last order of business is to evaluate take which requires no further evaluation of its second argument when its first argument is zero, so we just get:

1 : 1 : 2 : []

which is the final answer.

As I say, this is how Haskell would actually evaluate your program. (Well, it might do it a little differently because of optimizations, but the answer is guaranteed to be the same.)

Your alternate order in the edit will also work, though you're doing more evaluation than Haskell will. The reason you're getting the wrong answer is that this step:

1 : 1 : take 1 (scanl ( ) 2 (scanl ( ) 1 fibs))
=
1 : 1 : take 1 (scanl ( ) 2 (1 : scanl ( ) 1 fibs))

is incorrect. If you want to expand that second scanl following your approach, you'll need to expand fibs again first:

1 : 1 : take 1 (scanl ( ) 2 (scanl ( ) 1 fibs))
=
1 : 1 : take 1 (scanl ( ) 2 (scanl ( ) 1 (1 : scanl ( ) 1 fibs)))

and now you can apply the definition of scanl to the second occurrence:

1 : 1 : take 1 (scanl ( ) 2 (1 : scanl ( ) (1   1) (scanl ( ) 1 fibs)))

and to the first occurrence:

1 : 1 : take 1 (2 : scanl ( ) (2   1) (scanl ( ) (1   1) (scanl ( ) 1 fibs))
=
1 : 1 : 2 : take 0 (scanl ( ) (2   1) (scanl ( ) (1   1) (scanl ( ) 1 fibs))

No more evaluation is necessary but if you really want to go further, you'll have to expand fibs again before expanding the scanl occurrences from second-last to first:

1 : 1 : 2 : take 0 (scanl ( ) (2   1) (scanl ( ) (1   1) (scanl ( ) 1 (1 : scanl ( ) 1 fibs))))
=
1 : 1 : 2 : take 0 (scanl ( ) (2   1) (scanl ( ) (1   1) (1 : scanl ( ) (1   1) (scanl ( ) 1 fibs))))
=
1 : 1 : 2 : take 0 (scanl ( ) (2   1) (2 : scanl ( ) (2   1) (scanl ( ) (1   1) (scanl ( ) 1 fibs))))
=
1 : 1 : 2 : take 0 (3 : scanl ( ) (3   2) (scanl ( ) (2   1) (scanl ( ) (1   1) (scanl ( ) 1 fibs))))
=
1 : 1 : 2 : take 0 (3 : scanl ( ) 5 (scanl ( ) 3 (scanl ( ) 2 (scanl ( ) 1 fibs))))

and you can see that 5, not 4, is slowly making its way into the calculation.