These questions have to do more about how to think recursively in general, but I will take a specific example to illustrate.

Graham Hutton explains the function mSort in the video:

https://youtu.be/I9S61BYM9_4?t=2089

So, at the specific point I linked in the video, the professor says:

And here, I have two sorted lists:

msort :: [Int] -> [Int] 
msort []  = [] 
msort [x] = [x] 
msort xs  =      (msort ys) (msort zs)
    where
        (ys, zs) = halve xs

and highlights the expressions (msort ys) and (msort zs). Then, he adds the word merge in front of those expressions.

msort :: [Int] -> [Int] 
msort []  = msort [] 
msort [x] = msort [x] 
msort xs  = merge (msort ys) (msort zs)
    where
        (ys, zs) = halve xs

To me, it seems there are some assumptions, similar to assumptions in logic, like "if this hypothetical scenario is true, then (some statements are deduced)". Those are useful to think about recursion, but have nothing to do with the evaluation of the recursive function. So, my questions are:

• How can he speak about msort ys when msort at a point where it is not fully defined ?
• Everything written there doesn't have any magical meaning, of course. But are the chosen words only helpful to reason about the function? I am asking since he speaks about msort ys is a "sorted list". He uses the past tense.
• Does this assume halve is going to be defined in a sensible way ? Again, halve is just a name.

I apologize if these are really basic questions. It's something I've just started wondering recently.

CodePudding user response：

These questions are "basic" but in the sense that they are fundamental to understanding functional languages and the concept of recursive programs, not in the sense that they are easy or obvious to answer.

The similarity to assumptions in logic is not entirely coincidental. The definition of msort given by Hutton is related to proof by induction in mathematical logic. In a usual sort of mathematical inductive proof, we prove that something holds for a small "base case" (e.g., holds for n=0), and then we prove that if something holds for any arbitrary sized case (e.g., any particular n), it holds for a "slightly bigger" case (e.g., for n 1). From this, we are able to conclude that it holds for all cases (e.g., for all values of n>=0).

Here, we prove a property for a couple of small cases (e.g., it's easy to sort the empty list, and it's easy to sort the one-element list), and then we prove that if we can sort two lists of roughly length n/2 (e.g., msort ys and msort zs), then we can sort a list of length n (msort xs), and we conclude by induction that lists of any size can be sorted. There are lots of details to fill in here, like what it means to take half the length of an odd-length list to get two lists that are "roughly" half the length, etc., but this is the general idea.

It's maybe worth pointing out that, even though part of the mathematical proof takes the form "if we assume that lists of size 15 can be sorted, then we can sort a list of size 30", it is not necessary that we assume lists of size 15 can be sorted in order to use this proof. The proof works because the premises "a list of size 1 can be sorted" and "assuming a list of size n can be sorted, then a list of size n*2 can be sorted" allows us to conclude that all lists of size equal to powers of two can be sorted (and with some minor modifications to this proof, we can show that lists of any size can be sorted too). The "assumption" is part of the formal structure of the valid proof, not an assumption we need to make for the proof to be valid.

In a way, this is true of the recursive function msort. The magic of modern functional languages is that msort can be used within msort before it is "fully defined". That's because we don't need to show we can define msort for, say a list of size 15. We only need to show that we can define msort for a list of size 30 in terms of msort for a list of size 15, and as long as we add a couple of base cases that don't depend on msort (e.g., lists of size zero or one are sorted directly), the definition of msort -- like the mathematical proof of induction -- works fine.

When Sutton talks about msort ys being sorted in the past tense, he's running up against difficulties with matching English tenses to the meaning of recursive functions. At compile time, msort ys is just a reference to a function that is in the process of being defined, but that's the magic of recursive functions -- part of the process of defining them involves calling the function that's in the middle of being defined. At runtime, the tenses are accurate. When you run msort [4,3,2,1], it will invoke msort [4,3] which will sort the list into [3,4] and msort [2,1], which will sort the list into [1,2], and these sorted (past tense) values will be available to be merged into a final result [1,2,3,4].

I'm not sure I understand why you aren't sure you understand halve -- yes, this assumes that halve is going to be defined in some sensible way that matches its name. But, since halve doesn't depend on msort or on halve, it doesn't pose the same philosophical questions as msort. If it helps, pretend halve is defined as:

halve xs = (take n xs, drop n xs) where n = length xs `div` 2