[Agda] difficult termination

[Sergei Meshveliani]

Dear all,

I am thinking of the practical termination proof possibility in Agda.

In my current practice with computer algebra, all termination proofs are
as follows.

1) Syntactic:  the built-in rule of Agda when in each recursive call of
the function some argument is syntactically smaller (in a certain
"subterm" ordering) than in the current call. 

2) By the counter.

For example, for a certain recursively defined function  f : Bin -> Bin,
I prove termination by rewriting f as follows:

  f x =  aux x (toNat x) ≤-refl
    where
    aux : (x : Bin) -> (cnt : Nat) -> toNat x ≤ cnt -> Bin
    aux x cnt xN≤cnt =  
                     ...

When  cnt  is  0,  it is derived from  xN = toNat x ≤ cnt  that  
x ≡ 0#,  and this is the base of recursion.
Otherwise the LHS is
                  aux x (suc cnt) xN≤cnt',

and the recursive call is
                       aux y cnt yN≤cnt
 
cnt  is reduced by one,  and  y  is so that  xN ∸ yN ≥ 1  for  
                                                    yN = toNat y.

So that the first argument is reduced at least by one, and  yN ≤ cnt  is
derived from  xN≤cnt'.
And this recursive call of  aux  proves termination for Agda.

Probably, such proofs by the counter are possible only for primitively
recursive functions. 
For example, for the above  f,  (toNat x) is the upper bound for the
number of recursive calls of  aux.

Do I mistake?

Further, the Ackermann's function 
 
 ack : ℕ → ℕ → ℕ
 ack 0       m       =  suc m
 ack (suc n) 0       =  ack n 1
 ack (suc n) (suc m) =  ack n (ack (suc n) m)

is not primitively recursive. But Agda sees its termination by the
syntactic comparison rule.

Can anybody give a _simple_ example of a terminating algorithm which
is difficult or impossible to write in Agda with providing termination
proof for Agda ?

Regards,

------
Sergei