协助Agda的终止检查

Question

假设我们定义了一个函数

f : N \to N
f 0 = 0
f (s n) = f (n/2) -- this / operator is implemented as floored division.

Agda将在三文鱼中绘制f,因为它无法判断n/2是否小于n.我不知道怎么告诉Agda的终止检查器.我在标准库中看到它们有一个2的分区和n/2 <n的证明.但是,我仍然没有看到如何让终止检查器意识到已经在较小的子问题上进行了递归.

Answer 1

Agda的终止检查器只检查结构递归(即在结构上较小的参数上发生的调用),并且没有办法确定某个关系(例如_<_)暗示其中一个参数在结构上较小.

题外话:积极性检查发生类似的问题.考虑标准的定点数据类型:

data ?_ (F : Set ? Set) : Set where
  fix : F (? F) ? ? F

阿格达拒绝这一点,因为F它的第一个论点可能不是正面的.但是我们不能仅限?于采用正类型函数,或者表明某些特定类型函数是正数.

我们通常如何表明递归函数终止？对于自然数,这是事实,如果递归调用发生在严格较小的数字上,我们最终必须达到零并且递归停止; 对于列表,其长度相同; 对于集合,我们可以使用严格的子集关系; 等等.请注意,"严格较小的数字"不适用于整数.

所有这些关系所共有的财产被称为有根据的.非正式地说,如果一个关系没有任何无限的下行链,那么它就是有根据的.例如,<自然数是有根据的,因为任何数字n:

n > n - 1 > ... > 2 > 1 > 0

也就是说,这种链的长度受到限制n + 1.

? 然而,就自然数而言,并不是很有根据:

n ? n ? ... ? n ? ...

并且都不是<整数:

n > n - 1 > ... > 1 > 0 > -1 > ...

这对我们有帮助吗？事实证明,我们可以编码对于在Agda中有充分根据的关系意味着什么,然后使用它来实现您的功能.

为简单起见,我要将_<_关系烘焙到数据类型中.首先,我们必须定义一个数字可供访问的含义:n如果所有m这些数据都可访问,则可m < n访问.这当然会停止n = 0,因为没有m这样,m < 0而且这个陈述是微不足道的.

data Acc (n : ?) : Set where
  acc : (? m ? m < n ? Acc m) ? Acc n

现在,如果我们能够证明所有自然数都是可访问的,那么我们就证明它<是有根据的.为什么会这样？必须有有限数量的acc构造函数(即没有无限下行链),因为Agda不会让我们写无限递归.现在,似乎我们只是将问题推回了一步,但写出有根据的证据实际上是结构递归的!

因此,考虑到这一点,这里有充分理由的定义<:

WF : Set
WF = ? n ? Acc n

并且有充分的基础证明:

<-wf : WF
<-wf n = acc (go n)
  where
  go : ? n m ? m < n ? Acc m
  go zero    m       ()
  go (suc n) zero    _         = acc ? _ ()
  go (suc n) (suc m) (s?s m<n) = acc ? o o<sm ? go n o (trans o<sm m<n)

请注意,go在结构上很好地递归.trans可以像这样导入:

open import Data.Nat
open import Relation.Binary

open DecTotalOrder decTotalOrder
  using (trans)

接下来,我们需要一个证明? n /2? ? n:

/2-less : ? n ? ? n /2? ? n
/2-less zero          = z?n
/2-less (suc zero)    = z?n
/2-less (suc (suc n)) = s?s (trans (/2-less n) (right _))
  where
  right : ? n ? n ? suc n
  right zero    = z?n
  right (suc n) = s?s (right n)

最后,我们可以编写您的f函数.注意它是如何突然变得结构递归的,这要归功于Acc:递归调用发生在一个acc构造函数剥离的参数上.

f : ? ? ?
f n = go _ (<-wf n)
  where
  go : ? n ? Acc n ? ?
  go zero    _       = 0
  go (suc n) (acc a) = go ? n /2? (a _ (s?s (/2-less _)))

现在,不得不直接工作Acc并不是很好.这就是Dominique的答案所在.我在这里写的所有这些东西都已经在标准库中完成了.它更通用(Acc数据类型实际上是在关系上进行参数化),它允许您使用<-rec而不必担心Acc.

更仔细地看,我们实际上非常接近通用解决方案.让我们看看当我们对关系进行参数化时我们得到了什么.为简单起见,我不处理宇宙多态性.

关系A就是一个带两个As并返回的函数Set(我们可以称之为二元谓词):

Rel : Set ? Set?
Rel A = A ? A ? Set

我们可以Acc通过将硬编码更改为_<_ : ? ? ? ? Set某种类型的任意关系来轻松概括A:

data Acc {A} (_<_ : Rel A) (x : A) : Set where
  acc : (? y ? y < x ? Acc _<_ y) ? Acc _<_ x

有根据的定义也相应改变:

WellFounded : ? {A} ? Rel A ? Set
WellFounded _<_ = ? x ? Acc _<_ x

