在agda中合并排序

Posted 2023-02-25

【中文标题】在agda中合并排序

【英文标题】：Merge sort in agda

【发布时间】：2014-04-11 12:05:58

【问题描述】：

我想在 agda 中实现归并排序。如果我以天真的方式这样做，终止检查器将无法通过程序，因为在我们将输入列表分成两部分，然后递归调用自己之后，agda 不知道每个列表的大小都小于大小的原始列表。

我见过几种解决方案，例如这个：https://gist.github.com/twanvl/5635740，但代码对我来说似乎太复杂了，最糟糕的是我们将程序和证明混合在一起。

【参考方案1】：

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

首先，我们需要使合并排序通用：

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

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

open IsStrictTotalOrder strictTotalOrder

一旦我们证明某个关系是严格的全序，我们就可以将该证明作为该模块的参数，并得到相应的归并排序。

---

第一种方法是使用有根据的递归，这或多或少是您问题中的链接代码使用的。但是，我们不需要证明归并排序在有限次数的比较中返回其输入列表的排序排列，因此我们可以删减大部分代码。

我在this answer 中写了一些关于有根据的递归的内容，您可能想看看。

其他导入优先：

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

如果您在获取此过去终止检查程序时遇到问题，请查看my answer on this。它应该与 Agda 的开发版本一样工作。

split 也很简单：

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

但是现在我们进入了复杂的部分。我们需要证明split 返回两个都小于原始列表的列表（当然，只有当原始列表至少有两个元素时才成立）。为此，我们在列表上定义了一个新关系：xs <ₗ ys 持有 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)

最后，我们用<ₗ-rec 写成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) 中，我们不仅指定要递归的对象，而且还要证明参数小于原始参数。

---

第二种方法是使用大小的类型。我还在this answer写了一个概述，所以你可能想看看。

我们需要在文件顶部使用这个编译指示：

-# 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

实现保持不变，但类型发生了变化。此更改的作用是告诉 Agda split 是 size-preserving。这意味着两个结果列表不能大于输入列表。 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))

确实，这通过了终止检查器。诀窍是上面提到的 size-preserving 属性：Agda 可以看到 split ys 不会生成大于 ys 的列表，因此 x ∷ l 和 y ∷ r 都小于 x ∷ y ∷ ys .这足以说服终止检查员。

---

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

但是，由于这个答案已经很长了，我就给你一个link。

【讨论】：

@KonstantinSolomatov：顺便说一下，这是完整的代码：gist.github.com/vituscze/9440443 和 gist.github.com/vituscze/9440448