递归选择排序正确性证明

Question

我需要证明以下选择排序代码（在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（[]）总是被排序

---

归纳步骤

IH（归纳假设）=排序（ssort xs）

显示：排序（排序y＃xs）

情况I：x = y =最小值

sorted（sort y＃xs）=

sorted（let {x = x中的最小值（y＃xs）}：ssort（删除x（y＃xs）））=（根据定义）

sorted（let {y = y中的最小值（y＃xs）}：ssort（删除y（y＃xs）））=（通过替换）

sorted（y：ssort（删除y（y＃xs）））=

sorted（y：ssort（xs））=（按删除定义）

排序（y：ssort（xs））

通过IH，我们知道sort（xs）已排序，y也是最小值，因此它排在第一位

情况二：y不是最小值

sorted（sort y＃xs）=

sorted（let {x = x中的最小值（y＃xs）}：ssort（删除x（y＃xs）））=（根据定义）

.....

不知道

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