[Agda] Markov's principle

[Sergei Meshveliani]

On Sat, 2016-06-11 at 16:44 +0400, Sergei Meshveliani wrote:
> People,
> 
> I have a question about Markov's principle for termination proof.
> 
> Several months ago we discussed a simple program  nextPrime  for finding
> a prime natural next to the given prime  p.
> It uses a bound  b  which is simple to prove, but  cnt = b - n  being
> expensive to compare to 0 at run time. 
> 
> In order to have both a termination proof and fast comparison in the
> loop, there were considered a counter, two bounds, and the two search
> loops instead of one. 
> 
> Also Ulf Norell suggested a general approach of a large bound (say
> 2^1000) for the first loop. (I call this unfeasible bound). 
> 
> Now, with using the Markov's principle for termination proof, it is
> possible a simpler program:
> 
>    test  n = p+1, p+2 ...  for primality, and stop when  n  is prime.
> 
> Supposing non-termination leads to contradiction to that  b > p  is
> prime. Hence, the loop terminates.
> 
> So, Markov' principle is replaced in Agda with introducing an unfeasible
> bound and an additional loop
> --- for this particular example.
> 
> Can a replacement of this kind be made universal?
> Is Markov's principle generally replaced in Agda by some approach of the
> above kind?
> 

Probably, it can replace in this way only when there is proved some
bound B for the size of objects being tested in the loop. 

------
Sergei