[Agda] Running a classical proof with choice in Agda

[Martin Escardo]

A reply, together with an Agda question, follow.

On 09/05/11 11:13, Thierry Coquand wrote:
>> A more general question: Implementing Markov's principle in a naive way destroys termination for open terms. Is this avoided here? I suspect not...
>
>   I expect this extension to be SN also for open terms. At least we had a version (less elegant)
> of double negation shift that was SN in
>
> A proof of strong normalisation using domain theory.
> Logical Methods in Computer Science 3(4): (2007)
>
> and the same method (refinement of Ulrich Berger's) should apply here.

Yes, Thierry is right that one can write the proof terms for DNS 
(J-shift here) using Berger's method, and I should eventually do this 
(and I had in mind to do this), so that all open terms are SN.

For the moment, I don't think SN holds for all open terms. A potential 
counter-example is the file ProgramsWithoutSpecification.agda provided 
in the zip file given in the website: this exhausts the heap when I try 
to compile it, although all closed instances of this run in the module 
Examples.agda normalize.

I take the opportunity to make a general Agda question, that hopefully 
somebody in the Agda list can answer. In order to try to make 
ProgramsWithoutSpecification.agda compile, I tried to replace the 
definition of J-∀-shift-selection in the module 
Infinite-J-Shift-Selection.agda by a postulate, assuming that evaluation 
would stop when the uninterpreted term J-∀-shift-selection is 
encountered. However, with this not only 
ProgramsWithoutSpecification.agda still doesn't compile, but also 
Examples.agda now fails to compile!

PUZZLED!

The reason I am puzzled is that when we replace this by a postulate, 
termination checking gets enabled everywhere, but now a module that used 
to compile exhausts the heap! What is going on?

The reason I wanted to do this postulated version was to normalize the 
extracted program, with a constant for the DNS, to see what it looks like!

Martin
-- Appendix (with 4GB of memory):
mhe at escardo-desktop:~/beos/agda/postulate$ agda Examples.agda
Checking Examples (/home/mhe/beos/agda/postulate/Examples.agda).
Checking FinitePigeon (/home/mhe/beos/agda/postulate/FinitePigeon.agda).
Checking InfinitePigeon (/home/mhe/beos/agda/postulate/InfinitePigeon.agda).
Checking Logic (/home/mhe/beos/agda/postulate/Logic.agda).
Finished Logic.
Checking LogicalFacts (/home/mhe/beos/agda/postulate/LogicalFacts.agda).
Finished LogicalFacts.
Checking Two (/home/mhe/beos/agda/postulate/Two.agda).
Checking Equality (/home/mhe/beos/agda/postulate/Equality.agda).
Finished Equality.
Finished Two.
Checking Naturals (/home/mhe/beos/agda/postulate/Naturals.agda).
Finished Naturals.
Checking Addition (/home/mhe/beos/agda/postulate/Addition.agda).
Finished Addition.
Checking Order (/home/mhe/beos/agda/postulate/Order.agda).
Finished Order.
Checking Cantor (/home/mhe/beos/agda/postulate/Cantor.agda).
Finished Cantor.
Checking JK-Monads (/home/mhe/beos/agda/postulate/JK-Monads.agda).
Finished JK-Monads.
Checking JK-Choice (/home/mhe/beos/agda/postulate/JK-Choice.agda).
Checking JK-LogicalFacts 
(/home/mhe/beos/agda/postulate/JK-LogicalFacts.agda).
Finished JK-LogicalFacts.
Checking Choice (/home/mhe/beos/agda/postulate/Choice.agda).
Finished Choice.
Checking Infinite-JK-Shifts 
(/home/mhe/beos/agda/postulate/Infinite-JK-Shifts.agda).
Checking Infinite-J-Shift-Selection 
(/home/mhe/beos/agda/postulate/Infinite-J-Shift-Selection.agda).
Checking Finite-JK-Shifts 
(/home/mhe/beos/agda/postulate/Finite-JK-Shifts.agda).
Finished Finite-JK-Shifts.
Finished Infinite-J-Shift-Selection.
Finished Infinite-JK-Shifts.
Finished JK-Choice.
Finished InfinitePigeon.
Checking Finite (/home/mhe/beos/agda/postulate/Finite.agda).
Finished Finite.
Finished FinitePigeon.
agda: out of memory (requested 2097152 bytes)
mhe at escardo-desktop:~/beos/agda/postulate$