haskell - 递归选择排序正确性证明

Question

我需要证明以下selection sort代码(在 Haskell 中)总是排序:

import Data.List (minimum, delete)

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

我们可以假设我们有一个名为“sorted”的函数，用于检查列表何时排序。

通过结构归纳法证明的语句:sorted(ssort xs)

我尝试了以下方法，但无法完成证明。你能帮我完成证明吗？

<小时/>

基本情况:xs = []

sorted(ssort xs) =

sorted(ssort []]) =

sorted([]])

correct since sorted([]) is always sorted

<小时/>

归纳步骤

IH(归纳假设)=排序(ssort xs)

显示:已排序(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

Answer 1

你的归纳假设太弱了。您应该假设 ssort 在长度为 k 的任何列表上正常工作，而不是某些特定列表xs长度为 k 的 。

因此，假设 ssort 在任何长度为 k 的列表上都是正确的，并让 xs 为任何长度为 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