终止检查列表合并

Question

Agda 2.3.2.1无法看到以下函数终止:

open import Data.Nat
open import Data.List
open import Relation.Nullary

merge : List ? ? List ? ? List ?
merge (x ? xs) (y ? ys) with x ?? y
... | yes p = x ? merge xs (y ? ys)
... | _     = y ? merge (x ? xs) ys 
merge xs ys = xs ++ ys

Agda wiki说,如果递归调用的参数按字典顺序减少,那么终止检查器就可以了.基于此,似乎这个功能也应该通过.那我在这里错过了什么？此外,在以前版本的Agda中它可能还可以吗？我在互联网上看过类似的代码,没有人提到那里的终止问题.

Answer 1

我不能告诉你为什么会发生这种情况,但我可以告诉你如何治愈这些症状.在开始之前:这是终止检查程序的已知问题.如果你精通Haskell,你可以看看源代码.

一种可能的解决方案是将函数拆分为两个:第一个用于第一个参数变小的情况,第二个用于第二个变量:

mutual
  merge : List ? ? List ? ? List ?
  merge (x ? xs) (y ? ys) with x ?? y
  ... | yes _ = x ? merge xs (y ? ys)
  ... | no  _ = y ? merge? x xs ys
  merge xs ys = xs ++ ys

  merge? : ? ? List ? ? List ? ? List ?
  merge? x xs (y ? ys) with x ?? y
  ... | yes _ = x ? merge xs (y ? ys)
  ... | no  _ = y ? merge? x xs ys
  merge? x xs [] = x ? xs

所以,第一个功能切断xs,一旦我们必须切断ys,我们切换到第二个功能,反之亦然.

另一个(也许是令人惊讶的)选项,也是在问题报告中提到的,是通过以下方式介绍递归的结果with:

merge : List ? ? List ? ? List ?
merge (x ? xs) (y ? ys) with x ?? y | merge xs (y ? ys) | merge (x ? xs) ys
... | yes _ | r | _ = x ? r
... | no  _ | _ | r = y ? r
merge xs ys = xs ++ ys

最后,我们可以在tors上执行递归Vec,然后转换回List:

open import Data.Vec as V
  using (Vec; []; _?_)

merge : List ? ? List ? ? List ?
merge xs ys = V.toList (go (V.fromList xs) (V.fromList ys))
  where
  go : ? {n m} ? Vec ? n ? Vec ? m ? Vec ? (n + m)
  go {suc n} {suc m} (x ? xs) (y ? ys) with x ?? y
  ... | yes _                 = x ? go xs (y ? ys)
  ... | no  _ rewrite lem n m = y ? go (x ? xs) ys
  go xs ys = xs V.++ ys

但是,这里我们需要一个简单的引理:

open import Relation.Binary.PropositionalEquality

lem : ? n m ? n + suc m ? suc (n + m)
lem zero    m                 = refl
lem (suc n) m rewrite lem n m = refl

我们也可以直接go返回List并完全避免引理:

merge : List ? ? List ? ? List ?
merge xs ys = go (V.fromList xs) (V.fromList ys)
  where
  go : ? {n m} ? Vec ? n ? Vec ? m ? List ?
  go (x ? xs) (y ? ys) with x ?? y
  ... | yes _ = x ? go xs (y ? ys)
  ... | no  _ = y ? go (x ? xs) ys
  go xs ys = V.toList xs ++ V.toList ys

第一个技巧(即将函数分成几个相互递归的函数)实际上是非常好的记忆.由于终止检查器没有查看您使用的其他函数的定义,因此它拒绝了大量非常精细的程序,请考虑:

data Rose {a} (A : Set a) : Set a where
  []   :                     Rose A
  node : A ? List (Rose A) ? Rose A

现在,我们想要实现mapRose:

mapRose : ? {a b} {A : Set a} {B : Set b} ?
          (A ? B) ? Rose A ? Rose B
mapRose f []          = []
mapRose f (node t ts) = node (f t) (map (mapRose f) ts)

但是,终止检查器不会查看map它是否与元素没有任何关系,只是拒绝这个定义.我们必须内联定义map并编写一对相互递归的函数:

mutual
  mapRose : ? {a b} {A : Set a} {B : Set b} ?
            (A ? B) ? Rose A ? Rose B
  mapRose f []          = []
  mapRose f (node t ts) = node (f t) (mapRose? f ts)

  mapRose? : ? {a b} {A : Set a} {B : Set b} ?
             (A ? B) ? List (Rose A) ? List (Rose B)
  mapRose? f []       = []
  mapRose? f (t ? ts) = mapRose f t ? mapRose? f ts

通常,您可以在where声明中隐藏大部分混乱:

mapRose : ? {a b} {A : Set a} {B : Set b} ?
          (A ? B) ? Rose A ? Rose B
mapRose {A = A} {B = B} f = go
  where
  go      :       Rose A  ?       Rose B
  go-list : List (Rose A) ? List (Rose B)

  go []          = []
  go (node t ts) = node (f t) (go-list ts)

  go-list []       = []
  go-list (t ? ts) = go t ? go-list ts

注意:可以使用在定义两个函数的签名之前声明它们,而不是mutual在较新版本的Agda中.

更新:Agda的开发版本对终止检查器进行了更新,我将让提交消息和发布说明自行说明:

• 调用图完成的修订版,可以处理任意终止深度.这个算法已经在MiniAgda中待了一段时间,等待它的伟大日子.它现在在这里!选项 - 终止深度现在可以退役.

并从发布说明:

• 由'with'定义的函数的终止检查已得到改进.

  之前需要的案例 - 终止深度(现已过时!)通过终止检查器(由于使用'with')不再
  需要该标志.例如

  merge : List A ? List A ? List A
  merge [] ys = ys
  merge xs [] = xs
  merge (x ? xs) (y ? ys) with x ? y
  merge (x ? xs) (y ? ys)    | false = y ? merge (x ? xs) ys
  merge (x ? xs) (y ? ys)    | true  = x ? merge xs (y ? ys)
  

  之前未能终止检查,因为'with'扩展为辅助功能merge-aux:

  merge-aux x y xs ys false = y ? merge (x ? xs) ys
  merge-aux x y xs ys true  = x ? merge xs (y ? ys)
  

  此函数调用merge,其中一个参数的大小在增加.为了使这个通过,终止检查器现在在检查之前内联merge-aux的定义,从而有效地终止检查原始源程序.

  由于这种转换,对变量执行'with'不再保留终止.例如,这不会终止检查:

  bad : Nat ? Nat
  bad n with n
  ... | zero  = zero
  ... | suc m = bad m
  

事实上,您的原始功能现在通过终止检查!