# Insertion Sort from Permutation Sort

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Wed, 16 Oct 2013 16:05:24 +0900

Hello!

A folklore example of our community is "permutation sort", where a
list of numbers is sorted by "first" permuting all its elements
nondeterministically and "then" checking whether the result is sorted.

An important aspect of this example is pruning thanks to laziness.
Although the program looks like permuting first and then checking for
sortedness, large parts of the search space are pruned by lazy
evaluation, interleaving the generator and the test.

That said, the pruned parts are not large enough to make the resulting
program efficient. Experimental results suggest that it is still
exponential in the worst case.

It just occurred to me that permutation sort can be expressed in a way
that allows significantly more pruning. The essential idea is the
following observation:

isSorted (insert x xs) ==> isSorted xs

or equivalently

not (isSorted xs) ==> not (isSorted (insert x xs))

where `isSorted` checks whether a given list is sorted and `insert`
inserts the first argument into the second at an arbitrary position
nondeterministically.

Thanks to this observation, we can discard subsequent insertions if we
detect that intermediate results are already out of order.

One way to implement a `permute` operation is to use the `foldl`
function like this:

permute :: [a] -> [a]
permute = foldl (flip insert) []

In order to collect intermediate results, we can use `scanl` from the

insertions :: [a] -> [[a]]
insertions = scanl (flip insert) []

For example, `insertions [1,2]` has two possible results,
`[[],[1],[1,2]]` or `[[],[1],[2,1]]`. The last element of `insertions
l` is always a permutation of `l`.

In analogy to permutation sort defined as

psort :: [Int] -> [Int]
psort xs | isSorted p = p
where
p = permute xs

we can define a function isort that uses `insertions` rather than `permute`.

isort :: [Int] -> [Int]
isort xs | all isSorted ps = last ps
where
ps = insertions xs

Thanks to the above observation (and laziness of `all`), this
definition detects early if the final permutation is unsorted based on
unsortedness of an intermediate insertion.

It seems that unsorted insertions are discarded immediately, just as
if the `isSorted` check would have been incorporated into the
definition of `insert`. Experiments suggest that indeed, the resulting
code has quadratic worst case complexity, just like insertion sort.

The complete code is attached to this email.

Best regards,
Sebastian

P.S. My observation is inspired by a paper [1] shown to me by Keisuke
Nakano after I gave a Curry tutorial at NII Tokyo. Although
`insertions` does not seem to compute an "improving sequence" in the
sense of that paper, the technique seems certainly related.

[1] Pruning with improving sequences in lazy functional programs
Hideya Iwasaki,Takeshi Morimoto,Yasunao Takano