在agda中合并排序

康斯坦丁·索洛马托夫(Konstantin Solomatov)

我想在agda中实现合并排序。如果我天真地执行此操作,则终止检查器将无法通过程序,因为在将输入列表分为两部分然后递归调用自身之后,agda不知道每个列表的大小都小于该大小原始列表中的。

我已经看到了几种解决方案,例如以下解决方案:https : //gist.github.com/twanvl/5635740,但是代码对我来说似乎太复杂了,最糟糕的是我们将程序和证明混在一起。

维特斯

至少可以使用三种方式编写合并排序,以使其通过终止检查器。

首先,这是我们使合并排序通用的条件:

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module MergeSort
  {ℓ a} {A : Set a}
  {_<_ : Rel A ℓ}
  (strictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

open IsStrictTotalOrder strictTotalOrder

一旦证明某种关系是严格的总顺序,就可以将该证明用作该模块的参数并获得相应的合并排序。


第一种方法是使用有据可依的递归,这或多或少是您问题中链接的代码所使用的递归。但是,我们无需证明合并排序以有限的比较次数返回其输入列表的排序排列,因此我们可以剪切大多数代码。

我在此答案中写了一些关于有根据的递归的内容,您可能想检查一下。

其他进口优先:

open import Data.List
open import Data.Nat
  hiding (compare)
open import Data.Product
open import Function
open import Induction.Nat
open import Induction.WellFounded

这是的实现merge

merge : (xs ys : List A) → List A
merge [] ys = ys
merge xs [] = xs
merge (x ∷ xs) (y ∷ ys) with compare x y
... | tri< _ _ _ = x ∷ merge xs (y ∷ ys)
... | tri≈ _ _ _ = x ∷ merge xs (y ∷ ys)
... | tri> _ _ _ = y ∷ merge (x ∷ xs) ys

如果您在通过过去的终止检查器时遇到问题,请查看我对此的回答它应该与Agda的开发版本一样工作。

split 也很容易:

split : List A → List A × List A
split [] = [] , []
split (x ∷ xs) with split xs
... | l , r = x ∷ r , l

但是现在我们进入了复杂的部分。我们需要证明split返回的两个列表都比原始列表小(当然,只有原始列表中至少有两个元素时,这两个列表才成立)。为此,我们在列表上定义了一个新的关系:xs <ₗ yshold iff length x < length y

_<ₗ_ : Rel (List A) _
_<ₗ_ = _<′_ on length

这样的证明就很简单了,只是列表上的一个归纳法:

-- Lemma.
s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
s≤′s ≤′-refl     = ≤′-refl
s≤′s (≤′-step p) = ≤′-step (s≤′s p)

split-less : ∀ (x : A) y ys →
  let xs    = x ∷ y ∷ ys
      l , r = split (x ∷ y ∷ ys)
  in l <ₗ xs × r <ₗ xs
split-less _ _ [] = ≤′-refl , ≤′-refl
split-less _ _ (_ ∷ []) = ≤′-refl , ≤′-step ≤′-refl
split-less _ _ (x ∷ y ∷ ys) with split-less x y ys
... | p₁ , p₂ = ≤′-step (s≤′s p₁) , ≤′-step (s≤′s p₂)

现在,我们拥有了拥有完善的递归机制所需的一切。标准库为我们提供了_<′_有充分关系的证明,我们可以使用它来构建一个证明我们新定义的_<ₗ_关系也有充分依据的证明

open Inverse-image {A = List A} {_<_ = _<′_} length
  renaming (well-founded to <ₗ-well-founded)

open All (<ₗ-well-founded <-well-founded)
  renaming (wfRec to <ₗ-rec)

最后,我们使用<ₗ-recwrite merge-sort

merge-sort : List A → List A
merge-sort = <ₗ-rec _ _ go
  where
  go : (xs : List A) → (∀ ys → ys <ₗ xs → List A) → List A
  go [] rec = []
  go (x ∷ []) rec = x ∷ []
  go (x ∷ y ∷ ys) rec =
    let (l , r)   = split (x ∷ y ∷ ys)
        (p₁ , p₂) = split-less x y ys
    in merge (rec l p₁) (rec r p₂)

注意,在递归调用(rec)中,我们不仅指定要进行递归的内容,还证明了该参数小于原始参数。


第二种方法是使用大小类型。我还在此答案中写了一个概述,因此您可能需要检查一下。

我们需要在文件顶部使用此编译指示:

{-# OPTIONS --sized-types #-}

以及一组不同的进口:

open import Data.Product
open import Function
open import Size

但是,我们不能重用标准库中的列表,因为它们不使用大小类型。让我们定义自己的版本:

infixr 5 _∷_

data List {a} (A : Set a) : {ι : Size} → Set a where
  []  : ∀ {ι} →                  List A {↑ ι}
  _∷_ : ∀ {ι} → A → List A {ι} → List A {↑ ι}

merge 保持大致相同,我们只需要稍微改变一下类型就可以说服终止检查器:

merge : ∀ {ι} → List A {ι} → List A → List A

但是,split有一个微小但非常重要的变化:

split : ∀ {ι} → List A {ι} → List A {ι} × List A {ι}
split [] = [] , []
split (x ∷ xs) with split xs
... | l , r = x ∷ r , l

实现保持不变,但是类型改变了。这是什么变化的确是,它告诉阿格达这split大小保留这意味着两个结果列表不能大于输入的列表。merge-sort然后看起来很自然:

merge-sort : ∀ {ι} → List A {ι} → List A
merge-sort [] = []
merge-sort (x ∷ []) = x ∷ []
merge-sort (x ∷ y ∷ ys) =
  let l , r = split ys
  in  merge (merge-sort (x ∷ l)) (merge-sort (y ∷ r))

实际上,这已经超过了终止检查器。诀窍是上述尺寸保留属性:阿格达可以看到,split ys不会产生大于列表ys,因此x ∷ ly ∷ r均小于x ∷ y ∷ ys这足以说服终止检查器。


在通常意义上,最后一个并不是真正的合并排序。它使用相同的想法,但没有重复拆分列表,对列表进行递归排序然后将它们合并在一起,而是预先进行了所有拆分,将结果存储在树中,然后使用折叠树merge

但是,由于此答案已经相当长,因此我只给您一个链接

本文收集自互联网,转载请注明来源。

如有侵权,请联系 [email protected] 删除。

编辑于
0

我来说两句

0 条评论
登录 后参与评论

相关文章