練習問題 4.5.4
関数
insert
の以下ような定義を考える．
insert x xs = takeWhile (≦ x)xs ++ [x] ++ dropWhile (≦ x) xs
xs
が非減少列であるなら，すべての
x
について
insert x xs
も非減少列であることを示せ．
insert
を使ってリストを非減少列に整列する関数
isort
を定義せよ．このとき
foldr
を使え．
(1) ys が非減少列ならば []++ys も ys++[] も非減少列
(2) ys，zs が空ではない非減少列で，かつ last ys ≦ head zs ならば ys++zs は非減少列
(3) xs が非減少列ならば takeWhile p xs も dropWhile p xs もともに非減少列
(4) last (takeWhile (≦x) xs) ≦ x であるから (2)より xs が非減少列ならば takeWhile (≦x) xs ++ [x] も非減少列
(5) (4)，(2) xs が非減少列ならば (takeWhile (≦ x)xs ++ [x]) ++ dropWhile (≦ x) xs も非減少列
(6) したがって，xs が非減少列ならば insert x xs も非減少列である．
insert :: Ord a => a -> [a] -> [a]
insert x xs = takeWhile (<=x) xs ++ [x] ++ dropWhile (<=x) xs
isort :: Ord a => [a] -> [a]
isort = foldr insert []