{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Peter Morris Lecture 17: Merge Sort (II) In Merge.agda, we wrote a naive sorting algorithm that we might write in Haskell, but Agda didn't beleive that it was terminating. If we want to verify this algorithm as 'correct' we must first prove it is terminating. To do this, we observe that sorting proceeds in 2 phases. In the 1st the input list is repeatedly 'dealt' in to two roughly even length lists until the constituent lists are of length 1 (which we know, trivially, to be sorted). We observed this 1st stage amounts to building a balance tree of numbers. The second stage amounts to repeatedly merging this tree back into a single list. We shall now see that by exposing the tree built from the 1st stage, we can show that our algorithm terminates. -} module l17ii where open import Data.List open import Data.Nat open import Data.Product 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 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 {- We define another copy of the Booleans, which we will use to store information on the balancing of the tree, p0 will denoted a tree with as many elements in the left sub tree as the right. And p1 will denote a tree where there is one more bit of payload in the left hand tree as in the right. Trees are then empty, leaves, or nodes with parity information: -} data Parity : Set where p0 p1 : Parity data DealT (X : Set) : Set where empT : DealT X leafT : X → DealT X nodeT : Parity → DealT X → DealT X → DealT X {- We explain how to insert a new bit of payload into a tree, in the node case we decide where to put the new data by looking at the parity bit. if it is p0 we insert in the left and return a tree with parity p1. If it is p1 we insert on the right and return a p0 (balanced) tree: -} insert : {X : Set} → X → DealT X → DealT X insert x empT = leafT x insert x (leafT y) = nodeT p0 (leafT y) (leafT x) insert x (nodeT p0 l r) = nodeT p1 (insert x l) r insert x (nodeT p1 l r) = nodeT p0 l (insert x r) {- 'Dealing' then amounts to repeated inserting into a balanced tree, note that this operation differs from the previous deal in that it performs _all_ the dealing in one go. -} deal : List ℕ → DealT ℕ deal [] = empT deal (n ∷ ns) = insert n (deal ns) {- We now explain how to turn a tree into a sorted list by recursively merging the sub trees: -} mergeT : DealT ℕ → List ℕ mergeT empT = [] mergeT (leafT n) = [ n ] mergeT (nodeT p l r) = merge (mergeT l) (mergeT r) {- Our sorting algorithm then proceeds by first building and then recursively merging a tree. Hopefully you can observe that this is equivalent to the naive implementation but now Agda can see that it terminates: -} sort : List ℕ → List ℕ sort ns = mergeT (deal ns) ex1 : List ℕ ex1 = 5 ∷ 2 ∷ 0 ∷ 1 ∷ 4 ∷ 3 ∷ [] ex2 : List ℕ ex2 = 100 ∷ 1 ∷ 10 ∷ 1 ∷ 100 ∷ 10 ∷ []