[Agda] difficult termination

[Sergei Meshveliani]

On Mon, 2017-11-20 at 18:57 +0100, Nils Anders Danielsson wrote:
> On 2017-11-20 18:03, Sergei Meshveliani wrote:
> > This can be finding by  searching through  of any  n : ℕ  satisfying
> > some subtle property  P.
> > It needs to be known a non-constructive proof for  ∃ \(n : ℕ) → P n,
> > but a bound for such  x  to be not known.
> > I wonder what might be this example.
> 
> It should not be possible to implement something with the following type
> in Agda (if it is, then that is a bug):
> 
>    (P : ℕ → Set) → (∀ n → Dec (P n)) → ¬ ¬ ∃ P → ∃ P
> 
> This is (one form of) Markov's principle.
> 
> Here is one implementation that Agda rejects:
> 
>    markov : (P : ℕ → Set) → (∀ n → Dec (P n)) → ¬ ¬ ∃ P → ∃ P
>    markov P dec _ = search 0
>      where
>      search : ℕ → ∃ P
>      search n with dec n
>      ... | yes p = n , p
>      ... | no _  = search (suc n)
> 


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.

------
Sergei