我需要证明以下选择排序代码（在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 …
我在Haskell中寻找以下选择排序代码的非尾递归版本：
import Data.List (minimum, delete)
ssort :: Ord t => [t] -> [t]
ssort [] = []
ssort xs = let { x = minimum xs } in x : ssort (delete x xs)
您能否提供选择排序的非尾递归版本？
我知道更改原始代码不是一个好主意，但我需要该版本才能进行实验。