[Agda] Proof irrelevance and self-realizing formulas

[James Caldwell]

Very interesting discussion on proof irrelevance.  I thought I'd mention a
bit about Nuprl.  A very nice description of Nuprl written by Stuart Allen
is available online at
http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives.

In Nuprl, the set type, {x : T | P[x] }  is used to define squash,
squash(P)  =def  {True | P}.   There may be many proofs of P, but squashing
them reduces them all to a single inhabitant (*) of True.  If P is
uninhabited, squash(P) is uninhabited. Using this, define squash
stability,   sq_stable(P) =def  squash(P) => P.   Being squash stable means
that at least one of the proofs can be constructed just from the knowledge
that P is inhabited by at least one proof.

Adding the set type (comprehension subtypes) does require some management
since now there are (in the Nuprl implementation) so-called hidden
hypotheses.  Decomposing a set type {x:T | P[x]}  on the left yields
hypotheses  y:T, z^:P[y]  where z^ is "hidden".  Since the inhabitants of
the set type {x:T|P[x]} are simply elements a\in{}T such that P[a] holds
(but for which we do not know the proof)  we need to make sure that the
missing computational content does not find it's way into the proof.  Hidden
hypotheses may be "unhidden" if P is squash stable, or if it is stable or if
it is decidable, or if the computational content of the goal is trivial
(e.g. it is an equality or a membership).

I take a rather mercenary point of view; I am interested in programs and in
proofs as a means to constructing them.  Except perhaps in applications of
proof carrying code, to get good programs you probably do want to discard
the computationally uninteresting parts.  In a sorting algorithm, why carry
the proof that the sorted list is a permutation of its input and is
ordered?  Even classical logic for these computationally uninteresting parts
is  fine with me.

Best,
Jim
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090529/daabe494/attachment.html