What fails when using call/cc as realizer of the Peirce formula

Question

Define the axiom constants $p_{A,B}^{((A\rightarrow B)\rightarrow A)\rightarrow A}$ as realizers of the Peirce formula, and $f_A^{\bot\rightarrow A}$ as realizers of the Ex Falso Quodlibet. Then $p_{A\vee\lnot A,\bot}^{(\lnot (A\vee\lnot A)\rightarrow(A\vee\lnot A))\rightarrow(A\vee\lnot A)}\lambda_{u^{\lnot(A\vee\lnot A)}} . f_{A\vee\lnot A}^{\bot\rightarrow (A\vee\lnot A)} u (\vee_+^{\lnot A\rightarrow A\vee\lnot A} \lambda_{v^A}.u(\vee_+^{A\rightarrow A\vee\lnot A} v))$ proves the law of the excluded middle $A\vee\lnot A$.

Now, the function call-with-current-continuation, or short call/cc, in scheme, has the signature of $p$ (in Haskell, this one is replaced by its negative translation). The rest of the above term is covered by the Curry Howard Isomorphism, and therefore, using an instance of call/cc as a realizer of $p$ gives a program of type $A\vee\lnot A$.

Of course, something that one expects in programs extracted from constructive proofs must fail here, otherwise one could decide every proposition $A$. I was just wondering, what exactly it is.

Scheme's call/cc will fail with this term, since the continuation is called twice - but that is not really a problem, since one could just copy the whole context of the continuation and bind it into a new function which can then be called multiple times - that would produce a lot of overhead, but still would provide an effective algorithm which must not exist.

And having a call/cc in the beginning of a term does also not seem very useful, but inside another term, this should not be a problem.

Then, maybe in this context we must not use $f$. Normally, instances $f$ of the Ex Falso Quodlibet must never be called, and in this term, it could be called (and would give an instance of $A\vee\lnot A$) - but on the other hand, the continuation is called twice before ever coming to call $f$, so I am not sure whether this is actually the problem.

And then of course, $u$ is called twice, once with an instance of $A\vee\lnot A$ that eliminates to $A$, and once with an instance that eliminates to $\lnot A$. So probably calling $u$ with both outcomes of $A\vee\lnot A$ may produce endless loops or strange behaviour.

As I said, I am not sure what exactly fails here. Does anybody know?

Answer 1

I'm not sure what you mean by 'fail' here.

It is true, as you say, that classical proofs can exhibit behaviour that constructive proofs can't. In general, it's no longer true that a term of type A reduces to a constructive proof of the proposition A -- but that's only to be expected. Proof-terms in classical logic are strongly normalizing, though (if you're sensible about it), so there are no 'endless loops'. The difference is that, in general, such proof-terms can have more than one distinct normal form, and there is no good reason to pick one over any other.

You say

Scheme's call/cc will fail with this term, since the continuation is called twice

which is not true. Scheme continuations can be called any number of times. Also

Normally, instances f of the Ex Falso Quodlibet must never be called

is not true either. The ex falso sequitur quodlibet term discards the current continuation and returns its argument to the top level.

In terms of behaviour, functional programs use their continuations exactly once. Allowing EFSQ means that a program can discard, but not copy, its continuation. Admitting the double-negation rule duplex negatio affirmat allows programs to use their continuations an arbitrary number of times, including zero (or not, for Peirce's law). This corresponds to allowing exactly one, at most one and arbitrarily many formulas on the right-hand side of the turnstile in sequent calculus.

What the excluded-middle term does is this: it pretends to be a proof of not-A until such time as it is presented with a proof of A, whereupon it travels back in time (so to speak) and returns that proof of A instead (Wadler has a paper about this, I think). In general, classical proofs behave more like systems of communicating processes than functional programs. There are a couple of papers by Barbanera and Berardi that go into this in detail.