The Coq mailing list

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

Dear Xavier,

It looks like we agree on the description of the computational facts
under consideration! About the terminology, it seems that your main
concern is that some people, outside the community of computatibility
theory, might confusingly use expressions such as "decide" or "halting
problem" with a different meaning than they have in computability
theory. If so, this is a true concern. For instance, already in the
Coq file theories/Logic/Decidable.v, we find the following
somehow non-standard definition:

  Definition decidable (P:Prop) := P \/ ~ P.

When placing ourselves in an axiom-free Coq, this definition is a
reasonable alternative to the definition in computability theory,
i.e. to the existence of a (total) recursive function that returns
true iff P holds, since, indeed, any proof of (P \/ ~P), for P a class
of problems parameterized by an integer, can be turned (externally, by
extraction) into a recursive function provably total in Coq, and,
similarly for the converse direction (externally also, by extraction
of the proof of totality, all this leading by the way to synthetic
computability [1]). But the definition takes a different meaning in
the presence of axioms, and especially in the presence of classical
logic. I suspect that this bothered several of us at some time, and
maybe continues to bother, so, maybe, should this be clarified in the
file "Decidable.v".

Now, regarding what deserves to be called statement of decidability of
the halting problem, I'm not fully sure that we want to restrict
ourselves only to the traditional statement of computability theory
that implicitly relies on Kleene's realizability.

  ∃f:TM, (f total ∧ ∀m:TM, (f(m)↓true ∧ m halts) ∨ (f(m)↓false ∧ ¬ m halts))

Indeed, from the moment we agree on the facts under consideration, we
could as well generalize the use of Kleene realizability in
computability theory to other variants of realizability, such as,
including Kleene:

- Kleene-realizability
  - intuitionistic
  - using any turing-complete language
  - with "quote" access to the code, so diagonalization possible
- Kreisel-realizability
  - intuitionistic
  - using the internal language of provably-total functions of the logic 
under consideration
  - w/o access to the code, thus no diagonalization possible
  - with or without empty types [2]
- Krivine-realizability
  - classical, i.e.
    - intuitionistic up to double-negation/continuation-passing-style 
translation
    - relatively to a toplevel type
  - optionally with other side effects:
    - "quote" to get access to the code
    - memory cells and bar recursion to implement forcing
  - provides an interesting (context-dependent) computational content to
    problems to which Kleene or Kreisel-realizability have no direct solution

and then define "p K-decides P" to be "p K-realizes ∀n (P n ∨ ¬P n)".

Best,

Hugo

PS: If some people are interested in having the kind of topics
discussed in this thread transcribed somewhere (and with mistakes
corrected), maybe could we start a (collective) wiki page summarizing
the different issues (if it does not already exist somewhere).

PS2: I could have added the semi-classical Gödel-Diller-Nahm-realizability
to the list but I do not understand it well enough to classify it.

[1] see A. Bauer, 2006, "First steps in synthetic computability theory",
    as well as the Saarbrücken approach, as presented in e.g. Y. Forster
    
(https://yforster.github.io/files/talk-chocola-synthetic-computability.pdf)
[2] see discussion in Pédrot-Tabareau, 2018, "Failure is Not an Option"

On Sat, Feb 17, 2024 at 12:09:25PM +0100, Xavier Leroy wrote:
> 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
>     >
>