Why do constructivists not seem to care too much about call/cc

Question

So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't seem to find a flaw with it. However I can't really seem to see anyone else talking about it. It seems void of discussion. What gives?

It seems to me that if you have a construction like $f : \neg(\neg P)$ in some context then 1 of two things is true. Either you have access to an instance $\bot$ somehow in the current context in which case control flow would never reach here and we are safe to assume whatever OR given that $f : \neg(\neg P)$ means $f : (P \to \bot) \to \bot$ the only way $f$ can return $\bot$ is by constructing an instance of $P$ and applying it two it's argument (an instance of $P \to \bot)$. In such a case there was already SOME way of constructing an instance of $P$; it seems reasonable for call/cc to pull this construction out for me. My reasoning here seems somewhat suspect to me but my confusion still stands. If call/cc isn't just creating an instance of $P$ out of thin air (I don't see how it is) then what is the issue?

Do some well typed terms not containing call/cc not have normal forms? Is there some other property of such expressions that causes them to be suspect? Is there any noted reason why a constructivist shouldn't like call/cc?

Answer 1

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive mathematician.

To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc:

1. We provide a function $f$ which allegedly proves $\lnot p$. In reality $f$ is a bag of tricks.
2. If anyone ever applies $f$ to a proof of $p$, then $f$ unleashes call/cc to roll back time, and with a proof of $p$ in hand, changes its mind about $p \lor \lnot p$: this time claiming that it is a proof of $p$.

The constructive understanding of disjunction is algorithmic decidability, but the above is hardly making any decisions. As a test, a constructive mathematician might ask you how call/cc helps prove that every Turing machine halts or diverges. And what is the program witnessing this fact? (It ought to be the Halting Oracle.)

Answer 2

As you note, there is a possible constructive interpretation of classical logic in this sense. The fact that classical logic is equiconsistent with intuitionistic logic (say, Heyting Arithmetic) has been known for quite some time (already in 1933, e.g. Godel) using a double negation translation.

By a more sophisticated argument, it can be shown that Peano Arithmetic is conservative over HA for $\Pi^0_2$ statements. The essence of the result is that the classical proofs of $\Pi^0_2$ involving $\mathrm{call/cc}$ have the same computational content as a statement without that construct (by a CPS transformation).

However this is not true for statements above $\Pi^0_2$: statements in $\Sigma^0_3$, provable in PA, may not have a normal form amenable to extracting a witness! Computer scientists may not care about computing with proofs at this level, but it is somewhat inconvenient for philosophical considerations: have we proven the existence of something, or not?

I think this summarizes why "fixing" non-constructive logic by addition of $\mathrm{call/cc}$ may be unsatisfactory.

That being said, there is a lot of work exploring the computational aspects of computation within the "classical Curry-Howard" framework, e.g. the Krivine Machine, the Parigot calculus ($\lambda\overline{\mu}\tilde\mu$) and many others. See here for an overview.

Finally, it might be useful to note that while the situation is rather well understood in the predicate calculus and arithmetic cases, more powerful theories are much less explored. For example, IIRC, ZFC is conservative over IZF for $\Pi^0_2$ sentences as well (ZFC is conservative over ZF for arithmetic sentences, and ZF is conservative over IZF), which suggests there is a computational meaning for the axiom of choice. However this is very much an active field of research (krivine, Berardi et al.)

Edit: A very relevant question on mathoverflow appears here: https://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language

Answer 3

I agree with both Andrej's and Cody's answer. However, I think it is also worth mentioning why constructivists should care about control operators (call/cc).

These operators are usually connected to classical logic because when people looked at their typing rules (Felleisen, Griffin) they noticed that the types have the form of Peirce's Law or double-negation elimination ($\neg\neg P\vdash P$). Nevertheless, control operators were invented in the untyped setting of the Scheme programming language. Their purpose was to be able to enrich the programming language: instead of writing programs in continuation-passing style, one would be able to write programs in direct style using control operators.

One gain in using control operators in Proof Theory is the methodological one: instead of using a double-negation- and A-translation to extract programs from proofs of $\Pi^0_2$-theorems of Classical Arithmetic, one would use a control operator and perform direct rewriting normalization on the proof.

Another gain a constructivist should care about is that control operators show a way how to build a Curry-Howard extension of intuitionistic logic which is still constructive. For example, limiting the $P$ from the double negation elimination law to the $\Sigma^0_1$-class of formulas, allows to have a typed control operator that can prove for example Markov's Principle or the Double Negation Shift. These principles are usually not accepted by constructivists, but for hardly a good reason, since it is known that they do not destroy the Disjunction and Existence properties when added to intuitionistic logic.