Conversation
ana-pantilie
left a comment
ana-pantilie
left a comment
There was a problem hiding this comment.
Why do we want to allow checking procedures? Is this because we're not sure if the translation relation for inline is fully decidable?
|
This is what the entire email thread with Phil is about. Nothing is undecidable, but a decision procedure for inliner would be way too slow. Even the checking procedure is not that fast. And decision procedures in general can take exponential time, even for a simple pass like forceDelay. |
| data CertResult (P : Set 𝓁) : Set (suc 𝓁) where | ||
| proof : (p : P) → CertResult P | ||
| ce : (¬p : ¬ P) → {X X' : Set} → SimplifierTag → X → X' → CertResult P | ||
| abort : {X X' : Set} → SimplifierTag → X → X' → CertResult P |
There was a problem hiding this comment.
Should abort be renamed to unknown? Since this type means: either we have proof of P, a proof of ¬ P, or neither?
There was a problem hiding this comment.
unknown is not accurate. In general we do know that a proof doesn't exist. We just don't have a negative proof.
There was a problem hiding this comment.
In general we do know that a proof doesn't exist. We just don't have a negative proof.
That doesn't make sense in Agda's constructivist world. Logically, if we don't have a proof of P nor of ¬ P, then the result is unknown.
Even if we might reason about it outside of Agda (in X case we know that's not the right constructor so we can "abort"), the simple fact that we're not producing the proof means that Agda will never be convinced of that fact. Therefore, we won't have any formal guarantee of completeness.
There was a problem hiding this comment.
"unknown" is confusing because it has multiple meanings.
It could mean "we really don't know whether or not there is a proof - my checking procedure is really lousy, it may give up prematurely and may not find a proof even if one exists!" which is bad.
It could also mean what you said - "we do know that it will find a proof if one exists, and we can even formally prove it on paper using classic reasoning; we just haven't proved it in Agda." That's much better.
If we use "unknown", I think many people's first instinct would be the former meaning - at least that's the case for me. By the way, for the same reason I think "abort" isn't ideal either, but I can't think of a better word at the moment.
There was a problem hiding this comment.
As an example: the fastest prime testing algorithm can give yes/no quickly, but cannot quickly construct a negative proof (a factorization). If we use such an algorithm as a checking procedure, and it returns "no", it would be quite misleading to say "it is unknown whether the number is prime or not". We definitely do know that it's not prime, we just don't have a negative proof.
There was a problem hiding this comment.
Not to mention that in some cases (specifically, in the inliner case) we do have an Agda proof of completeness for the checking procedure.
There was a problem hiding this comment.
I don't know what to name this! Maybe undecided, or do you think that still suffers from the same possible misinterpretations as unknown? Perhaps we can just document the constructors better: if it's "undecided" (or whatever name we choose) then it's up to the engineer to provide a completeness proof in whatever way they can. Also, maybe @basetunnel or @ramsay-t or Phil have better ideas for naming. In any case, I don't want to block this any further so I'll approve it but I still think it needs some clarification either through naming or through documentation or both.
There was a problem hiding this comment.
I'll add some documents separately.
We should document this decision (no pun intended). The main takeaway I guess is that we're sacrificing completeness for performance, but that this does not affect soundness in any way. |
zliu41
left a comment
zliu41
left a comment
There was a problem hiding this comment.
The main takeaway I guess is that we're sacrificing completeness for performance
That's not true. We don't need to sacrifice completeness for the checking procedure to be much faster. Knowing that a proof can't exist is often computationally easier than constructing an actual negative proof.
| data CertResult (P : Set 𝓁) : Set (suc 𝓁) where | ||
| proof : (p : P) → CertResult P | ||
| ce : (¬p : ¬ P) → {X X' : Set} → SimplifierTag → X → X' → CertResult P | ||
| abort : {X X' : Set} → SimplifierTag → X → X' → CertResult P |
There was a problem hiding this comment.
unknown is not accurate. In general we do know that a proof doesn't exist. We just don't have a negative proof.
2 participants
Allows each pass to choose between a decision procedure, which returns
ProofOrCE, or a checking procedure, which returnsProof?.