[Agda] size-based termination

[Andreas Abel]

Hi Ondrej,

On 12/22/10 10:59 AM, Ondrej Rypacek wrote:
> -- 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
>
> 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 problem here is the deep matching qtrans (qsym (...)).  For one, 
sized types would definitely work here (make Quo indexed by size).  [If 
you do not hit a bug].

Or: Cannot you define a more general function that has a flag whether it 
stepped over a qsym.  You want two qsym to cancel out, this is like the 
structurally recursive algorithm to compute a negation normal form.

Here is the Coq code (excuse my heresy).

Require Import Coq.Bool.Bool.

(* assume a type of propositional variables *)
Parameter A : Set.

(* propositional formulas *)
Inductive Form : Set :=
| fAtom  : A -> Form
| fTrue  : Form
| fFalse : Form
| fAnd   : Form -> Form -> Form
| fOr    : Form -> Form -> Form
| fNot   : Form -> Form.

(* computing the negation normal form *)

Fixpoint nnf' (f : Form) (negate : bool) : Form :=
   match f with
     | fAtom a    => if negate then fNot (fAtom a) else fAtom a
     | fTrue      => if negate then fFalse else fTrue
     | fFalse     => if negate then fTrue  else fFalse
     | fAnd f1 f2 => if negate then fOr  (nnf' f1 negate) (nnf' f2 negate)
                               else fAnd (nnf' f1 negate) (nnf' f2 negate)
     | fOr  f1 f2 => if negate then fAnd (nnf' f1 negate) (nnf' f2 negate)
                               else fOr  (nnf' f1 negate) (nnf' f2 negate)
     | fNot f     => nnf' f (negb negate)
   end.

Definition nnf (f : Form) := nnf' f false.

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