The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Fri, Feb 16, 2024 at 10:30 PM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

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.

The alternate model of computation I had in mind is just effectful programming, where the execution of a program has visible effects on / interactions with the environment, beyond computing a return value.  This includes control operators as well as state.

It does change the model of computation, compared to what computability theory uses.  Computability theory is interested in pure, mathematical functions and predicates (int -> int or int -> bool) that can be computed by a Turing machine or some equivalent device.  That Turing machines are very imperative doesn't change anything to the fact that computability is a theory of pure computations.

A stateful function such as let r = ref 0 in fun () -> incr r; r! is not a computable function, not because we don't know how to execute it (OCaml does it just fine) but because it is not a mathematical function: its result depends on the calling context, namely on how many times it has been called already.

Likewise, the term call/cc (fun cc => inr (fun a => cc (inl a))) is not a decision procedure because it is not a procedure: its result depends on the calling context, namely how its continuation is going to use its result.

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.

No, CPS transformation is not going to give you a Turing machine that decides whether another Turing machine terminates.

Applied locally to a subterm, CPS transformation changes the type of this term.  So, from a call/cc-based proof of P \/ ~P you get an effect-free proof of the double negation of P \/ ~P, which doesn't compute anything useful on its own.

Using the CPS transformation on your whole proof of a proposition P and applying the resulting CPS term to the identity continuation, you do get an effect-free proof of P if P is simple enough (Pi_0^2 in the case of Friedman's conservativity result).  But forall tm : TuringMachine, terminates(tm) \/ ~terminates(tm) is not Pi_0^2.  So, again, you'll get an effect-free proof of some other property.

Again, this is all perfectly normal, but let's acknowledge these facts instead of claiming that "call/cc decides the halting problem".

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?

Again, this is changing the meaning of "oracle" from the one established in computability theory, and I find this unwise.  What I fully agree with is that the kind of dynamic interactions between the axiom and the proof that you allude to is interesting and well worth understanding.

- Xavier

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
>