通过排序反转列表?

August 20, 2013

前天在某个地方的习题看到的，忘了具体是哪里。

问：能不同通过一个特定排序关系和特定的排序算法实现反转列表？

例如这个：

cmp x y = if x == y then LT else GT

reverseBySort = sortBy cmp

用QuickCheck试了一下似乎真可以哦：

ghci > quickCheck $ \ls -> reverse ls == reverseBySort (ls::[Int])
+++ OK, passed 100 tests

再把测试次数加大，发现这个cmp和sortBy是是不行的：

ghci> let prop = \ls -> reverse ls == reverseBySort (ls::[Int])
ghci> quickCheckWith (stdArgs {maxSuccess = 10000}) prop
*** Failed! Falsifiable (after 4107 tests and 2 shrinks):
[6,6,0,6]

现在有这些函数:

  1. cmp :: Ord a -> a -> a -> Ordering
  2. sortBy :: Ord a => (a -> a -> Ordering) -> [a] -> [a]

其中sortBy必须满足sortBy compare是正确的升序排序，怎么证明 \(\exists ls . sortBy \;cmp\; ls \neq reverse\; ls\) ?