Email Gateway (Aug 22 2022 at 11:36): Email Gateway (Aug 22 2022 at 11:36):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
for those of you who do not regularly check stackoverflow but might have
an answer to my question there (yes I am looking at you Florian ;) ) I'm
brazenly posting the link to my question here
http://stackoverflow.com/q/32926842/476803
In short, my question is: What is the easiest way to generate code for a
sorting algorithm that sorts its argument in reverse order, while
building on top of the existing List.sort?
cheers
chris
Email Gateway (Aug 22 2022 at 11:40):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Christian,
Here are my thoughts about List.sort & friends:
a) The first problem with List.sort and friends is that they are defined in the type class
linorder, although their definitions could be made as well in the type class ord. Three
years ago (2ada2be850cb), I have moved all the operations for red-black trees (RBT) into
the linorder type class, precisely because I wanted to use them with other ordering
relations. Ideally, the same should be done for List.sort and friends.
For the time being, you can still avoid some of the overheads by using the foundational
constant linorder.sort_key, which takes the order as an additional argument. So, you can
pass in the dual order. With a single interpretation for the dual order, you should get
all the theorems you need. You can even define an abbreviation for it:
interpretation dual!: linorder "op ≥" "op > :: _ :: linorder ⇒ _" by(rule dual_linorder)
abbreviation "rsort == linorder.sort_key op ≥ (λx. x)"
Unfortunately, code generation does not work out of the box, because the code setup has
only been done for the type-class based instance. If List.sort was defined in the type
class ord, one could simply re-declare the code equations (as I did for the RBT operations
in my AFP entry Containers). Alternatively, you can prove that sort & friends are
parametric (as Peter did for RBT operations in his AFP entry Collections) and exploit
parametricity like he does, but my feeling is that this again requires unconditional
equations, i.e., a definition in ord.
b) The second problem is that we want to implement List.sort with different algorithms
during code generation. For linear orders, this is no problem, because the result is
unique. However, if we pass in a non-linear order, the outcome might depend on the
algorithm. Thus, we can only do program refinement for linear orders. In that view, even
if we move List.sort to the type class ord, we still have problems, because we cannot
prove the code equations for arbitrary ordering relations any more.
Ideally, we should separate the proving part from the code generation part. AFAICS, the
following should work.
Move List.sort and friends to type class ord. For ease of use and compatibility, we can
add sign constraints such that type inference infers the linorder sort constraints for
List.sort.
Define a type 'a linorder of linear orders using typedef and an embedding
linorder_of :: "'a :: linorder itself => 'a linorder"
Define operations for sorting lists that are parametrised with the order from the type
'a linorder. Prove equations like "List.sort_key == sort_key_impl TYPE('a)".
Adapt all the implementations for sorting such that they refine sort_key_impl rather
than List.sort_key.
Apart from sorting, such a setup could be used for further improvements to the generated
code. For example, one could refine the type 'a linorder to provide a comparator instead
of a comparison operation.
I guess such a change requires quite a lot of work to be carried out on the whole
repository. At the moment, I do not have the time to carry all this out, but if the issue
is pressing for you, you might want to try it yourself. But before you start, we should
also ask Florian on his opinion.
Best,
Andreas
Email Gateway (Aug 22 2022 at 11:45):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian, hi Andreas,
I think there is one misperception concerning sort_key – it is not
parametrized by an order, but by a morphism:
"sort_key" :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list"
Hence reverse sorting is difficult to accomplish unless you have a
structure where each element has a dual wrt. the underlying order.
Hence the only way possible I see with the matter »as it is« is indeed a
separate interpretation of the linorder to its dual, together with
suitable mixins:
theory Sort
imports Main "~~/src/Tools/Permanent_Interpretation"
begin
context linorder
begin
permanent_interpretation dual!: linorder greater_eq greater for dummy :: 'b
defining
insort_rev_key = "dual.insort_key :: ('b ⇒ 'a) ⇒ 'b ⇒ 'b list ⇒ 'b list"
and sort_rev_key = "dual.sort_key :: ('b ⇒ 'a) ⇒ 'b list ⇒ 'b list"
by default auto
end
export_code sort_rev_key in Haskell
(Note that you need more mixins if you use the quicksort implementation
from Multiset.thy)
Surely not very convincing due to all the mess generated by the dual order.
IMHO the best way to continue from here is to develope a algorithmic
theory on sorting, which is specifically designed for executability. I
guess this should follow the spirit of the Isabelle collection
framework. The sort in List.thy then could stand as it is.
All the best,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 11:45):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
I think there is one misperception concerning sort_key – it is not
parametrized by an order, but by a morphism:"sort_key" :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list"
The morphism is not the parametrisation I was referring to. I meant the implicit
parametrisation with the order coming from the type class linorder. Obviously, this
parameter can only be seen by looking at the foundational constant for sort_key.
IMHO the best way to continue from here is to develope a algorithmic
theory on sorting, which is specifically designed for executability. I
guess this should follow the spirit of the Isabelle collection
framework. The sort in List.thy then could stand as it is.
I am also in favour of separating reasoning and code generation. But ultimately, you want
to connect the two kinds of sorting.
Best,
Andreas
Am 05.10.2015 um 09:17 schrieb Andreas Lochbihler:
Hi Christian,
Here are my thoughts about List.sort & friends:
a) The first problem with List.sort and friends is that they are defined
in the type class linorder, although their definitions could be made as
well in the type class ord. Three years ago (2ada2be850cb), I have moved
all the operations for red-black trees (RBT) into the linorder type
class, precisely because I wanted to use them with other ordering
relations. Ideally, the same should be done for List.sort and friends.For the time being, you can still avoid some of the overheads by using
the foundational constant linorder.sort_key, which takes the order as an
additional argument. So, you can pass in the dual order. With a single
interpretation for the dual order, you should get all the theorems you
need. You can even define an abbreviation for it:interpretation dual!: linorder "op ≥" "op > :: _ :: linorder ⇒ _"
by(rule dual_linorder)
abbreviation "rsort == linorder.sort_key op ≥ (λx. x)"Unfortunately, code generation does not work out of the box, because the
code setup has only been done for the type-class based instance. If
List.sort was defined in the type class ord, one could simply re-declare
the code equations (as I did for the RBT operations in my AFP entry
Containers). Alternatively, you can prove that sort & friends are
parametric (as Peter did for RBT operations in his AFP entry
Collections) and exploit parametricity like he does, but my feeling is
that this again requires unconditional equations, i.e., a definition in
ord.b) The second problem is that we want to implement List.sort with
different algorithms during code generation. For linear orders, this is
no problem, because the result is unique. However, if we pass in a
non-linear order, the outcome might depend on the algorithm. Thus, we
can only do program refinement for linear orders. In that view, even if
we move List.sort to the type class ord, we still have problems, because
we cannot prove the code equations for arbitrary ordering relations any
more.Ideally, we should separate the proving part from the code generation
part. AFAICS, the following should work.
Move List.sort and friends to type class ord. For ease of use and
compatibility, we can add sign constraints such that type inference
infers the linorder sort constraints for List.sort.Define a type 'a linorder of linear orders using typedef and an
embeddinglinorder_of :: "'a :: linorder itself => 'a linorder"
Define operations for sorting lists that are parametrised with the
order from the type 'a linorder. Prove equations like "List.sort_key ==
sort_key_impl TYPE('a)".Adapt all the implementations for sorting such that they refine
sort_key_impl rather than List.sort_key.Apart from sorting, such a setup could be used for further improvements
to the generated code. For example, one could refine the type 'a
linorder to provide a comparator instead of a comparison operation.I guess such a change requires quite a lot of work to be carried out on
the whole repository. At the moment, I do not have the time to carry all
this out, but if the issue is pressing for you, you might want to try it
yourself. But before you start, we should also ask Florian on his opinion.Best,
AndreasOn 03/10/15 21:59, Christian Sternagel wrote:
Dear all,
for those of you who do not regularly check stackoverflow but might have
an answer to my question there (yes I am looking at you Florian ;) ) I'm
brazenly posting the link to my question herehttp://stackoverflow.com/q/32926842/476803
In short, my question is: What is the easiest way to generate code for a
sorting algorithm that sorts its argument in reverse order, while
building on top of the existing List.sort?cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC