Glossary FDLnotes

The Significance of Certificates

The "internal" significance of Certificates in a closed map is determined by the policies for how they are created, deleted and altered. Some policies for the effects upon certificates of various closed map operations are suggested in Certificate Bias and in Conservation and Destruction. Thus, the existence of a certificate in a current closed map directly indicates merely that at some time it was created in a current closed map according to a creation-policy implemented for that kind of certificate, and has not been deleted by various subsequent alterations of the current closed map, and that any alterations to the certificate's content has been according to the policy implemented for certificates of its kind. As usual with formal and computational data, further significance is attached externally based upon understanding the "internal" significance.

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

Glossary FDLnotes