The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I realize belatedly that my explanation mostly duplicates what Hugo had already written, which I had only skimmed.  Sorry about that Hugo!

On Wed, Feb 14, 2024, 10:51 Jason Gross <jasongross9 AT gmail.com> wrote:

call/cc does decide the halting problem, just as it allows implementing excluded middle.  When you ask it to decide the halting problem, it takes the current continuation, and then claims that your TM never halts.  In order to use that proof, you must provide evidence that your TM does halt.  When you do this, instead of producing a contradiction, the program uses the continuation to effectively rewind time, and this time it says "in fact your TM does halt" and uses the evidence you gave it.

In symbols, if you want A + (A -> False), you get it as (call/cc (fun cc => inr (fun a => cc (inl a)))).

Best,

Jason Gross

On Wed, Feb 14, 2024, 10:39 Xavier Leroy <xavier.leroy AT college-de-france.fr> wrote:

On Wed, Feb 14, 2024 at 11:59 AM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Hi,

The Limited Principle of Ominiscience (LPO) is indeed rather standard
in the context of the constructive study of real analysis where it
basically amounts to assuming the decidability of the disequality of
Cauchy reals [1]. The Coquelicot paper that Kile Stemen is mentioning
is, I guess, [2], section 3.2, where other applications are given.

There are computational interpretations of this axiom

For some meaning of "computational". 

but not purely
functional ones. The basic interpretation is as an effectful program
that duplicates its evaluation context, as would be allowed by the
call-with-current-continuation (callcc) operator, or, to some extent,
by setjmp/longjmp in C.

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?

 

Cheers,

- Xavier Leroy

So, to vizualise the computation, you have to consider a program p
that uses LPO. For the purpose of a decision that p expects from LPO,
the latter first assumes that (forall n, P n) holds, which is a safe
assumption until p eventually wants to exploit this assumption by
providing some natural number n₀ for which it wants to know (P n₀). At
this time, LPO uses its assumption on the decidability of P to
determine if (P n₀) or ~(P n₀) holds. In the first case, its initial
guess that (forall n, P n) holds is satisfied (for this particular n₀)
and the evaluation of p can go on, until p wants to use the assumption
(forall n, P n) for another n, in which case the process is
repeated. In the second case, LPO changes its mind, which is possible
because it memoized the evaluation context in which it was initially
called. So, it resumes to this former point of the evaluation and now
says that {n | ~P n} holds, taking n₀ as the witness.

Note that alternative computational interpretations of LPO specific to
the form of LPO have been provided, e.g. by Aschieri, Berardi and
Birolo [3].

I can also recommend Phil Wadler's nice story rephrasing in "demonic"
terms the "magic" behind excluded-middle ([4], top of page 7). Since
LPO is the particular instantiation of excluded-middle to
∑⁰₁-formulas, this story applies to LPO too.

In any case, that's a fascinating topic...

Best,

Hugo

[1] https://ncatlab.org/nlab/show/principle+of+omniscience#the_limited_principle_of_omniscience
[2] https://www.lri.fr/~melquion/doc/14-mcs.pdf
[3] https://dmg.tuwien.ac.at/aschieri/RealizabilityforHAEM1-ExceptionsProofs.pdf
[4] https://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf

On Wed, Feb 14, 2024 at 10:15:05AM +0000, mukesh tiwari wrote:
> Thanks Kyle! 
>
> Best,
> Mukesh 
>
> On Wed, 14 Feb 2024 at 05:12, Kyle Stemen <ncyms8r3x2 AT snkmail.com> wrote:
>
>     That's the limited principle of omniscience. The Coquelicot paper explains
>     how it's used for classical real analysis.
>
>     On Tue, Feb 13, 2024 at 7:02 AM mukesh tiwari
>     mukeshtiwari.iiitm-at-gmail.com |coq-club/Example Allow| <
>     dsd13c3nm2whb1t AT sneakemail.com> wrote:
>
>         Hi everyone, 
>
>         I was looking into Coq standard library and saw this axioms
>         sig_forall_dec [1] by a mere accident. I am trying to understand the
>         intuition behind this axiom but my programming intuition simply cannot
>         get it. I admit it is a classical axiom but I am finding it very hard
>         to wrap my head around it.  
>
>
>         The way I see *sig_forall_dec* is a function that takes a function P
>         --which returns Prop for every natural number-- and a function f
>         ((forall n, {P n} + {~P n})) —which takes a natural number return P n
>         or ~P n-- and it returns a proof object {n | ~P n} or returns a
>         function {forall n, P n}. This whole things, to me, appears like a
>         magic because we are turning a function *f* into proof object ({n | ~P
>         n}) or a function for which P holds for every natural number ({forall
>         n, P n}). I will appreciate if someone can shed a light on the
>         intuition behind this magic. I presume it is used in reasoning of real
>         numbers so what kind of proofs about real numbers require this axioms? 
>
>
>
>         Axiom sig_forall_dec
>           : forall (P : nat -> Prop),
>             (forall n, {P n} + {~P n})
>             -> {n | ~P n} + {forall n, P n}.
>
>
>         Best, 
>         Mukesh
>
>         [1] https://coq.inria.fr/doc/V8.17.1/stdlib/
>         Coq.Reals.ClassicalDedekindReals.html 
>