[Agda] Running a classical proof with choice in Agda

[Thorsten Altenkirch]

Cool!

Just from a first glance, I am confused by the following

Why has pigeonhole a hidden parameter R which is not referenced in the rest of the type?

I guess the definition of pigeonhole unifies R with the first parameter to Pigeonhole but this should be expressed in the type. 

I suspect it may be better to turn R (i.e. the type of responses for the continuations) into a module parameter instead of threading it through the definitions.

A more general question: Implementing Markov's principle in a naive way destroys termination for open terms. Is this avoided here? I suspect not...

Cheers,
Thorsten

On 9 May 2011, at 10:29, Martin Escardo wrote:

> Dear Agda- and type-theorists,
> 
> Using
> 
>  * Berardi-Bezem-Coquand's functional, or alternatively
> 
>  * Escardo-Oliva's countable product of selection functions,
> 
> for giving a proof term for classical countable choice, we prove the classical infinite pigeonhole principle in Agda: every infinite boolean sequence has a constant infinite subsequence, where the existential quantification is classical (double negated).
> 
> As a corollary, we get the finite pigeonhole principle, using Friedman's A-translation (by hand) to make the existential quantifiers intuitionistic.
> 
> This we can run, and it runs fast enough. The point is to illustrate in Agda how we can get witnesses from classical proofs that use countable choice. The finite pigeonhole principle has a simple constructive proof, of course, and hence this is really for illustration only.
> 
> This can be seen at
> 
> http://www.cs.bham.ac.uk/~mhe/pigeon/
> 
> with nice html formating of the Agda files produced by the Agda system.
> 
> The two little modules that implement the Berardi-Bezem-Coquand and Escardo-Oliva functionals disable the termination checker, but no other module does. The type of these functionals in Agda is the J-shift principle, which generalizes the double-negation shift. More details in the above web page.
> 
> Best wishes,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda