[Agda] Proof irrelevance and self-realizing formulas

[Arnaud Spiwack]

Hello everyone,

(Sorry if this mail is sent twice, it seems to have been blocked due to me
using a wrong adress)

I think it might be worth pointing that the computational content of
Golbach's conjecture (since it seems to have become the running example) may
very well not be considered void. It is fairly easy to build an algorithm
which given an n returns a maybe (exists j, k <= n, prime j /\ prime k /\ 2
* n + 4 = j  + k). The difficult proof is that which might prove that it's
always a Just.
In any case if we look at such an algorithm, the naive way to do that (by
iterating over primes smaller than n) we get an algorithm which is O(n^2),
that is an exponential algorithm if n has a reasonable representation.
Exponential algorithms are not really "void". Maybe there are better
algorithms to get these j and k (whenever they exist). This would lead to
different proofs I guess (at least of proofs of "if there exists j and k,
then this algorithm outputs them").

My personal growing issue with "proof irrelevance" is that it means "I never
care about the proofs", and that we intend "I don't care about a proof while
building a program". It doesn't quite feel right, maybe sometimes I want to
compute the witnesses of Goldbach's conjecture and sometimes I all but want
it (if it's an exponential algorithm then one has better to be careful about
when it's used). This leads to works like the lightnings from Connor and
Peter or CIC* from Bruno Barras and Bruno Bernardo. Which have funny
unwanted property too (elimination of False seems not to be too natural in
that setting, which probably implies that something is missing).

Also I guess this philosophical debates has invited the notion of
justification of proofs. An intuitionistic proof is a program, which will
always, given sufficiently many objects provides an obvious evidence of its
truth "on" these objects. Which is a lie, since it might very well require
more time than there is left to the universe to provide this evidence
(which, you will agree with me, is certainly problematic). This begs the
question: is such a proof an acceptable one? I would say yes, but then
again, it's likely that it might not be as nice as a polynomial-time proof
(which still might be rather long though (like eternal but more rarely)). So
is there a need of a notion of complexity in proofs (not logical complexity,
but execution time complexity)? But if so, then it might become important to
consider more proofs, with different execution models (exceptions? effects?)
which might prove to be of a lesser complexity for certain theorem. But if
we go in that direction we seem to be contradicting the principle of proof
irrelevance, don't we?




Arnaud

2009/5/28 Thorsten Altenkirch <txa at cs.nott.ac.uk>

> Hi Andrej,
>
> it is always fun to argue with you :-)
>
>  How do we explain that we are using the fact that p has inhabitants w.o.
>>> looking at them?
>>>
>>
>> This would probably have to be a primitive notion (hence my claim that
>> you need support at the meta-level).
>>
>
> So in Type Theory it is a definable notion (using equality) what is the
> point of having it as a primitive notion?
>
>
>>  I think you calculate a realizer not a proof.
>>>
>>
>> I think so, too. Perhaps the conclusion is that there is life after
>> type theory.
>>
>
> To me it seems rather like life *before* Type Theory. This distinction of
> proofs and programs to me is a relict of classical logic.
>
>  I think that was the point of my MSFP talk in Iceland
>> last year, but I did not present it very well.
>>
>
> I think it was an excellent talk and you made your point very well. Maybe
> you should mail the link to your slides here.
>
>  I never understood why
>> the BHK interpretation has to assume that there are no other forms of
>> computation apart from realizers of proofs in intuitionistic logic.
>>
>
> In my view the BHK interpretation provides a notion of evidence in form of
> a functional program not a realizer.
>
>  For example, why isn't the fan functional (a realizer for Brouwer's
>> fan theorem from which compactness of [0,1] follows) a "good"
>> computation? It's certainly useful, as Martin Escardo has been
>> showing.
>>
>
> There is a foundational and a pragmatic answer to this question:
>
> Foundational: There are certainly principles which are constructlvely valid
> (i.e. can be realized) which are not intuitionistically valid (Markov's
> principle is another example), i.e. they don't follow from the
> intuitionistic explanation of the connectives. While it may be good to know
> that they are realizable this is not sufficient as evidence that we should
> accept them as ways of reasoning. E.g. it is better if one can provide a
> translation which shows that an intuitionistic proof can be interpreted in a
> non-standard way which validates the additional principles. I think this is
> possible in the case of Markov's principle.
>
> Pragmatic: Adding these principles to Type Theory as computations would
> destroy normalisation of open terms. You can certainly add the as equational
> assumptions but this would destroy canonicity (i.e. there are terms which
> don't reduce).
>
>  Indeed, and this is certainly not a *proof* because it doesn't tell us why
>>> Goldbach;s conjecture is true.
>>>
>>
>> I agree it's not a proof. On the other hand, the computational content
>> of Goldbach's conjecture is void.  If I gave Thorsten a constructive
>> proof of Goldbach's conjecture and I gave Connor a classical proof,
>> could Thorsten compute more than Connor? So I am not sure proofs
>> should be identified with (terminating) computations.
>>
>
> No the difference is not in "computation" but in "justification".
>
>
>>  Not sure about Agda, but I don't see the advantahe.
>>>
>>
>> The advantage of having "proof irrelevance" as a basic notion is that
>> the resulting system would be more expressive. For example,  we could
>> express the fact that certain parts of a proof are "computationally
>> boring". Perhaps Agda already has a way of erasing the boring part of
>> an extracted realizer/proof? (I readily admit I know very little about
>> Agda, but I would like to learn more.)
>>
>
> I think the efficient compilation of Agda programs is an important and
> challenging question. However, I don't think we have to change the
> foundations to achieve this. And indeed proof-irrelevance (i.e. Prop) seems
> a good way to mark computationally irrelevant subterms.
>
> Cheers,
> Thorsten
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses, which could damage your computer
> system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090528/629c494a/attachment-0001.html