Как сгенерировать код для обратной сортировки

Question

Что является самым простым способом генерации кода для алгоритма сортировки, который сортирует свой аргумент в обратном порядке, а строит поверх существующего List.sort?

Я придумал два решения, которые показаны ниже в моем ответе. Но оба они не очень удовлетворительны.

Любые другие идеи, как это можно сделать?

Answer 1

Я придумал два возможных решения. Но у обоих есть (серьезные) недостатки. (Я хотел бы получить результат почти автоматически.)

1. Ввести новый тип Haskell. Например, если мы хотим, чтобы сортировать списки nat с, что-то вроде

   datatype 'a new = New (old : 'a) 
   
   instantiation new :: (linorder) linorder 
   begin 
   
   definition "less_eq_new x y ⟷ old x ≥ old y" 
   definition "less_new x y ⟷ old x > old y" 
   
   instance by (default, case_tac [!] x) (auto simp: less_eq_new_def less_new_def) 
   
   end 
   

   На данный момент

   value [code] "sort_key New [0::nat, 1, 0, 0, 1, 2]" 
   

   дает желаемую обратную сортировку. Хотя это сравнительно просто, это не так автоматично, как хотелось бы, чтобы решение было и, кроме того, имело небольшие накладные расходы во время выполнения (поскольку Isabelle не имеет ).

2. Через локаль для двойного линейного порядка. Сначала мы более или менее копируем существующий код для сортировки вставки (но вместо того, чтобы полагаться на класс типа, мы делаем параметр, который представляет сравнение явно).

   fun insort_by_key :: "('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'a list ⇒ 'a list" 
   where 
       "insort_by_key P f x [] = [x]" 
   | "insort_by_key P f x (y # ys) = 
       (if P (f x) (f y) then x # y # ys else y # insort_by_key P f x ys)" 
   
   definition "revsort_key f xs = foldr (insort_by_key (op ≥) f) xs []" 
   

   на данный момент у нас есть код для revsort_key.

   value [code] "revsort_key id [0::nat, 1, 0, 0, 1, 2]" 
   

   , но мы также хотим, все хорошие результаты, которые уже были доказаны в linorder местности (что вытекает из linorder класса). С этой целью мы вводим двойственный линейный порядок и используем «mixin» (не уверен, что я использую правильное имя здесь), чтобы заменить все вхождения linorder.sort_key (что не позволяет генерировать код) нашим новым " константа кода "revsort_key.

   interpretation dual_linorder!: linorder "op ≥ :: 'a::linorder ⇒ 'a ⇒ bool" "op >" 
   where 
       "linorder.sort_key (op ≥ :: 'a ⇒ 'a ⇒ bool) f xs = revsort_key f xs" 
   proof - 
       show "class.linorder (op ≥ :: 'a ⇒ 'a ⇒ bool) (op >)" by (rule dual_linorder) 
       then interpret rev_order: linorder "op ≥ :: 'a ⇒ 'a ⇒ bool" "op >" . 
       have "rev_order.insort_key f = insort_by_key (op ≥) f" 
       by (intro ext) (induct_tac xa; simp) 
       then show "rev_order.sort_key f xs = revsort_key f xs" 
       by (simp add: rev_order.sort_key_def revsort_key_def) 
   qed 
   

   Хотя с этим решением мы не имеем какое-либо во время выполнения пенальти, он слишком многословен, на мой вкус и не легко адаптироваться к изменениям в настройке стандартного кода (например, если мы хотим использовать mergesort от Archive of Formal Proofs для всех наших операций сортировки).