现在,由于它Acc是一种与任何其他类型的归纳数据类型,我们应该能够编写它的消除器.对于归纳类型,这是一个折叠(很像foldr列表的消除器) - 我们告诉消除器如何处理每个构造函数的情况,并且消除器将其应用于整个结构.

在这种情况下,我们可以使用简单的变体做得很好:

foldAccSimple : ? {A} {_<_ : Rel A} {R : Set} ?
                (? x ? (? y ? y < x ? R) ? R) ?
                ? z ? Acc _<_ z ? R
foldAccSimple {R = R} acc? = go
  where
  go : ? z ? Acc _ z ? R
  go z (acc a) = acc? z ? y y<z ? go y (a y y<z)

如果我们知道这_<_是有根据的,我们可以Acc _<_ z完全跳过这个论点,所以让我们写一个小的便利包装器:

recSimple : ? {A} {_<_ : Rel A} ? WellFounded _<_ ? {R : Set} ?
            (? x ? (? y ? y < x ? R) ? R) ?
            A ? R
recSimple wf acc? z = foldAccSimple acc? z (wf z)

最后:

<-wf : WellFounded _<_
<-wf = {- same definition -}

<-rec = recSimple <-wf

f : ? ? ?
f = <-rec go
  where
  go : ? n ? (? m ? m < n ? ?) ? ?
  go zero    _ = 0
  go (suc n) r = r ? n /2? (s?s (/2-less _))

事实上,这看起来(和工作)几乎像标准库中的那个!

这是完全依赖的版本,以防您想知道:

foldAcc : ? {A} {_<_ : Rel A} (P : A ? Set) ?
          (? x ? (? y ? y < x ? P y) ? P x) ?
          ? z ? Acc _<_ z ? P z
foldAcc P acc? = go
  where
  go : ? z ? Acc _ z ? P z
  go _ (acc a) = acc? _ ? _ y<z ? go _ (a _ y<z)

rec : ? {A} {_<_ : Rel A} ? WellFounded _<_ ?
      (P : A ? Set) ? (? x ? (? y ? y < x ? P y) ? P x) ?
      ? z ? P z
rec wf P acc? z = foldAcc P acc? _ (wf z)

Answer 2

我想提供一个与上面给出的略有不同的答案.特别是,我想建议,而不是试图以某种方式说服终止检查器,实际上,不,这个递归是完全正常的,我们应该尝试重新建立有根据的,以便递归显然是好的,因为结构化.

这里的想法是,问题来自于无法看到它n / 2在某种程度上是"的一部分" n.结构递归想要将一个东西分解成它的直接部分,但是它n / 2的"部分"的方式n是我们互相贬低suc.但事先并不明显有多少下降,我们必须四处寻找并尝试排队.如果我们有一些具有"多个"构造函数的类型,那会更好suc.

为了使问题稍微有趣,让我们尝试定义行为类似的函数

f : ? ? ?
f 0 = 0
f (suc n) = 1 + (f (n / 2))

也就是说,应该是这样的

f n = ? log? (n + 1) ?

现在,上述定义自然不会起作用,出于同样的原因你f不会这样做.但是让我们假装它做了,让我们探索"道路",可以说,这个论点将通过自然数字.假设我们看一下n = 8:

f 8 = 1 + f 4 = 1 + 1 + f 2 = 1 + 1 + 1 + f 1 = 1 + 1 + 1 + 1 + f 0 = 1 + 1 + 1 + 1 + 0 = 4

所以"路径"是8 -> 4 -> 2 -> 1 -> 0.比方说,11？

f 11 = 1 + f 5 = 1 + 1 + f 2 = ... = 4

所以"路径"是11 -> 5 -> 2 -> 1 -> 0.

很自然地,这里发生的是,在每一步我们要么除以2,要么减去1并除以2.每个自然数大于0都可以这种方式唯一地分解.如果它是偶数,则除以2并继续,如果它是奇数,则减1并除以2然后继续.

所以现在我们可以确切地看到我们的数据类型应该是什么样子.我们需要一个具有构造函数的类型,意思是"两倍多suc",另一个代表"两倍suc多加一",当然还有一个构造函数,意思是"零sucs":

data Decomp : ? ? Set where
  zero : Decomp zero
  2*_ : ? {n} ? Decomp n ? Decomp (n * 2)
  2*_+1 : ? {n} ? Decomp n ? Decomp (suc (n * 2))

我们现在可以定义将自然数分解为Decomp与其对应的函数:

decomp : (n : ?) ? Decomp n
decomp zero = zero
decomp (suc n) = decomp n +1

它有助于定义+1为DecompS:

_+1 : {n : ?} ? Decomp n ? Decomp (suc n)
zero +1 = 2* zero +1
(2* d) +1 = 2* d +1
(2* d +1) +1 = 2* (d +1)

给定a Decomp,我们可以将它压缩成一个自然数,忽略了2*_和之间的区别2*_+1:

flatten : {n : ?} ? Decomp n ? ?
flatten zero = zero
flatten (2* p) = suc (flatten p)
flatten (2* p +1 = suc (flatten p)

现在,定义f以下内容是微不足道的:

f : ? ? ?
f n = flatten (decomp n)

这很愉快地通过终止检查器没有任何问题,因为我们从来没有真正重复出现问题n / 2.相反,我们将数字转换为以结构递归方式直接表示其通过数字空间的路径的格式.

编辑它刚刚发生在我之前,这Decomp是二进制数的小端表示.2*_是"向末尾追加0 /向左移位1位"并且2*_+1"向末尾追加1 /向左移1位并加1".所以上面的代码实际上是关于显示二进制数在结构上是递归的,除以2,它们应该是!这让我更容易理解,但我不想改变我已经写过的东西,所以我们可以在这里做一些重命名:Decomp〜>Binary,2*_〜>_,zero,2*_+1〜>_,one,decomp〜>natToBin,flatten〜>countBits.

Answer 3

在接受了Vitus的回答之后,我发现了一种不同的方法来实现证明函数终止于Agda的目标,即使用"大小类型".我在这里提供我的答案,因为它似乎是可以接受的,也是对这个答案的任何弱点的批评.

描述了大小类型:http: //arxiv.org/pdf/1012.4896.pdf

它们在Agda中实现,而不仅仅是MiniAgda; 见这里:http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf.

我们的想法是增加数据类型,其大小允许类型检查器更容易证明终止.大小在标准库中定义.

open import Size

我们定义大小的自然数:

data Nat : {i : Size} \to Set where
    zero : {i : Size} \to Nat {\up i} 
    succ : {i : Size} \to Nat {i} \to Nat {\up i}

接下来,我们定义前驱和减法(monus):

pred : {i : Size} ? Nat {i} ? Nat {i}
pred .{? i} (zero {i}) = zero {i}
pred .{? i} (succ {i} n) = n 

sub : {i : Size} ? Nat {i} ? Nat {?} ? Nat {i}
sub .{? i} (zero {i}) n = zero {i}
sub .{? i} (succ {i} m) zero = succ {i} m
sub .{? i} (succ {i} m) (succ n) = sub {i} m n

现在,我们可以通过Euclid算法定义除法:

div : {i : Size} ? Nat {i} ? Nat ? Nat {i}
div .{? i} (zero {i}) n = zero {i}
div .{? i} (succ {i} m) n = succ {i} (div {i} (sub {i} m n) n)

data ? : Set where
record ? : Set where
notZero :  Nat ? Set
notZero zero = ?
notZero _ = ?

我们给非零分母划分.如果分母非零,则其形式为b + 1.然后我们做divPos a(b + 1)= div ab因为div ab返回ceiling(a /(b + 1)).

divPos : {i : Size} ? Nat {i} ? (m : Nat) ? (notZero m) ? Nat {i}
divPos a (succ b) p = div a b
divPos a zero ()

作为辅助:

div2 : {i : Size} ? Nat {i} ? Nat {i}
div2 n = divPos n (succ (succ zero)) (record {})

现在我们可以定义一种用于计算第n个斐波那契数的分而治之的方法.

fibd : {i : Size} ? Nat {i} ? Nat
fibd zero = zero
fibd (succ zero) = succ zero
fibd (succ (succ zero)) = succ zero
fibd (succ n) with even (succ n)
fibd .{? i}  (succ {i} n) | true = 
  let
    -- When m=n+1, the input, is even, we set k = m/2
    -- Note, ceil(m/2) = ceil(n/2)
    k = div2 {i} n
    fib[k-1] = fibd {i} (pred {i} k)
    fib[k] = fibd {i} k
    fib[k+1] =  fib[k-1] + fib[k]
  in
    (fib[k+1] * fib[k]) + (fib[k] * fib[k-1])
fibd .{? i} (succ {i} n) | false = 
  let
    -- When m=n+1, the input, is odd, we set k = n/2 = (m-1)/2.
    k = div2 {i} n
    fib[k-1] = fibd {i} (pred {i} k)
    fib[k] = fibd {i} k
    fib[k+1] = fib[k-1] + fib[k]
  in
    (fib[k+1] * fib[k+1]) + (fib[k] * fib[k])

Answer 4

你不能直接这样做:Agda的终止检查器只考虑语法上较小的参数的递归.但是,Agda标准库提供了一些模块,用于使用函数参数之间有充分理由的顺序来证明终止.自然数的标准顺序就是这样的顺序,可以在这里使用.

使用Induction.*中的代码,您可以按如下方式编写函数:

open import Data.Nat
open import Induction.WellFounded
open import Induction.Nat

s??s : ? {n m} ? n ?? m ? suc n ?? suc m
s??s ??-refl = ??-refl
s??s (??-step lt) = ??-step (s??s lt)

proof : ? n ? ? n /2? ?? n
proof 0 = ??-refl
proof 1 = ??-step (proof zero)
proof (suc (suc n)) = ??-step (s??s (proof n))

f : ? ? ?
f = <-rec (? _ ? ?) helper
  where
    helper : (n : ?) ? (? y ? y <? n ? ?) ? ?
    helper 0 rec = 0
    helper (suc n) rec = rec ? n /2? (s??s (proof n))

我在这里找到了一篇有一些解释的文章.但可能有更好的参考.