[Agda] Classical Mathematics for a Constructive World
Martin Escardo
m.escardo at cs.bham.ac.uk
Tue Nov 27 22:55:39 CET 2012
On 27/11/12 21:19, Peter Divianszky wrote:
> Still I have questions:
>
> Can your 'pigeonhole' generalized to functions (ℕ → ¬ ¬ ₂)?
Meaning?
> I can't find a transformation from (ℕ → ¬ ¬ ₂) to (¬ ¬ (ℕ → ₂)).
The first person to find such a function was Spector in the late 1950's
or early 1960's. The recursion scheme used to define it is called
(Spector) bar recursion.
Other recursion schemes were given much more recently by
Berardi-Bezem-Coquand (end of last millennium), Berger (early this
millennium), Escardo-Oliva (some years ago).
The Agda pigeon program can run with any of the three in the last
paragraph, and there is a file in which you can choose which one you
want to use. The default choice is selfish.
A tutorial paper about the EO functional is here:
http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/
> Are the spaces (¬ ¬ (ℕ → ₂)) and (ℕ → ¬ ¬ ₂) different?
Very.
> Isn't the latter more "classical"?
What is a classical space?
Best,
Martin
More information about the Agda
mailing list