The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Xavier,

> The LPO axiom implies that the halting problem is decidable. (Just take P n 
> =
> "my Turing machine has not terminated yet after n steps".) You're not saying
> that callcc decides the halting problem, right?

It depends on what you mean by "decide".

What we have is a callcc-based computational content to an LPO-based
proof of the decidability of the halting of any Turing Machine.

Then, if, by "deciding" is meant the existence of the code of a
recursive function taking a machine as input and returning a boolean
such that the boolean is true iff the machine terminates, we would
additionally need a form of the axiom of Church's thesis. If I'm
correct, all basic forms of it are consistent with plain Coq (see
e.g. Pédrot's great talk on "quote" in Coq [1]) but inconsistent with
the corresponding form of LPO (by "form" I mean whether we use
"exists" or "sig" in various places of the statement).

This inconsistency of Church's thesis and LPO is actually reassuring:
we added instructions to the language, so we would need another
language of programs than recursive functions to take into account the
presence of LPO. This is e.g. the step taken by Jean-Louis Krivine who
extracts callcc-based programs from classical proofs [2].

This suggests another definition of "deciding" which is the ability to
"approximate" the truth of (P n \/ ~ P n), in the sense of being able
to locally produce a witness of (P n \/ ~ P n) in the context of any
other proof p that relies on (P n \/ ~ P n). Then, in this sense,
emphasized by Jason, the answer is yes, callcc "decides" the halting
problem. In particular, if p is the proof of a ∑⁰₁-formula, where
∑⁰₁-formulas are the analogous in logic of base types such as int or
bool in programming, the callcc-based proof of LPO will have taken
enough local decisions so that, if the evaluation terminates, it
produces a correct and effect-free value of type the given
∑⁰₁-formula.

Best,

Hugo

PS: My callcc-based explanation of LPO somehow introduced confusion as
there are actually different forms of LPO (in Prop or in Type) and I
gave an interpretation for the simplest of those, the one in Prop,
while the original question was rather about the version in Type. I'm
coming back to it in a different message.

[1] https://www.pédrot.fr/slides/deducteam-12-23.pdf
[2] e.g. https://www.irif.fr/~krivine/articles/Luminy04.pdf