The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Splitting off from the thread on sig_forall_dec, I have a question about call/cc

> 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 phrase "duplication of evaluation context" suggests that call/cc should let me do something like partial evaluation under binders, but I don't believe it does.

Concretely, suppose I have a function `f : A -> B * C` and I want to turn this into `g : (A -> B) * (A -> C)` such that `forall a, (fst g) a = fst (f a) /\ (snd g) a = snd (g a)`, in such a way that, if I am the author of `f`, I can cause `g` to lift any computation in `f` that does not depend on its binder in such a way that the computation is shared between the two components of `g`.  (I am ultimately interested in figuring out if there's a principled way to do this for functions deeply embedded in PHOAS, in linear time complexity, that doesn't involve routing through some first-order representation of binders, where such computation lifting is comparatively trivial.)

Is there any primitive that does this sort of thing?  Or any existing literature on the computational complexity of various operations induced by different representations of binders?

Thank you,

Jason

On Wed, Feb 14, 2024, 02:59 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 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.

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 
>