[Sorry for the **ultra** late response. I began writing a reply, went busy
with urgent things... Finally I met Michael at Canterbury some days ago and
realized this was pending.]
Michael is right. I have mixed two different -- but related -- events from
my deep memory.
The first one is the discovery of the pruning effect of laziness on the
naive sort algorithm when "adapted" to the Babel language, which was used
to outperform Prolog. I say "adapted" because in order to achieve the lazy
interleaving of generator and test I needed to code 'permut', 'insert',
etc. as nondeterministic functions which were not legal Babel, but which
happened to work just fine -- the compiler did not reject them and they
returned all the answers. The standard encoding of relations in Babel by
translating Horn clauses into boolean functions did not behave lazily
(basically, it was as inefficient as the Prolog version). So, the example
was a hack that I showed in the demos but that did not actually appear in
the papers.
Of course, as pointed out before, this is still exponential. For example,
if permutations of a list of n elements are generated by randomly picking
one element from it and then appending a permutation of the remaininng
elements (which leads to a pseudo selection sort) it is clear that the
search space contains all the subsequences of the sorted list, i.e. 2^n
paths, and all but one lead to failure. If permutation is implemented by
randomly inserting the head element in a permutation of the tail, then it
can take a long time until the elements "reach the surface" so that they
can be consumed by the test predicate, as in:
isSorted (insert 1 (insert 2 (insert 3 (insert 4 (insert 5 [7,0])))))
which would reduce to False almost immediately if the deduction engine
could apply the lemma mentioned by Sebastian. The method that Sebastian
proposes cleverly solves the problem by "promoting" [7,0] to the first
positions of the 'insertions' sequence [[0], [7,0], ...] so that it can be
discarded by (all isSorted).
The second one is that by transforming the code using folds and unfolds,
efficient algorithms can actually be produced.
I am attaching some examples of this. The examples have been developed in
my own Sloth system, but can be adapted, if necessary to other FLP systems.
File
NaiveSort.curry
contains a naivesort algorithm in which permutation generation is based on
nondeterministic insertion. The transformed code thus implements insertion
sort.
File
NaiveSort2.curry
contains a naivesort algorithm in which permutation generation is based on
nondeterministically picking an element. The transformed code thus
implements selection sort. Both examples require the lemma used by
Sebastian in order to proceed.
Finally, file
NaiveSort7.curry
contains a polynomical naive sort in which, like in Sebastian's solution,
an intermediate type is used.
Best regards.
--
Julio Mariño
Babel research group
Universidad Politecnica de Madrid
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Sep 24 2014 - 17:30:10 CEST