The Coq mailing list

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

Hi again,

To clarify the situation, I realize that we need to distinguish
sig_forall_dec from its variant in Prop. So, let me make a difference
between (for P decidable):

  LPO_informative : {n | ~P n} + {forall n, P n}

and

  LPO_prop : (exists n, ~P n) \/ (forall n, P n)

If LPO_informative (= sig_forall_dec) directly implies LPO_prop, what
allows to go back from LPO_prop to LPO_informative is the axiom of
unique choice.

In the context of constructive mathematics, unique choice is often
taken as granted, so the two are conflated but in a context without
unique choice, which is the case of Coq by default, it makes a
difference. And the difference is particularly visible at the level of
the computational content: what I described in my previous message is
the computational content of LPO_prop and it "only" requires some form
of callcc isolated in the Prop stratum. In the presence of unique
choice (or if considering LPO_informative directly), the Prop world
"leaks" in the Type world, so that more "computational power" is
needed. This might have been what Mukesh then Xavier implicitly
questioned: indeed we additionally need at some time to "emulate" the
behavior of the underlying (non-recursive) function that associates an
"option nat" to any decidable predicate over nat.

The rest of this long message is to describe how "bar recursion" can
be used to compute with some simple instances of LPO_informative, and,
if I'm saying "some instances", it is that the question of attaching a
computational content to the full generality of LPO_informative is to
my knowledge an open problem, where by full generality is meant that P
ranges over arbitrary predicates. So, I will restrict the discussion
to the simpler but paradigmatic case of the termination of a Turing
machine, that is, morally, to a class of predicates indexed by just an
integer.

We shall thus use bar recursion which is a form of forcing originally
introduced to realize the axiom of dependent choice in the presence of
classical logic, and which is a fortiori usable to realize the axiom
of unique choice in the presence of classical logic.

Let's apply sumor and sig elimination to the halting problem instance
of LPO_informative so that it is rephrased as the existence of an

  f : TM -> option nat

such that, for all Turing machine state m:

  f m = Some n -> terminates m n
  f m = None -> (forall n, ~ terminates m n)

As in the case of callcc, giving a computational content to such
statement requires reasoning in the context of the evaluation of a
proof p of some other formula, where p depends on the halting
problem. As in the case of callcc, the evaluation context at the time
when p calls the halting problem has also to be kept.

What bar recursion does is to compute finite approximations of f with
enough precision to grant what the evaluation of the program p needs.
If the evaluation eventually stops, it will have de facto needed to
observe only a finite fragment of f, so being able to provide finite
approximations is enough as soon as these approximations are as
informative as the program p requests them to be.

Bar induction uses a memory cell storing a finite approximation of the
expected function. In the case of the halting problem, it will require
a memory cell of type (list {m:TM & n:nat & terminates m n}).

Informally, the computational content is the following:
- when initially called by p, memoize the evaluation context and
  declare a mutable variable "v:list {m:TM & n:nat & terminates m n}"
  initialized with the empty list; this memory will maintain what is
  known about each Turing machine considered at some time along the
  interaction of the program p with this particular instance of LPO;
- satisfy the request of p by defining (f m) to be Some n if some
  (m,(n,w)) occurs in v and None otherwise (that is, at the beginning,
  the constant function None, but this will evolve);
- prove (f m = Some n -> terminates m n) by returning the corresponding
  proof w of (terminates m n);
- prove (f m = None -> forall n, ~ terminates m n) by deciding (terminates m 
n):
  - if m has terminated in less than n steps with proof w, add the
    triple (m,n,w) to v and go back to the beginning of the call with
    the refined approximation,
  - if m did not terminate after n steps, returns the proof of
    non-termination as requested.

As touched above, to my knowledge, it is an open problem to equip the
whole of Coq with a clearly-defined computational content for
LPO_informative in its full generality, but an abstract argument
allows to assert that such computational content does exist, just
because there are translations of Coq + axiom of choice + classical
logic into Zermelo-Fraenkel set theory + a tower of inaccessible
cardinals and that we have a computational interpretation of the
latter (e.g. using Krivine's classical realizability). The problem is
mostly that these translations are too complex (they typically involve
Gödel's constructible sets to interpret the axiom of choice) for
anyone being able yet to extract a clear computational content out of
them.

Also, back to the question of Xavier, we never produced a code for the
function f, even not a code involving callcc. What we produced were
only approximations of f, guided by the requests of the client p of
LPO_informative. Told in another way, where the computation happens is
not in f but in the proof of the (ideal) existence of an f.

Best,

Hugo

PS: The story continues further. For instance, there are connections
between bar recursion and System F (see works by V. Blot, and
indirectly É. Miquey), there are connections with coinduction (see
Escardó and Oliva's coinductive product of selection functions), there
are connections between bar recursion and continuity (see works by
M. Baillon).

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 
>