[Agda] size-based termination

[Ondrej Rypacek]

>
> {-# OPTIONS --no-termination-check #-}
>
Thanks, that'll do for the moment.

> Aeh.  Depends.  What about adding a dummy argument which is structurally
> decreasing in each recursive call?

Yes, sure. But this must be tied somehow with the real argument I'm
recursing on, so that I don't run out of my structural argument before
the size is actually zero.

>
> With more concrete input I can give more concrete answers...

Here it is:

-- equivalence by a chain of elements of X
data Quo {X Y : Set}(f g : X → Y) : Y → Y → Set where
  qrefl : (b : Y) → Quo  f g b b
  qsym : {a b : Y} → Quo f g a b → Quo f g b a
  qstep : {a b c : Y} → {x : X} → f x ≡ a → g x ≡ b → Quo f g b c → Quo f g a c
  qstep' : {a b c : Y} → {x : X} → f x ≡ b → g x ≡ a → Quo f g b c → Quo f g a c


The difficulty comes from the fact that I don't have qrefl, qsym ,
qtrans, and qatom, but qstep merges transitivity and step into one ,
providing for a right bracketed representation of the transitive
reflexive symmetric closure of a qstep : Quo f g a b. Hope this all
makes sense, but I don't want to tire you with too much irrelevant
detail. So it's sort of a cut eliminated reflective transitive
symmetric closure.

Now I want to recover transitivity by a function.

qtrans : {X Y : Set}{a b c : Y}{f g : X → Y} → Quo f g a b → Quo f g b
c → Quo f g a c
qtrans {a = .b} {b = b} (qrefl .b) k =  k
qtrans {a = a} (qsym (qrefl .a)) k = k
qtrans (qsym (qsym  y)) k = qtrans y k
qtrans (qsym (qstep y y' y0)) k = qtrans (qsym y0) (qstep' y y' k)
qtrans {a = a} {b = b} {c = c} (qsym {.b} {.a} (qstep' {.b} {b'} {.a}
{x} y y' y0)) k = qtrans (qsym y0) (qstep y y' k)
qtrans (qstep y y' y0) k = qstep y y' (qtrans y0 k)
qtrans (qstep' y y' y0) k = qstep' y y' (qtrans y0 k)


The nonstructural cases are no. 5 and 6 , the depth of the first
argument decreases though.

I tried introducing a size argument to Quo, making it a family indexed
by Nat, but then the following becomes more complicated , because now
Quo is not an equivalence for any specific n : Nat but as a family as
a whole.


quoIsEquivalence : ∀ {X Y f g} → IsEquivalence (Quo {X}{Y} f g)
quoIsEquivalence {X}{Y}{f}{g} = record { refl = λ {x} → qrefl x ; sym
= λ {i}{j} x → qsym x ; trans = λ x y → qtrans x y   }


If I just pass a Nat along with a Quo , I must make sure it is the
size, and that at each step it remains so.
So if I define a size : Quo f g a b -> Nat , I could add an auxiliary
argument (n : Nat) together with (n == size q). And then perhaps
recurse on the proof that n == size q ? Or more precisely, use it to
ensure that I don't run out of q before n , or n before q.

Does this sound like a viable strategy ?


I was hoping there is a paper or a piece of source code where I could
find an example of this so I'm not  reinventing the wheel.

Cheers,
Ondrej


>
> Cheers,
> Andreas
>