[Agda] termination proofs

[gallais at ensl.org]

Hi Serge,

This is a well-known problem and one possible trick is to
perform all the sub-computations in a with clause.

See comment 10 of this issue for a code snippet :
http://code.google.com/p/agda/issues/detail?id=59#c10

Cheers,

--
gallais


On 22 September 2012 14:05, Serge D. Mechveliani <mechvel at botik.ru> wrote:
> People,
> I have a question on the termination proofs.
> Consider the example:
>
>   merge : List Nat x List Nat -> List Nat
>   merge ([] ,      ys     ) =  ys
>   merge (xs ,      []     ) =  xs
>   merge (x :: xs , y :: ys)  with  x <=? y
>   ...                    | yes _ =  x :: (merge (xs ,      y :: ys))
>   ...                    | _     =  y :: (merge (x :: xs , ys     ))
>
> (a couple of math symbols are replaced, for this letter).
> Agda-2.3.0.1  reports  "Termination checking failed ...".
>
> I hoped that each the argument   (xs , y:: ys)  and  (x :: xs , ys)
> is syntactically smaller than    (x :: xs , y ::ys),
>
> that the compiler would find it, and that this is sufficient for the
> termination proof.
>
> Has it sense considering some development for the Agda termination
> syntax ordering?
>
> What may be a possibly simple way out for this particular program?
> To introduce to the loop an additional argument of
>                                        l = length (xs ++ ys)  : Nat
> ?
> (similarly, put  counterList = xs ++ ys,  and remove the head from
> counterList in the loop).
>
> Now, for a general situation: my current naive idea is as follows.
> (1) The programmer introduces for each problem function  foo  the size
>     function
>              size-foo : <arguments of foo> -> Nat
>     and adds its value  s  to the arguments -- which makes it  foo'.
> (2) The proof is provided in the program loop for that
>     size-foo args > size-foo args'  for  args  and  args'  from LHS
>     and RHS respectively ...
> (3) s == 0  is set as an additional stop point for  foo' (and the proof
>     is provided in the result for the aimed properties of  foo, foo').
>
> Seeing (1), (2), (3), the compiler will hopefully decide that  foo'
> terminates, and this looks like a verification.
>
> What an approach does  Agda  suggest for a programmer?
>
> Thank you in advance for explanation,
>
> -------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda