Glossary FDLnotes
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Conflicts of Certificate Significance - a Scenario

Continuing the discussion of internal and external significance of certificates begun in Certificate Significance, it is possible for us to be mistaken or in disagreement about the external significance we have attributed to a kind of certificate. For example, suppose we have employed a kind of certificate for generating or verifying formal inference steps; the certificate policy might go something like this: invoke a specified inference engine, building it first (perhaps compiling its code) if need be, and apply it to an inference step object in the current closed map; if the inference engine says the step is "good", create the certificate, whose content will refer to the inference step. This is the "internal" significance. External significance to some persons might comprise the conformance of the inference step to a certain independently understood class of inference rules. For a person who judges all these rules to be correct, the external significance may further comprise the validity of the certified inference step. Of course, maybe it will be later discovered or suspected that the inference engine is flawed and doesn't simply implement the inference rules it was thought to implement. Then that external significance is lost.

Let us continue with this example of the flawed proof engine, and consider a recovery scenario. Suppose that further study and improvement of the inference engine leads to the judgement that there is an easy bug fix, and that there is a simple test that detects at least the bad inferences that the older version of the engine erroneously okayed. Now we have fallen into doubt about already certified proofs. One simple fix is to employ a similar form of certificate, the difference being that it invokes the new engine rather than the old one, and simply try to certify all the old inferences with the new form of certificate. The old certificates need not be deleted, although perhaps they may be eventually.

Consider now a more sophisticated scenario. Stipulate a form of certificate that is created this way: given an inference step, first look and see if there is a certification for it (pointing to it) of the old sort that uses the defective engine; if there is no old-engine certificate then use the new engine; if there is an old-engine certificate then apply the test for possibly-bad inferences postulated above for this scenario; if the inference is possibly-bad then use the new engine, but otherwise, simply point to the old-engine certificate. If there were many proofs with the old engine but the bulk of inferences were okay according to the new test, and if running the engine is often expensive, then this method could represent a significant efficiency as a corrective.

Let's do a quick survey of when these various certificates are appropriate. Let's also make the more interesting assumption that whether the engine is flawed is not agreed upon by all parties. Persons who think the old engine was correct will still accept the old certificates with their original significance for correctness. Persons who think the new engine is correct and that the test for possibly-bad cases is an accurate assessment will accept both new-engine certificates and also the hybrid certificates that depend on the old engine. Persons who think the new engine is correct but don't trust the test for possibly-bad cases will insist on the simple new-engine certificates. All these certifications can coexist, even if their external significances are in dispute. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes