FDL notes - Altering Certificates

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

Altering Certificates

In Current Closed Maps we specified some operations on the current closed map considered "conservative". Conservative operations are simple, whereas other operations force reconsideration of some Certificates which may have become "stale" as a result. The assumption here is that certificates are normally intended to attest to some facts about the contents of, or identity between, objects and so may fall into doubt when those change. Rather than simply deleting or discounting certificates that become doubtful, we anticipate a more incremental processing of doubtful certificates that might rehabilitate some certificates or even leave them intact. The presence of stale certificates in the current closed map corresponds to an "inconsistent" state in a database, and part of completing an operation on the current closed map is to eliminate staleness. Reconsidering a certificate can result in its modification or deletion, which can force reconsideration of further certificates that depend on it, and so a protocol is needed for resolving these cascades of certificates going stale. See Stale Certificates.

As explained in Certificate Structure, to implement a kind of certificate one adopts a procedure for creating new certification objects of that kind, and a procedure for reconsidering a certificate. When a reconsideration procedure for a certificate is executed to (successful) completion, the certificate object is either left intact, updated, or deleted. These certification procedures, in addition to creating certificates or modifying contents of "reconsidered" certificates, may create or delete other objects, and may alter the contents of non-certificates. But some basic operations may have cascading consequences on the FDL, beyond the control of any specific certification procedure:

* Execution of a certificate creation procedure is a basic operation on the current closed map, and the content of the certificate will include an indication of its kind. Creation procedures can take arguments supplied at execution. The indication of certificate kind is beyond the reach of the certificate creation procedure stipulated for the kind itself, and is controlled by the system.

* Execution of a reconsideration procedure for a kind of certificate is a basic operation that can be applied to any extant certificate of that kind. Again, the content cannot be altered to omit the fact that it is a certificate of its kind.

* The content of any non-certificate can be changed to any content except that it cannot have the form characterizing certificates.

* Object indices can be identified with each other (see Folding).

* When any object's content is altered other than by conservative operations (see Conservation and Destruction), be it a certificate or not, each certificate object referring to it in certain limited ways will be "reconsidered" according to the procedure specified for its kind. If reconsidering a certificate alters its content, then certificates referring to it must themselves be marked for reconsideration. If reconsidering a certificate leaves it intact, then it engenders no further marking for reconsideration.

* Similarly, when multiple objects are identified with each other (see Folding), any certificate that contains references to more than one of them gets marked for reconsideration.

See also Assimilation to Certificates.

Of course, there are practical issues of making these current closed map transformations convenient. For example, users must be able to abort transformations and get advice about consequences of proposed transformations. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes

*	Execution of a certificate creation procedure is a basic operation on the current closed map, and the content of the certificate will include an indication of its kind. Creation procedures can take arguments supplied at execution. The indication of certificate kind is beyond the reach of the certificate creation procedure stipulated for the kind itself, and is controlled by the system.

*	Execution of a reconsideration procedure for a kind of certificate is a basic operation that can be applied to any extant certificate of that kind. Again, the content cannot be altered to omit the fact that it is a certificate of its kind.

*	The content of any non-certificate can be changed to any content except that it cannot have the form characterizing certificates.

*	Object indices can be identified with each other (see Folding).

*	When any object's content is altered other than by conservative operations (see Conservation and Destruction), be it a certificate or not, each certificate object referring to it in certain limited ways will be "reconsidered" according to the procedure specified for its kind. If reconsidering a certificate alters its content, then certificates referring to it must themselves be marked for reconsideration. If reconsidering a certificate leaves it intact, then it engenders no further marking for reconsideration.

*	Similarly, when multiple objects are identified with each other (see Folding), any certificate that contains references to more than one of them gets marked for reconsideration.