[Agda] difficult termination

[Sergei Meshveliani]

On Mon, 2017-11-20 at 20:34 +0000, Martin Escardo wrote:
> 
> On 20/11/17 18:57, mechvel at botik.ru wrote:
> > Thank you.
> > Yes, I thought of Markov's principle.
> > It is good.
> > But P is still rather arbitrary.
> > It is desirable to have an example in which P is as concrete
> > as possible.
> > May be, some modification of Ackermann's function is possible.
> 
> It won't be so easy. You are asking questions about the proof theory of 
> Agda / Martin-Lof Type Theory.
> 
> If you don't have any universe (type "Set") or fancy inductive types 
> (defining universes), the expressivity of the language is like that of 
> Goedel's system T regarding what functions N->N you can defined 
> (including, in particular, Ackermann's function, as you say).
> 
> Once you start having universes Set1, Set2, Set3, ... you start 
> increasing the amount of definable functions N->N. The termination 
> checker by itself won't believe your definitions automatically, though, 
> as you increase the universes you allow yourself to use. Instead, you 
> will have to provide bonafide, rather subtle, means of definition by 
> yourself.
> 
> Also, there is another subtle point: the fact that you can't prove 
> something like "for all ..., blah", doesn't mean that you will be able 
> to come up with an example of a "..." such that "not blah".


This can be some P for which  \exists P  is proved non-constructively
and is very difficult to prove constructively.
For example, Higman's lemma about a certain repetition existing in any
infinite sequence of words. But Higman's lemma has a simple enough proof
in Agda -- for the alphabet of two letters (see Sergei Romanenko's
code). Probably general case is not much more complex.  

Primitive recursion is not enough for practical usage of Agda. 
But adding such a simple rule of termination as "argument being a proper
subterm" seems to change the situation greatly.
And I wonder -- how greatly.

I continue programming computer algebra, and wonder: when there will
encounter a practical method, for which I fail with termination proof.

Regards,

------
Sergei