[Agda] termination proofs

[Serge D. Mechveliani]

On Sat, Sep 22, 2012 at 02:17:16PM +0100, gallais @ ensl.org wrote:
[..]
> 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
[..]

I am trying this approach. Thank you.

This is a particular issue concerninig  termination--and--`with'.

But what a generic approach does  Agda  suppose for a programmer?

Where it is specified in the Language which functions are considered
as provably terminating?
I have seen somewhere an explanation about a certain syntactic
comparison of LHS and RHS, and now do not recall of where this is
described.

Further, Agda specifies clearly what is an ordinary proof: a member
of a such and such (dependent) type defined in a program. And it is a
_data_  of the language, it can be explicitly processed by the user
program. This provides an explicit verification. And there are possible
various library	tools which help constructing such proofs.

Now: how to make a  termination	proof  as explicit as possible?
There is a certain syntactic rule  (call it  synt-terminate )
of which I ask above, hidden somewhere, being not a Language data, 
and which cannot be verified.
Imagine that this hidden part is put fixed for ever,  and all the rest
to be developed as libraries of functions which provide a size function
or an help function in various situations, thus reducing a termination
proof to  synt-terminate. I wonder what might be the consequences.

What is the Agda approach? where to read about this?

Thanks,

------
Sergei


 
> 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 ...".
[..]