functional-programming - 协助Agda的终止检查器

Question

假设我们定义一个函数

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

Agda会在鲑 fish 中绘制f，因为它无法分辨n / 2是否小于n。我不知道该如何告诉Agda的终止检查器。我在标准库中看到它们有2的下限除法和n / 2

Answer 1

Agda的终止检查器仅检查结构递归(即，在结构上较小的参数上发生的调用)，并且无法建立某种关系(例如_<_)表示某个参数在结构上较小。

离题:阳性检查器也会发生类似的问题。考虑标准的定点数据类型:

data μ_ (F : Set → Set) : Set where
  fix : F (μ F) → μ F

Agda拒绝这样做，因为 F的第一个参数可能不是正数。但是我们不能将 μ限制为仅使用正类型函数，也不能证明某些特定类型函数是正类型。

我们通常如何显示递归函数终止？对于自然数，这是一个事实，如果递归调用发生在严格较小的数字上，则最终我们必须达到零，并且递归停止；对于 list ，其长度保持不变；对于集合，我们可以使用严格子集关系；等等。请注意，“严格小于数字”不适用于整数。

所有这些关系共有的属性(property)被称为有根据。非正式地讲，如果没有任何无限的下降链，则该关系是有充分根据的。例如，关于自然数的 <是有充分根据的，因为对于任何数字 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上的关系只是一个接受两个 A并返回 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)