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 将在鲑鱼中绘制 f，因为它无法判断 n/2 是否小于 n。我不知道如何告诉 Agda 的终止检查器任何事情。我在标准库中看到他们有一个除以 2 和一个证明 n/2 < n。但是，我仍然看不到如何让终止检查器意识到已经对较小的子问题进行了递归。

Answer 1

Answer 2

I would like to offer a slightly different answer than the ones given above. In particular, I want to suggest that instead of trying to somehow convince the termination checker that actually, no, this recursion is perfectly fine, we should instead try to reify the well-founded-ness so that the recursion is manifestly fine in virtue of being structural.

The idea here is that the problem comes from being unable to see that n / 2 is somehow a "part" of n. Structural recursion wants to break a thing into its immediate parts, but the way that n / 2 is a "part" of n is that we drop every other suc. But it's not obvious up front how many to drop, we have to look around and try to line things up. What would be nice is if we had some type that had constructors for "multiple" sucs.

To make the problem slightly more interesting, let's instead try to define the function that behaves like

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

that is to say, it should be the case that

f n = ⌈ log₂ (n + 1) ⌉

Now naturally the above definition won't work, for the same reasons your f won't. But let's pretend that it did, and let's explore the "path", so to speak, that the argument would take through the natural numbers. Suppose we look at 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

so the "path" is 8 -> 4 -> 2 -> 1 -> 0. What about, say, 11?

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

so the "path" is 11 -> 5 -> 2 -> 1 -> 0.

Well naturally what's going on here is that at each step we're either dividing by 2, or subtracting one and dividing by 2. Every naturally number greater than 0 can be decomposed uniquely in this fashion. If it's even, divide by two and proceed, if it's odd, subtract one and divide by two and proceed.

So now we can see exactly what our data type should look like. We need a type that has a constructor that means "twice as many suc's" and another that means "twice as many suc's plus one", as well as of course a constructor that means "zero sucs":

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

We can now define the function that decomposes a natural number into the Decomp that corresponds to it:

decomp : (n : ℕ) → Decomp n
decomp zero = zero
decomp (suc n) = decomp n +1

It helps to define +1 for 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)

Given a Decomp, we can flatten it down into a natural number that ignores the distinctions between 2*_ and 2*_+1:

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

And now it's trivial to define f:

f : ℕ → ℕ
f n = flatten (decomp n)

This happily passes the termination checker with no trouble, because we're never actually recursing on the problematic n / 2. Instead, we convert the number into a format that directly represents its path through the number space in a structurally recursive way.

Edit It occurred to me only a little while ago that Decomp is a little-endian representation of binary numbers. 2*_ is "append 0 to the end/shift left 1 bit" and 2*_+1 is "append 1 to the end/shift left 1 bit and add one". So the above code is really about showing that binary numbers are structurally recursive wrt dividing by 2, which they ought to be! That makes it much easier to understand, I think, but I don't want to change what I wrote already, so we could instead do some renaming here: Decomp ~> Binary, 2*_ ~> _,zero, 2*_+1 ~> _,one, decomp ~> natToBin, flatten ~> countBits.

Answer 3

After accepting Vitus' answer, I discovered a different way to accomplish the goal of proving a function terminates in Agda, namely using "sized types." I am providing my answer here because it seems acceptable, and also for critique of any weak points of this answer.

Sized types are described: http://arxiv.org/pdf/1012.4896.pdf

They are implemented in Agda, not only MiniAgda; see here: http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf.

The idea is to augment the data type with a size that allows the typechecker to more easily prove termination. Size is defined in the standard library.

open import Size

We define sized natural numbers:

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

Next, we define predecessor and subtraction (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

Now, we may define division via Euclid's algorithm:

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 _ = ⊤

We give division for nonzero denominators. If the denominator is nonzero, then it is of the form, b+1. We then do divPos a (b+1) = div a b Since div a b returns 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 ()

As auxiliary:

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

Now we can define a divide and conquer method for computing the n-th Fibonacci number.

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))

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

Answer 5

A similar question appeared on the Agda mailing-list a few weeks ago and the consensus seemed to be to inject the Data.Nat element into Data.Bin and then use structural recursion on this representation which is well-suited for the job at hand.

You can find the whole thread here : http://comments.gmane.org/gmane.comp.lang.agda/5690

Answer 6