在agda中合并排序

Question

我想在agda中实现合并排序.如果我以天真的方式执行此操作,终止检查程序无法通过程序,因为在我们将输入列表分成两部分,然后递归调用自己之后,agda不知道每个列表的大小小于大小原始清单.

我已经看过几个解决方案,例如这个:https://gist.github.com/twanvl/5635740但代码对我来说似乎太复杂了,最糟糕的是我们混合了程序和证明.

Answer 1

至少有三种方法可以编写合并排序,以便它通过终止检查程序.

首先,我们需要使合并排序通用:

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)

最后,我们<?-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)中,我们不仅指定要递归的内容,还要证明参数小于原始参数.

第二种方法是使用大小的类型.我在这个答案中也写了一个概述,所以你可能想看一下.

我们需要在文件顶部的这个pragma:

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

事实上,这已经过了终止检查器.诀窍是上面提到的大小保留属性:Agda可以看到split ys不会产生大于的列表ys,因此x ? l并且y ? r都小于x ? y ? ys.这足以说服终止检查员.

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

但是,由于这个答案已经相当长,我只会给你一个链接.