Well-founded recursion gets us to the next level

[sassa_nf]

Ok, Agda can't see why binary number addition, _-|-_, in the other post terminates. Suppose we were to convince it that it does terminate.

It may be possible to attach a "size" of the value - say, the number of bits - to the binary number. Then we could at least reason about the size of the binary numbers decreasing as the addition progresses. But if the size is set definitely, then it is impossible to perform addition at all:

_-|-_ : Bin p -> Bin q -> Bin ...?...

That is, even if we knew the sizes p and q of the two numbers, what should the type of the result be? It may be max(p, q), and it may be max(p, q)+1, depending on how the carry-over happens.

Let's introduce a sized Bin:

bit-len : Bin -> Nat
bit-len b     = zero
bit-len (m O) = succ (bit-len m)
bit-len (m I) = succ (bit-len m)

S-Bin : Nat -> Set
S-Bin n = Sigma Bin \x -> bit-len x < n

which is basically the binary number and a proof that its bit length is smaller than n. Then prove that the _<_ is well-founded, and use this fact to demonstrate the recursion terminates.

<-Well-founded : Well-founded Nat _<_
<-Well-founded x = acc (aux x) where
   aux : (x y : Nat) -> y < x -> Acc _<_ y
   aux zero     y        ()
   aux x        zero     z<        = acc \_ () -- this is the case terminating the recursion; could have called <-Well-founded zero
   aux (succ x) (succ y) (s<s y<x) with is-eq? (succ y) x
   ...                   | no  sy!=x = aux x (succ y) (neq y<x sy!=x)
   ...                   | yes sy==x rewrite sy==x = <-Well-founded x

The recursion terminating case constructs an Acc with a function that just cannot be called - you can't provide an instance of _< zero. By the way, this is the same with _<<_ from the other post, it just is harder to see that it exists: because of the forced pattern matches the case for aux zero _ () is not visible.

Then we can write a function that given two Bin numbers produces a size and the proof that both numbers are smaller than that: max-len : (x y : Bin) -> Sigma Nat \n -> Sigma (bit-len x < n) \_ -> (bit-len y < n)

_-|-_ : Bin -> Bin -> Bin
x -|- y with max-len x y
...   | n , (x<n , y<n) = Sigma.fst (a (<-Well-founded n) b (x , x<n) (y , y<n)) where
  a : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ n)
  a+O : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ (succ n))
  a+I : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ (succ n))

  a+O f c m n with a f c m n
  ...                | r , r<n = r O , s<s r<n

  a+I f c m n with a f c m n
  ...                | r , r<n = r I , s<s r<n

  a {zero} _ _ (_ , ())
  a {succ sz} (acc f) cc mm nn with cc | mm | nn
  ... | b | m O , s<s m< | n O , s<s n< = a+O (f sz n<n1) b (m , m<) (n , n<)
  ... | b | m O , s<s m< | n I , s<s n< = a+I (f sz n<n1) b (m , m<) (n , n<)
  ... | b | m I , s<s m< | n O , s<s n< = a+I (f sz n<n1) b (m , m<) (n , n<)
  ... | b | m I , s<s m< | n I , s<s n< = a+O (f sz n<n1) (b I) (m , m<) (n , n<)
  ... | c | m O , s<s m< | n O , s<s n< = a+I (f sz n<n1) b (m , m<) (n , n<)
  ... | c | m O , s<s m< | n I , s<s n< = a+O (f sz n<n1) c (m , m<) (n , n<)
  ... | c | m I , s<s m< | n O , s<s n< = a+O (f sz n<n1) c (m , m<) (n , n<)
  ... | c | m I , s<s m< | n I , s<s n< = a+I (f sz n<n1) c (m , m<) (n , n<)
  ... | b | b   , z<     | n   , n<     = n , trans-< n< n<n1
  ... | b | m   , m<     | b   , z<     = m , trans-< m< n<n1
  ... | c | b   , z<     | b   , z<     = b I , s<s z<
  ... | c | b   , z<     | n O , s<s {n = succ sz'} n< = a (acc f) b (b I , s<s (z< {sz'})) (n O , s<s n<)
  ... | c | b   , z<     | n I , s<s {n = succ sz'} n< = a (acc f) b (b I , s<s (z< {sz'})) (n I , s<s n<)
  ... | c | m O , s<s {n = succ sz'} m< | b   , z<     = a (acc f) b (m O , s<s m<) (b I , s<s (z< {sz'}))
  ... | c | m I , s<s {n = succ sz'} m< | b   , z<     = a (acc f) b (m I , s<s m<) (b I , s<s (z< {sz'}))

See, here the proof of Well-foundedness of _<_ produces an initial Acc for the max bit size. Now we can produce Acc for smaller bit sizes at will, for example, when the bit sizes of addends change. Agda knows that process terminates - we can't keep constructing new Acc forever.

But Agda also says that you've got to always construct a new Acc, when calling the helper function. The last four cases do not do so, so Agda complains about non-termination just like without any well foundedness of _<_. So, well-founded or not, it is also the case of how you use it. The correct way to describe the last four cases is:

  ... | c | b   , z<     | n O , n<     = n I , trans-< n< n<n1
  ... | c | b   , z<     | n I , s<s {n = succ sz'} n< = a+O (f sz n<n1) c (b , z< {sz'}) (n , n<)
  ... | c | m O , m<     | b   , z<     = m I , trans-< m< n<n1
  ... | c | m I , s<s {n = succ sz'} m< | b   , z<     = a+O (f sz n<n1) c (m , m<) (b , z< {sz'})

That is, whenever a recursive call is made, something must reduce in size - at least Acc. The original call pattern that shuffles carry flag with one of the addends without changing their size, cannot be demonstrated to terminate.

But then, of course, if we just require the addends to always decrease in size, none of this complexity is needed.

_-|-_ = a b where
   a : Bin -> Bin -> Bin -> Bin
   a b b     n     = n
   a b m     b     = m
   a b (m O) (n O) = (a b     m n) O
   a b (m I) (n O) = (a b     m n) I
   a b (m O) (n I) = (a b     m n) I
   a b (m I) (n I) = (a (b I) m n) O
   a c b     b     = b I
   a c (m O) b     = m I
   a c (m I) b     = (a c     m b) O
   a c b     (n O) = n I
   a c b     (n I) = (a c     b n) O
   a c (m O) (n O) = (a b     m n) I
   a c (m I) (n O) = (a c     m n) O
   a c (m O) (n I) = (a c     m n) O
   a c (m I) (n I) = (a c     m n) I

Works just fine, but where we'd be without the detour?