Well-founded recursion has a fixed point

[sassa_nf]

I don't know if there is "the right" way to design inductive types.

https://stackoverflow.com/questions/58899323/how-to-choose-the-design-for-a-well-founded-inductive-type - has an interesting answer that makes the rabbit hole a little deeper, but doesn't particularly advise on what "the right" design is, or whether there even is "the right" design.

Suppose, we are dealing with a list of bits:

data Bin : Set where
   b  : Bin -- an infinite chain of leading zeros
   _O : Bin -> Bin -- a chain ending in zero
   _I : Bin -> Bin -- a chain ending in one

Adding two binary numbers should be straightforward, right?

_-|-_ : Bin -> Bin -> Bin
_-|-_ = 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 O) (n I) = (a b m n) I
  a b (m I) (n O) = (a b m n) I
  a b (m I) (n I) = (a (b I) m n) O
  a c b     n     =  a b c n
  a c m     b     =  a b m c
  a c (m O) (n O) = (a b m n) I
  a c (m O) (n I) = (a c m n) O
  a c (m I) (n O) = (a c m n) O
  a c (m I) (n I) = (a c m n) I

Just enumerate all the cases, reuse calls to the helper function, to add carry flag. We have 12 cases, not 8, because we have extra four cases to deal with the extra constructor, b. Seems legit? Well, computer says "no": not all the calls can be seen to terminate. They do terminate, just cannot be seen to. So we need to demonstrate that the recursion is well-founded: that no matter what is on input, the chain of invocations is finite, the function "a" has a fixed point.

The design for inductive type may help. Maybe this choice of type Bin is poor. Appreciate the difference:

data _<<_ (x : Nat) : Nat -> Set where
  <-b : x << (succ x)
  <-s : (y : Nat) -> x << y -> x << (succ y)

This is the canonical "less-than" relationship for natural numbers. I only used "<<" to distinguish it from the one I actually defined:

data _<_ : Nat -> Nat -> Set where
   z<  : {n : Nat} -> zero < (succ n)
   s<s : {m n : Nat} -> m < n -> (succ m) < (succ n)

It is possible to show they are equivalent.

A relationship is said to be well-founded, if for any value you can "access" all "smaller" values, and no descending chain is infinite.

-- accessibility
data Acc {A : Set} (_<_ : A -> A -> Set) (x : A) : Set where
   acc : ((y : A) -> y < x -> Acc _<_ y) -> Acc _<_ x

Well-founded : (A : Set) -> (R : A -> A -> Set) -> Set
Well-founded A _<_ = (x : A) -> Acc _<_ x

See that function passed to acc constructor? That function can produce a "smaller" value Acc y for a given x. The relationship is well-founded, if we can construct such a Acc for any x.

Here's the canonical way of solving this for the "<<":

<<-Well-founded : Well-founded Nat _<<_
<<-Well-founded x = acc (aux x) where
   aux : (x y : Nat) -> y << x -> Acc _<<_ y
   aux .(succ x) x <-b = <<-Well-founded x
   aux .(succ x) y (<-s x x<y) = aux x y x<y

It's recursive, isn't it? But why is it well-founded? Can you see when it terminates? Its fixed point is very well hidden.

Comments

[juan_gandhi]

I don't even know which language it is, but I appreciate a lot the interest to well-founded relations. They are special. A well-founded category has a very specific lattice of topologies ("Lawvere topologies", as they are called now).

[sassa_nf]

This is Agda and well-founded relations are key to proving termination.

[xacid]

https://en.wikipedia.org/wiki/Agda_(programming_language)

кстати тоже шведы если чо))

[sassa_nf]

...based on Martin-Lof Type Theory, also a Swede. :)