{-# OPTIONS --no-termination-check #-} {- Computer Aided Formal Reasoning (G53CFR, G54CFR) Peter Morris Lecture 17: Merge Sort (I) We started 3 lectures on implementing, and incrementally refining an implementation of Merge Sort. Our aim is to establish the correctness of the implementation, using techniques from earlier lectures: -} module l17i where open import Data.List open import Data.Nat open import Data.Product {- We will only consider sorting lists of natural numbers, for simplicity. We begin by defining a comparison function of two Natural Numbers, this returns an Order (a copy of the Booleans): -} data Order : Set where le gt : Order order : ℕ → ℕ → Order order zero n = le order (suc m) zero = gt order (suc m) (suc n) = order m n {- Now we can explain how to merge two sorted lists of Natural Numbers, using the comparison function above. Remember that naively we wanted to write merge: merge : List ℕ → List ℕ → List ℕ merge [] ns = ns merge (m ∷ ms) [] = m ∷ ms merge (m ∷ ms) (n ∷ ns) with order m n ... | le = m ∷ merge ms (n ∷ ns) ... | gt = n ∷ merge (m ∷ ms) ns But this doesn't pass Agda's termination checker, it analyses the definition to see any inductive argument gets smaller in all recursive calls, which is not the case. Instead we must tease this one function out into to mutually defined functions, one we call when ms gets smaller, the other when ms gets smaller: -} mutual merge : List ℕ → List ℕ → List ℕ merge [] ns = ns merge (m ∷ ms) [] = m ∷ ms merge (m ∷ ms) (n ∷ ns) with order m n ... | le = m ∷ merge ms (n ∷ ns) ... | gt = n ∷ merge' m ms ns merge' : ℕ → List ℕ → List ℕ → List ℕ merge' m ms [] = m ∷ ms merge' m ms (n ∷ ns) with order m n ... | le = m ∷ merge ms (n ∷ ns) ... | gt = n ∷ merge' m ms ns {- To sort efficiently, merge sort must split the list to be sorted into 2 lists of roughly the same size, to do this we 'deal' the input list out, as if it were a pack of cards: -} deal : List ℕ → (List ℕ × List ℕ) deal [] = [] , [] deal (n ∷ []) = [ n ] , [] deal (n ∷ n' ∷ ns) with deal ns ... | (xs , ys) = n ∷ xs , n' ∷ ys {- And now we can sort, by merging the result of sorting the two 'piles': -} sort : List ℕ → List ℕ sort ns with deal ns ... | (xs , []) = xs ... | (xs , ys) = merge (sort xs) (sort ys) {- However, Agda is again unconvinced that this terminates, it's is unable to see that in the 2 recursive calls that xs and ys are infact smaller than the input, ns. -} ex1 : List ℕ ex1 = 5 ∷ 2 ∷ 0 ∷ 1 ∷ 4 ∷ 3 ∷ [] ex2 : List ℕ ex2 = 100 ∷ 1 ∷ 10 ∷ 1 ∷ 100 ∷ 10 ∷ []