[Agda] termination proofs

Serge D. Mechveliani mechvel at botik.ru
Sat Sep 22 15:05:56 CEST 2012

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