协助Agda的终止检查器 [英] Assisting Agda's termination checker

问题描述

假设我们定义一个函数

  f：N \ to N 
f 0 = 0 
f （sn）= f（n / 2） - 这个/运算符被实现为分区。 
  

Agda会在鲑鱼中画f，因为它不能分辨n / 2是否小于n。我不知道如何告诉Agda的终止检查员什么。我在标准库中看到他们有一个2的地板分区和一个证明n / 2 < ñ。然而，我仍然没有看到如何让终止检查器意识到已经对较小的子问题进行了递归。

解决方案

Agda的终止检查器只检查结构递归（即在结构上较小的参数上发生的调用），并且没有办法确定某个关系（如 _< _ ）意味着一个的论点在结构上更小。

---

移动：类似的问题发生在积极性检查器上。考虑标准的定点数据类型：

  dataμ_（F：Set→Set）：设置
修正：F（μF）→μF 
  

Agda否认这一点，因为 F 在第一个参数中可能不是肯定的。但是我们不能限制μ只采用正类型函数，或者显示某些特定类型的函数是正的。

---

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

所有这些关系共享的属性称为充分的自信。非正式地说，如果一个关系没有任何无限下行链，那么它就是有根据的。例如，关于自然数的< 是有根据的，因为对于任何数字 n ：

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

也就是说，这样的链的长度受限于 n + 1 。

≤然而，没有充分的根据：

  n≥n≥...≥n≥... 
  

既不是< 整数：

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

---

这对我们有帮助吗？事实证明，我们可以编码它在Agda中的关系，并将其用于实现您的功能。

为简单起见，我要去将 _< _ 关系烘焙成数据类型。首先，我们必须定义一个数字可以访问的含义：如果所有的 m 这样， n 是可访问的那 m < n 也可以访问。当然这停在 n = 0 ，因为没有 m ，所以 m 并且这个语句持平。



  data Acc（n：ℕ）：Set where 
 acc：（∀m→m   

现在，如果我们可以证明所有的自然数都是可访问的，那么我们证明< 是有根据的。为什么？必须存在有限数量的 acc 构造函数（即没有无限下行链），因为Agda不会让我们编写无限递归。现在，看起来好像我们只是将问题推回了一步，但写出有根据的证明实际上是结构递归！

因此，考虑到这一点，< / code>的定义是有根据的：



  WF ：设置
 WF =∀n→Acc n 
  

而且有充分理由证明：

 < -wf：WF 
 <-wf n = acc（go n）
其中
去：∀nm→m < n→Acc m 
去零m（）
去（suc n）零_ = accλ_（）
去（suc n）（suc m）（s≤sm   

那 go 在结构上是很好的递归。 trans 可以像这样导入：



  open import Data.Nat  
打开导入 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：：→ℕ
fn = go _（<-wf n）
其中
 go：∀n→Acc n→ℕ
 go zero_ = 0 
 go（suc n）（acc a）= go⌊n /2⌋（a _（s≤s（/ 2 -  
 $ / code> 





---

现在，必须直接使用 Acc 并不是很好。这就是Dominique的答案。我写在这里的所有东西已经在标准库中完成了。这是更一般的（ Acc 数据类型实际上是通过关系进行参数化的），它允许您只使用< -rec 而不用担心 Acc 。

---

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

A 上的关系只是一个函数， code> A s并返回 Set （我们可以称它为二元谓词）：

  Rel：Set→Set 1 
 Rel A = A→A→Set 
  

通过改变硬编码 _< _：ℕ→ℕ→Set ，我们可以很容易地推广 Acc $ c>到某个类型的任意关系 A ：

  data Acc {A}（_ <：RelA）（x：A）：设置其中
 acc：（∀y→y   

良好的定义随之发生变化：



  WellFounded：∀{A}→Rel A→Set 
 WellFounded _< _ =∀x→Acc _< _ x 
  pre> 
 
 
现在，既然 Acc 是一个类似于任何其他类型的归纳数据类型，我们应该能够编写它的消除器。对于归纳类型，这是一个折叠（很像 foldr 是列表的消除器） - 我们告诉消除器如何处理每个构造器的情况，消除器将这个应用于整个结构。
 
 
 
在这种情况下，我们可以用简单的变体完成： 
 
 
  foldAccSimple：∀{A} {_ <：Rel A} {R：Set}→
（∀x→（∀y→y ∀z→Acc _< _ z→R 
 foldAccSimple {R = R} acc'= go 
其中
去：∀z→Acc _z→R 
 go z（acc a）= acc'zλy y   
如果我们知道 _< _ 是有根据的，我们可以跳过 Acc _< _ z 所以我们来写一个小的便利包装器： 
 
 
  recSimple：∀{A} {_< _：Rel A}→WellFounded _< _→{R：Set}→
（∀x→（∀y→y  A→R 
 recSimple wf acc'z = foldAccSimple acc'z（wf z）
  
最后：
 
 
 < -wf：WellFounded _< _ 
 < - wf = { - 相同的定义 - } 
 
 <-rec = recSimple <-wf 
 
f：ℕ→ℕ
f =< -rec go 
其中
去：∀n→（∀m→m < （s-s）/ b（b）（b）（b）b→b→b→b→b→b→b code> 
事实上，这看起来（和起作用）差不多，就像标准库中的一样！
 
 
 
 
 
 
以下是完全相关的版本，以备不时之需： 
 
 
  foldAcc：∀{A} {_ <：Rel A}（P：A→Set）→
（∀x→（∀y→y ∀z→Acc _< _ z→P z 
 foldAcc P acc'= go 
 where 
 go：∀z→Acc _z→P z 
 go _ （acc a）= acc'_λ_y 
 rec：∀{A} {_ <：Rel A}→WellFounded _< _ →
（P：A→Set）→（∀x→（∀y→y ∀z→P z 
 rec wf P acc'z = foldAcc P acc'_（wf z）
  
 
Suppose we define a function
f : N \to N
f 0 = 0
f (s n) = f (n/2) -- this / operator is implemented as floored division.
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'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 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.

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
That is, the length of such chain is limited by n + 1.

≤ on natural numbers, however, is not well-founded:
n ≥ n ≥ ... ≥ n ≥ ...
And neither is < on integers:
n > n - 1 > ... > 1 > 0 > -1 > ...




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.

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
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
And the well-foundedness proof:
<-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)
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)
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)
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 _)))




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 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
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
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)
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)
And finally:
<-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屋！