[Agda] difficult termination

[Martin Escardo]

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

Martin