The Coq mailing list

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

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