Logic for Computer Science - How to define msort, merge and split functions inductively?

In "Modelling Computing Systems: Mathematics for Computer Science", I came across a logic exercise to inductively define a merge sort function 'mergeSort', with a hint to first define auxillary functions 'split' and 'merge'. The style of the logic so far looks like this for inductively defined sets Odd and Even, and some other functions that manipulate lists (isort, insert, length, append):

1 ∈ Odd;
if n ∈ Odd then (n+2) ∈ Odd;
0 ∈ Even;
if n ∈ Even then (n+2) ∈ Even;

isort([]) = [];
isort(a:L) = (insert a)(isort(L));

(insert a)[] = [a];
(insert a)(b:L) = if a < b then a:(b:L) else b:((insert a)L);

length([]) = 0;
length(n:L) = 1 + length(L);

L1 ++ [] = L1;
(a:L1) ++ L2 = a:(L1 ++ L2);


I have tried, but I can't figure out how to define the first auxillary function 'split', which should split a list in roughly the same size. So far, I've defined the base cases for empty list and list with single element, but I don't know how to define the inductive case. I am not sure about the logic, the notation and also not about how I could make sure that the function doesn't use the same tail of the list L?

split([]) = ([],[]);
split(a:[]) = ([a],[]);
split(a : b : L) = if length(a : b : L) ∈ Even
(a : (split(L)), b : (split(L)));
else
(a : (split(L)), b : (split(b : L)));


How can I inductively call the split function again, without repeating the same split?

I have defined the merge function like this, and am pretty sure that should work:

merge(L1,[]) = L1;
merge([],L2) = L2;
merge(a:L1, b:L2) = if a < b
(a:(merge(L1, b:L2)));
else
(b:(merge(a:L1, L2)));


As for the final function mergeSort, I've gotten this far:

mergeSort([]) = [];
mergeSort(a:[]) = [a];
mergeSort(L) = merge("firstResultOf"(split(L)), "secondResultOf"(split(L)));


I don't know how to make it clear in the function that merge should use the first and second output lists of split. And I am unsure how to call mergeSort inductively..

How would you do it, using this type of notation?

• merge("firstResultOf"(split(L)), "secondResultOf"(split(L))) is the same thing as merge(split(L)). But that won't work, you don't have any recursive calls to mergeSort. Jan 28, 2023 at 23:58

You can avoid odd and even by considering one more case in split. Any you need recursive calls in mergeSort. Here's a working Haskell solution.

    split :: [a] -> ([a], [a])
split [] = ([], [])
split [x] = ([x], [])
split [x,y] = ([x], [y])
split (x : y : l) = (x:xs, y:ys) where (xs,ys) = split l

merge :: Ord a => ([a], [a]) -> [a]
merge (xs, []) = xs
merge ([], ys) = ys
merge (x:xs, y:ys) | x <= y    = x : merge (xs, y:ys)
| otherwise = y : merge (x:xs, ys)

mergeSort :: Ord a => [a] -> [a]
mergeSort [] = []
mergeSort [x] = [x]
mergeSort xs = merge (mergeSort ys, mergeSort zs) where (ys, zs) = split xs