Curry-Howard and programs from non-constructive proofs

Question

This is a follow up question to

What is the difference between proofs and programs (or between propositions and types)?

What program would correspond to a non-constructive (classical) proof of the form $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$? (Assume that $T$ is some interesting decidable relation e.g. $e$-th TM does not halt in $k$ steps.)

(ps: I am posting this question partly because I am interested in learning more about what Neel means by "the Godel-Gentzen translation is a continuation-passing transformation" in his comment.)

Answer 1

This an interesting question. Obviously one can't expect to have a program that decides for each $e$ whether $\forall k T(e, k)$ holds or not, as this would decide the Halting Problem. As mentioned already, there are several ways of interpreting proofs computationally: extensions of Curry-Howard, realizability, dialectica, and so on. But they would all computationally interpret the theorem you mentioned more or less in the following way.

For simplicity consider the equivalent classical theorem

(1) $\exists i \forall j (\neg T(e, j) \to \neg T(e, i))$

This is (constructively) equivalent to the one mentioned because given $i$ we can decide whether $\forall k T(e, k)$ holds or not by simply checking the value of $\neg T(e, i)$. If $\neg T(e, i)$ holds then $\exists i \neg T(e, i)$ and hence $\neg \forall i T(e, i)$. If on the other hand $\neg T(e, i)$ does not hold then by (1) we have $\forall j (\neg T(e, j) \to \bot)$ which implies $\forall j T(e, j)$.

Now, again we can't compute $i$ in (1) for each given $e$ because we would again solve the Halting Problem. What all interpretations mentioned above would do is to look at the equivalent theorem

