Nottingham FP Lab Blog

Continuations and classical logic

by Hancock on December 9, 2007.
Tagged as: Lunches.

Hank wrote on the board an interesting universe of “classical propositions”, due to Erik Palmgren. (It is mentioned in “25 years of constructive type theory.) One supposes given a universe (U,T) of small sets, and then inductively defines a set of codes Unotnot. This has a ground code G(a) for each a : U, and is closed under 0, conjunction, implication, and universal quantification over any small set. Then one defines for any small set A a decoding function T_A : Unotnot -> U. For example T_A(0) = A, T_A(G(a)) = (T(a) -> A) -> A,
and T_A does the obvious things on conjunction, implication, and universal quantification.

Erik’s universe behaves like an embedding of classical logic into type-theory. The inspiration for it is called “Friedman’s A-translation”, which is in fact a translation of classical logic into *minimal logic* — that is, intuitionistic logic without ex-falso-quodlibet. Roughly speaking, Friedman’s translation is the much older Godel-Gentzen “double negation translation”, with the absurd proposition 0 replaced by a random proposition A. What is so clever about this translation is firstly its extreme simplicity, and secondly that it allowed Friedman to perform a rather magical trick, showing that in common situations, classical and intuitionistic systems prove the same “Pi02″ formulas. These are
formulas of the form $\forall x. \exists y. P(x,y)$ , where P is quantifier free. Such statements include the statement that a Turing machine defines a total function. Another example is the statement that a sequence of numbers increases infinitely often.

Everybody who has heard of the continuation monad, or the continuation transform(s) should at this point be suspicious that they must have something to do with the A-translation. The continuation monad is in some sense the mother of all monads — – you can get an inkling of this merely by contemplating the type of the bind operator for an arbitrary monad M, namely (>>=) : M a -> (a -> M b) -> M b. Quite obviously M b is some kind of “result” type. Continuations are used for all kinds of things: to enforce particular evaluation orders for programs in the lambda-calculus (the so-called CBV and CBN transforms); to re-express recursive programs in a tail-recursive form; as well as to encode all kinds of bizarre “jumps”, “exits” and what-have-you.

Thorsten spoke for a bit about situations in which classical systems are *not* conservative over their intuitionistic versions for Pi02 formulas. He was particularly interested in systems of iterated inductive definitions, where the mu-bound variables can interact and “feedback” in rather fascinating ways. The work of Robert Lubarsky on the modal mu-calculus may be relevant in this connection.

The situation is indeed rather obscure. The double-negation translation does not work in the systems ID1, ID2, … because the ground formulas are no longer decidable. Yet, the really interesting step is that from ID1 to ID2. There is good reason to believe that the notion of classical truth in ID1 can be explained in constructive terms (though by something more subtle than the double negation translation — namely a game-theoretic translation). This does *not* seem to be the case for ID2. The importance of the step from ID1 to ID2 has been stressed by Thierry Coquand.

Fortuitously, our seminar speaker later in the afternoon, Monika Seisenberger from Swansea, showed us some technology based on the A-translation, for extracting algorithms from classical proofs. Indeed, she showed us it working to give a tail-recursive version of the reverse function. This machinery works in the MINLOG system, developed by Schwichtenberg and others (like Monika) at Munich.