The Coq mailing list

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

Dear Xavier,

I agree, the idea of oracle (here an oracle for ∑⁰₁-problems) looks
like a good way to describe the kind of non-recursive function that
principles such as LPO assert to exist (and then, rephrased in these
terms, bar recursion is an algorithm that computes approximations of
such oracle).

Reflecting about your remark on alternate models of computation,
alluding I guess to my paragraph on Krivine's realizability, I would
like to say with hindsight that my analysis was too sketchy.

In particular, if callcc adds an instruction to lambda-calculus, I
would not say that it fundamentally changes the model of computation
as everything that can be said about lambda-calculus + callcc can
already be said in lambda-calculus (hence in Turing machines) up to a
continuation-passing-style translation. In this translation, what
happens is not a change of model but the new fact that a callcc
program takes (implicitly) an evaluation context as extra argument.

In particular, the inconsistency of Church's thesis and LPO is not
about a different model of computation, as I might have let it
thought, but more about a different specification of functions. In
the presence of callcc, even though there is a new instruction in the
concrete language, the model of computation is still fundamentally the
one of recursive functions. So what would have to be changed in the
presence of LPO or callcc is instead the statement of Church's thesis,
from:

  ∀f:nat→nat, ∃m:TM, ∀a:nat, m(⌊a⌋)↓⌊f(a)⌋

to something about nat→(nat→A)→A for arbitrary A, so, thinking aloud,
presumably of the form:

  ∀f:nat→nat, ∃m:TM, ∀a:nat, ∀m':TM, m'(⌊f(a)⌋)↓ → m(⌊a⌋,m')↓

As a double-check, let's try to apply this variant of Church's thesis to
the LPO-and-unique-choice-based proof of

  {f:TM→option nat | ∀m, match f m with Some n ⇒ terminated m n | None ⇒ ∀n, 
¬terminated m n}

and, indeed, the statement that we get does not look anymore amenable
to the diagonal argument showing the indecidability of the halting
problem. That is, continuing elaborating on this intuition, the code
of the function f given by this modified Church Thesis (moreover
reminding that this f is itself an evolving approximation of the
oracle), does not decide the halting problem, but decides the halting
problem only in the context of any other recursive computation relying
on the halting problem. In any case, I believe that there would be an
agreement that this is something different than "deciding the halting
problem", and that this continuation-based alternative statement is
actually not any more about callcc either since we could have produced
the same conclusion by reasoning up to continuation-passing-style
translation.

Maybe a conclusion of the exchange would be that there is still
nevertheless an alternative to the common thinking that an oracle
takes decisions about infinity: it is enough to take good-enough
finite decisions in any finite context to let others believe that this
is about knowing everything in advance. Would you e.g. agree with this
kind of slogan?

Best,

Hugo

PS: In any case, thanks for the stimulating discussion.

On Fri, Feb 16, 2024 at 06:11:28PM +0100, Xavier Leroy wrote:
> Dear Hugo,
> 
> Thanks a lot for your detailed analysis !  The interpretation of classical
> logic using control operators like call/cc is now well known, and I always
> enjoy explaining it to students, but the concept of "bar recursion" and its
> "implementation" using local state were new to me.
> 
> Computability theory gives precise, universally-adopted definitions of
> computable functions and of decision procedures.  While I'm completely open 
> to
> other models of computation than Turing machines, and spent much research 
> and
> teaching effort on those alternate computation models, I'd rather stick to 
> the
> standard meaning of "decision procedure", and avoid claims such as "call/cc
> does decide the halting problem", which just reflect poorly on this 
> community.
> 
> Computability theory also provides a concept that might help answer Mukesh's
> initial question: the notion of an oracle (https://en.wikipedia.org/wiki/
> Oracle_machine).  The "sig_forall_dec" axiom just adds to Coq's language an
> oracle that solves a number of problems, including the halting problem, but 
> not
> all undecidable problems, if I understand correctly.  The Coquelicot
> formalization of reals uses it to obtain (among other things) a 
> Boolean-valued
> equality test between real numbers, which cannot be defined in plain Coq, as
> equality between two real numbers is an undecidable problem.
> 
> Hope this helps,
> 
> - Xavier Leroy
> 
> On Thu, Feb 15, 2024 at 10:34 AM Hugo Herbelin <Hugo.Herbelin AT inria.fr> 
> wrote:
> 
>     I'm told that "(P n \/ ~ P n)" is confusing in the paragraph
>     below.
> 
>     > 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). (...)
> 
>     It should be read it either as Q \/ ~Q for general Q, or as
>     ({n | ~P n} + {forall n, P n}) for the P that was under discussion
>     (ignoring the ability to then extract an "option nat" from it, that
>     the other message discusses).
> 
>     Sorry.
> 
>     Hugo
>