(2) $\forall f \exists i' (\neg T(e, f(i')) \to \neg T(e, i'))$

The function $f$ is called the Herbrand function. It tries to compute a counter example $j$ for each given potential witness $i$. It is clear that (1) and (2) are equivalent. From left to right this is constructive, simply take $i' = i$ in (2), where $i$ is the assumed witness of (1). From right to left one has to reason classically. Assume (1) was not true. Then,

(3) $\forall i \exists j \neg (\neg T(e, j) \to \neg T(e, i))$

Let $f'$ be a function witnessing this, i.e.

(4) $\forall i \neg (\neg T(e, f'(i)) \to \neg T(e, i))$

Now, take $f = f'$ in (2) and we have $(\neg T(e, f'(i')) \to \neg T(e, i'))$, for some $i'$. But taking $i = i'$ in (4) we obtain the negation of that, contradiction. Hence (2) implies (1).

So, we have that (1) and (2) are classically equivalent. But the interesting thing is that (2) has now a very simple constructive witness. Simply take $i' = f(0)$ if $T(e, f(0))$ does not hold, because then the conclusion of (2) is true; or else take $i' = 0$ if $T(e, f(0))$ holds, because then $\neg T(e, f(0))$ does not hold and the premise of (2) is false, making it again true.

Hence, the way to computationally interpret a classical theorem like (1) is to look at a (classically) equivalent formulation which can be proven constructively, in our case (2).

The different interpretations mentioned above only diverge on the way the function $f$ pops up. In the case of realizability and the dialectica interpretation this is explicitly given by the interpretation, when combined with some form of negative translation (like Goedel-Gentzen's). In the case of Curry-Howard extensions with call-cc and continuation operators the function $f$ arises from the fact that the program is allowed to "know" how a certain value (in our case $i$) will be used, so $f$ is the continuation of the program around the point where $i$ is computed.

Another important point is that you want the passage from (1) to (2) to be "modular", i.e. if (1) is used to prove (1'), then its interpretation (2) should be used used in similar way to prove the interpretation of (1'), say (2'). All the interpretations mentioned above do that, including the Goedel-Gentzen negative translation.

Answer 2

It's fairly well-known that classical and intuitionistic arithmetic are equiconsistent.

One way of showing this is via the "negative embeddings" of classical logic into intuitionistic logic. So, suppose $\phi$ are formulas of classical first-order arithmetic. Now, we can define a formula of intuitionistic logic as follows:

$$ \begin{array}{lcl} G(\top) & = & \lnot\lnot\top \\ G(\phi \land \psi) & = & \lnot\lnot(G(\phi) \land G(\psi)) \\ G(\bot) & = & \lnot\top \\ G(\lnot\phi) & = & \lnot G(\phi) \\ G(\phi \vee \psi) & = & \lnot(\lnot G(\phi) \land \lnot G(\psi)) \\ G(\forall x.\;\phi) & = & \forall x.\; \lnot\lnot G(\phi) \\ G(\exists x.\;\phi) & = & \lnot \forall x.\; \lnot(G(\phi)) \\ G(P) & = & \lnot\lnot P \\ \end{array} $$

Note that $G(\phi)$ is basically a homomorphism that sticks in extra not-not's everywhere, except that at disjunctions and existentials, it uses de Morgan duality to turn them into conjunctions and universals. (I'm pretty confident this is not the exact Godel-Gentzen translation, since I cooked it up for this answer -- basically anything you write using double-negation + de Morgan duality will work. This variety actually turns out to be important for computational interpretations of classical logic; see below.)

First: It's obvious that this translation preserves classical truth, so that $G(\phi)$ is true if and only if $\phi$ is, classically speaking.

Second: It's less obvious, but still the case, that for formulas in the $\forall, \implies, \land, \lnot$ fragment, provability in intuitionistic and classical logic coincide. The way to prove this is to first look at formulas drawn from this grammar:

$$ \newcommand{\bnfalt}{\;\;|\;\;} \begin{array}{lcl} A,B & ::= & \forall x.\;A(x) \bnfalt A \implies B \bnfalt A \land B \bnfalt \lnot A \bnfalt \lnot\lnot P \end{array} $$

And then we can prove as a lemma (by induction on $A$) that $G(A) \implies A$ is derivable intuitionistically. So now, we can show the equiderivability of negative formulas by doing an induction over the structure of the proof (in, say, the sequent calculus) and use the previous lemma to simulate the law of the excluded middle.

So, how should you think about this intuitively?

• First, the proof-theoretic view. If you look at the rules of the sequent calculus, you can see that the only place classical and intuitionistic logic seriously differ is in the rules for disjunction and existentials. So we are using this fact to show that that proofs in one logic of these formulas can be translated to proofs in the other. This shows how to think of constructive logic as an extension of classical logic with the two new connectives $\exists$ and $\vee$. What we call "classical existence" and "classical disjunction" were just abbreviations involving $\forall$, conjunction, and negation, and so to talk about actual existence we needed to introduce new connectives.

• Second, there's a topological view. Now, the model of a classical logic (as a family of sets) is a Boolean algebra (ie, a family of subsets closed under arbitrary unions, intersections and complements). It turns out that the model of intuitionsitic logic is as a topological space, with the propositions being interpreted as open sets. Them the interpretation of negation is the interior of the complement, and then it's easy to show that $\lnot\lnot\lnot P = \lnot P$, which means that double-negation sends us into the smallest clopen covering each open --- and the clopens form a Boolean algebra.

Now, thanks to Curry-Howard, we know how to interpret proofs in intuitionistic logic as functional programs. So, one possible answer (but not the only one) to the question of "what is the constructive content of a classical proof?" is the following:

The computational content of a classical proof is whatever the computational content of the translation of its proof (according to the negative translation) is.

So let's look at the translation of $G(A \vee \lnot A) = \lnot(\lnot G(A) \land \lnot\lnot G(A))$. So this says that the constructive content of the excluded middle is the same as saying that it's not the case that $\lnot P$ and and $\lnot\lnot P$ hold -- ie, noncontradiction. So in this sense, there's not actually very much computational content to the law of the excluded middle.

To see what it is concretely, recall that constructively, negation is defined as $\lnot A == A \implies \bot$. So this formula is $((G(A) \implies \bot) \land ((G(A) \implies \bot) \implies \bot)) \implies \bot$. The following bit of Ocaml code will illustrate:

type bot = Void of bot
type 'a not = 'a -> bot

let excluded_middle : ('a not * 'a not not) not = fun (u, k) -> k u 

That is, if you get not-A and not-not-A, you can just pass the first negation to the second to derive the contradiction you want.

Now, what is a continuation passing-style transformations?

• A continuation of type $\tau$ is something that takes a value of type $\tau$ and computes a final answer from it.
• Continuations are used to model program contexts. That is we might have a term $3+5$ evaluating as part of a much larger program $C[3+5]$. All that stuff around it will take the result of computing $3 + 5$ and compute the final answer.
• So you can think of a continuation of type $\tau$ as a function $\tau \to \alpha$, where $\alpha$ is whatever the answer type is.
• So if you have a program $e$ of type $\tau$, we can "CPS-convert" it by finding a term of type $(\tau \to \alpha) \to \alpha$, which will end up passing whatever $e$ would have computed to its continuation. (Basically, this just makes control flow explicit.)
• But we have to do this hereditarily, so that every subterm of the program has made its continuation explicit.

Now,

• The negative translation basically hereditarily sends $\phi$ to $\lnot\lnot\phi$.
• However, while our translation uses negation, it never actually eliminates the false proposition -- so the translation works parametrically in that proposition.
• In particular, we can replace $\bot$ with any answer type $\alpha$.
• So we hereditarily replace $\phi$ with $(\phi \to \alpha) \to \alpha$.
• This is a CPS transformation.

I saw "a" CPS transformation, since as I mentioned earlier, there are many negative translations which let you prove this theorem, and each one corresponds to a different CPS trasnformation. In operational terms, each transformation corresponds to a different evaluation order. So there is no unique computational interpretation of classical logic, since you've got choices to make and the difference choices have very different operational characteristics.

Answer 3

There are whole conferences on the subject of non-constructive proofs as programs, and I am no expert on the subject. Above, Neel Krishnaswami alluded to a longer answer he is preparing, which, judging from his work here, will be excellent. This is just a taste of an answer.

It turns out the the type of call-with-current-continuation corresponds to the proposition known as Peirce's law, which can be used to prove the Law of Excluded Middle ($\forall P, P \lor \lnot P$). An LEM program can be written using callcc. In Coq:

Set Implicit Arguments.

Axiom callcc : forall (A B : Set), ((A -> B) -> A) -> A.

Lemma lem : forall (A B:Set), sum A (A -> B).
Proof.
  intros.
  eapply callcc.
  intros H.
  right.
  intros.
  apply H.
  left.
  assumption.
Defined.

Recursive Extraction lem.

gives the O'Caml code:

type ('a, 'b) sum =
  | Inl of 'a
  | Inr of 'b

(** val callcc : (('a1 -> 'a2) -> 'a1) -> 'a1 **)

let callcc =
  failwith "AXIOM TO BE REALIZED"

(** val lem : ('a1, 'a1 -> no) sum **)

let lem =
    callcc (fun h -> Inr (fun h0 -> h (Inl h0)))

The cleanest introduction to this I have seen is in Tim Griffin's "A formulae-as-types notion of control".