# Re: Insertion Sort from Permutation Sort

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

Hi Julio,

that's interesting. The Babel implementation must have been different
from the Curry implementations I was aware of until today.

Can you provide a reference to the implementation you have in mind?
After a quick search, I just found [2] which investigates the run time
of permutation sort on page eleven. Even the best (lazily pruning)
version there (apparently) still has exponential complexity.

Thanks,
Sebastian

[2] Efficient Translation of Lazy Functional Logic Programs into Prolog
Michael Hanus
www.informatik.uni-kiel.de/~mh/papers/LOPSTR95.ps

On Wed, Oct 16, 2013 at 6:32 PM, Julio Mariņo <jmarino_at_fi.upm.es> wrote:
> Permutation sort was one of the standard benchmarks of the Babel FL language
> in the early nineties. The fact that its lazy implementation was equivalent
> to insertion sort was well known, and we actually used the performance
> figures to impress the Prolog people ;)
>
> Julio
>
>
> On Wed, Oct 16, 2013 at 9:05 AM, Sebastian Fischer
> <sebf_at_informatik.uni-kiel.de> wrote:
>>
>> 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
>> `List` module instead of `foldl`
>>
>> 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
>>
>> _______________________________________________
>> curry mailing list
>> curry_at_lists.RWTH-Aachen.DE
>> http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
>>
>
>
>
> --
> Julio Mariņo
> Babel research group