[TYPES] What's a program? (Seriously)

[streicher at mathematik.tu-darmstadt.de]

Indeed, "macro" is a bad wording for translational semantics.
Most effects can be explained by such a tranlation inluding continuation
which are discussed here.
But not all of them as e.g. various kinds of nondeterminism or probability.

Also the more refined model constructions of Krivine cannot be explained
this way, e.g. when he introduces a kind of quote for realizing dependent
choice. But one can avoid this using bar recursion which is nothing but an
instance of general recursion in the target language.
This, however, does not apply to his most recent work covering full AC
where he introduces extensions of lambda calculus which cannot be
explained by translation to pure functional programming.

As long as one does not reason about programs extracted from classical
proofs it is no problem if they are cluttered with such fancy constructs.
But if one does it becomes a nightmare since one does not know how to do
this. That is a problem already for continuations though there exist
axiomatizations for them.

Therefore, the 'unwinders' rather follow the path of negative translation
followed by some functional interpretation. But as soon as you go beyond
Pi^0_2 the negative translation of a meaningful statement becomes fairly
obscure. In any case it is very different from the original statement
understood constructively.

A typical example is the socalled Specker phenomenon. When you classically
prove the existence of a real number then often you can extract a
computable Cauchy sequence for which there does not exist a computable
modulus of convergence meaning that you can't extract sufficiently good
approximations.

Thus, all this extraction business works only for Pi^0_2 sentences. But
for those ZFC is conservative over ZF for which ordinary control operators
work!

Thomas