CODEWITHSUNDEEP
haskellinductionproof-of-correctness
P. Ez
P. Ez

Reputation: 103

recursive selection sort proof of correctness

I need to prove that the following selection sort code (in Haskell) is always sorting:

import Data.List (minimum, delete)

ssort :: Ord t => [t] -> [t]
ssort [] = []
ssort xs = let { x = minimum xs } in  x : ssort (delete x xs)

We can assume that we have a function called "sorted" that checks when a list is sorted.

Statement to prove by structural induction: sorted(ssort xs)

I tried the following but I was not able to complete the proof. Can you please help me out to complete the proof?

Base case: xs = []

sorted(ssort xs) =

sorted(ssort []]) =

sorted([]])

correct since sorted([]) is always sorted

Inductive step

IH (inductive hypothesis) = sorted(ssort xs)

show: sorted(ssort y#xs)

case I: x = y = minimum

sorted(ssort y#xs) =

sorted(let { x = minimum (y#xs)} in x : ssort (delete x (y#xs))) = (by definition)

sorted(let { y = minimum (y#xs)} in y : ssort (delete y (y#xs))) = (by substitution)

sorted(y : ssort (delete y (y#xs))) =

sorted(y : ssort (xs)) = (by delete definition)

sorted(y : ssort (xs))

by IH we know that ssort (xs) is sorted, also y is the minimum value so it goes first

case II: y is not minimum

sorted(ssort y#xs) =

sorted(let { x = minimum (y#xs)} in x : ssort (delete x (y#xs))) = (by definition)

.....

no idea

Upvotes: 2

Views: 404

Answers (1)

moonGoose
moonGoose

Reputation: 1510

Your inductive hypothesis is too weak. You should assume that ssort works correctly on any list of length k rather than some specific list xs of length k.

So, instead, assuming ssort is correct on any list of length k and letting xs be any list of length k+1, 

ssort xs 
= let x = minimum xs in x : ssort (delete x xs) -- by definition of `ssort`
= let x = minimum xs in x : sorted (delete x xs) -- `delete x xs` has length `k` so `ssort` sorts it correctly by IH
= sorted xs -- by definition of sorted, minimum, delete

Upvotes: 6

Related Questions