协助 Agda 的终止检查器 [英] Assisting Agda's termination checker
问题描述
假设我们定义了一个函数
Suppose we define a function
f : N o 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.但是，我仍然看不到如何让终止检查器意识到递归是针对较小的子问题进行的.
Agda will paint f in salmon because it cannot tell if n/2 is smaller than n. I don't know how to tell Agda's termination checker anything. I see in the standard library they have a floored division by 2 and a proof that n/2 < n. However, I still fail to see how to get the termination checker to realize that recursion has been made on a smaller subproblem.
推荐答案
Agda 的终止检查器只检查结构递归(即发生在结构上较小的参数上的调用)，而无法建立特定关系(例如 _<_) 意味着其中一个参数在结构上更小.
Agda's termination checker only checks for structural recursion (i.e. calls that happen on structurally smaller arguments) and there's no way to establish that certain relation (such as _<_) implies that one of the arguments is structurally smaller.
题外话:积极性检查器也有类似的问题.考虑标准的定点数据类型:
Digression: Similar problem happens with positivity checker. Consider the standard fix-point data type:
data μ_ (F : Set → Set) : Set where
fix : F (μ F) → μ F
Agda 拒绝这样做，因为 F 在它的第一个参数中可能不是正数.但是我们不能限制 μ 只接受正类型函数，或者证明某个特定类型的函数是正的.
Agda rejects this because F may not be positive in its first argument. But we cannot restrict μ to only take positive type functions, or show that some particular type function is positive.
我们通常如何证明递归函数终止?对于自然数，事实是如果递归调用发生在严格较小的数上，我们最终必须达到零并且递归停止；对于列表，其长度也是如此；对于集合，我们可以使用严格的子集关系；等等.请注意，严格较小的数字"不适用于整数.
How do we normally show that a recursive functions terminates? For natural numbers, this is the fact that if the recursive call happens on strictly smaller number, we eventually have to reach zero and the recursion stops; for lists the same holds for its length; for sets we could use the strict subset relation; and so on. Notice that "strictly smaller number" doesn't work for integers.
所有这些关系共有的属性称为有根据的.非正式地说，如果一个关系没有任何无限下降链，它就是有充分根据的.例如，< 在自然数上是有根据的，因为对于任何数 n:
The property that all these relations share is called well-foundedness. Informally speaking, a relation is well-founded if it doesn't have any infinite descending chains. For example, < on natural numbers is well founded, because for any number n:
n > n - 1 > ... > 2 > 1 > 0
也就是说，这种链的长度受n + 1的限制.
That is, the length of such chain is limited by n + 1.
≤ 在自然数上是没有根据的:
≤ on natural numbers, however, is not well-founded:
n ≥ n ≥ ... ≥ n ≥ ...
< 也不是整数:
n > n - 1 > ... > 1 > 0 > -1 > ...
<小时>
这对我们有帮助吗?事实证明，我们可以对在 Agda 中建立良好关系的关系进行编码，然后使用它来实现您的功能.
Does this help us? It turns out we can encode what it means for a relation to be well-founded in Agda and then use it to implement your function.
为简单起见，我将把 _<_ 关系烘焙到数据类型中.首先，我们必须定义一个数字的可访问性意味着什么:n 是可访问的，如果所有 m 使得 m <;n 也可以访问.这当然在 n = 0 处停止，因为没有 m 所以 m 0 并且此语句不重要.
For simplicity, I'm going to bake the _<_ relation into the data type. First of all, we must define what it means for a number to be accessible: n is accessible if all m such that m < n are also accessible. This of course stops at n = 0, because there are no m so that m < 0 and this statement holds trivially.
data Acc (n : ℕ) : Set where
acc : (∀ m → m < n → Acc m) → Acc n
现在，如果我们可以证明所有自然数都是可访问的，那么我们就证明了 < 是有根据的.为什么呢?acc 构造函数的数量必须是有限的(即没有无限下降链)，因为 Agda 不会让我们编写无限递归.现在，看起来好像我们只是将问题向前推了一步，但编写有根据的证明实际上是结构递归的！
Now, if we can show that all natural numbers are accessible, then we showed that < is well-founded. Why is that so? There must be a finite number of the acc constructors (i.e. no infinite descending chain) because Agda won't let us write infinite recursion. Now, it might seem as if we just pushed the problem back one step further, but writing the well-foundedness proof is actually structurally recursive!
因此，考虑到这一点，以下是 < 的定义是有根据的:
So, with that in mind, here's the definition of < being well-founded:
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 可以这样导入:
Notice that go is nicely structurally recursive. trans can be imported like this:
open import Data.Nat
open import Relation.Binary
open DecTotalOrder decTotalOrder
using (trans)
接下来，我们需要证明⌊ n/2⌋ ≤ n:
Next, we need a proof that ⌊ 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 构造函数.
And finally, we can write your f function. Notice how it suddenly becomes structurally recursive thanks to Acc: the recursive calls happen on arguments with one acc constructor peeled off.
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.
Now, having to work directly with Acc isn't very nice. And that's where Dominique's answer comes in. All this stuff I've written here has already been done in the standard library. It is more general (the Acc data type is actually parametrized over the relation) and it allows you to just use <-rec without having to worry about Acc.
仔细观察，我们实际上非常接近通用解决方案.让我们看看当我们对关系进行参数化时会得到什么.为简单起见，我不处理全域多态性.
Taking a more closer look, we are actually pretty close to the generic solution. Let's see what we get when we parametrize over the relation. For simplicity I'm not dealing with universe polymorphism.
A 上的关系只是一个函数，它接受两个 A 并返回 Set(我们可以称之为二进制谓词):
A relation on A is just a function taking two As and returning Set (we could call it binary predicate):
Rel : Set → Set₁
Rel A = A → A → Set
通过将硬编码的 _<_ : ℕ → ℕ → Set 更改为某种类型 A 上的任意关系，我们可以轻松地概括 Acc:
We can easily generalize Acc by changing the hardcoded _<_ : ℕ → ℕ → Set to an arbitrary relation over some type A:
data Acc {A} (_<_ : Rel A) (x : A) : Set where
acc : (∀ y → y < x → Acc _<_ y) → Acc _<_ x
有根据的定义相应地发生了变化:
The definition of well-foundedness changes accordingly:
WellFounded : ∀ {A} → Rel A → Set
WellFounded _<_ = ∀ x → Acc _<_ x
现在，由于 Acc 是一种与其他任何类型一样的归纳数据类型，我们应该能够编写它的消除器.对于归纳类型，这是一个折叠(很像 foldr 是列表的消除器)——我们告诉消除器如何处理每个构造函数的情况，消除器将其应用于整个结构.
Now, since Acc is an inductive data type like any other, we should be able to write its eliminator. For inductive types, this is a fold (much like foldr is eliminator for lists) - we tell the eliminator what to do with each constructor case and the eliminator applies this to the whole structure.
在这种情况下，我们将使用简单的变体:
In this case, we'll do just fine with the simple variant:
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 参数，所以让我们编写一个小的便利包装器:
If we know that _<_ is well-founded, we can skip the Acc _<_ z argument completly, so let's write small convenience wrapper:
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 _))
事实上，这看起来(和工作)几乎就像标准库中的一样！
And indeed, this looks (and works) almost like the one in the standard library!
如果您想知道，这里是完全依赖的版本:
Here's the fully dependent version in case you are wondering:
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)
这篇关于协助 Agda 的终止检查器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
