The Significance of Certificates

The only general policy for changing certificate content that we currently expect to adopt was alluded to in Certificate Bias; the system can change the content of a certificate by marking it as "stale" and possibly deleting object references within it to no-longer extant objects. Such a vestigial certificate thus signifies merely the past existence of a certificate having certain content. These vestigial certificates will, therefore, tend to have little formal value, and are expected to serve as hints about previous situations, which may have some heuristic value. See Certificate Structure and Stale Certificates for detail on certification policy.

A simple content alteration policy, one might deem it the default, is extreme sensitivity to the content and number of objects referred to by the certificate. It is this: if the content of any object the certificate refers to is changed, then the certificate must be deleted (or its content must be altered to mark it vestigial); its fate will be the same should multiple references within the certificate get "identified", by Folding, say.

For example, if a proof "goes bad" because of some alterations to underlying content, say a change of definition or deletion of an inference rule upon which it depended, or through forced identification of two "primitive" notions, then the objects certifying it as a well-formed proof (according to whatever standards) will be deleted or marked as stale. If they are altered to these vestigial forms rather than deleted, they may be useful in further attempts to attach new certificates to the proof.

A more permanently useful vestigial certification would be a certificate of object creation. An object creation certificate might be implemented to indicate that an object it refers to was created at a certain time in a certain Session. Then, as we can infer from the general policies mentioned above, a vestigial certificate of this kind still signifies that the object was created at the specified time but may have undergone a change of content. So some vestigial certificates do retain their significance.

One might also implement kinds of certificates that are insensitive to some alteration of content in referenced objects. For example, one might adopt a criterion for mere annotation of programs or formal data that does not affect correctness, and leave "annotation insensitive" certificates intact if objects they refer to are altered merely in their annotations.

Returning to external significance of certificates, it is also possible for us to be mistaken or in disagreement about the external significance we have attributed to a kind of certificate. This lies beyond the responsibility of the closed map management system. For a scenario exploring this situation see Conflicts of Significance.

The most important promise implementors can make with regard to certification is that the policy for creation and update of each kind of certificate is permanent, once implemented. If a new policy is needed or desired, a new kind of certificate must be implemented. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html