Elaboration on certificate structure.
(from Nov 17 Seminar)

After the introduction of Simple Certificate Systems some diagrams (not reproduced here) were drawn to illustrate certificate structure and how certificates relate to texts generally.

The diagrams emphasized the following features:

A number of issues raised by me and by the audience before and during the presentation of these diagrams were addressed:

What makes something a certificate? The fact that that its content has a certificate identifier (drawn as being in the special box defining certificate identifiers) as its first pointer.

Can the certificate creation code be updated? Only if the the certificates pointing to it as such are deleted. (Note this concerns the code pointed to by the certificate rather than the contents of the certificate iteslf.)

Why keep the pointer to the certificate creation code after the certificate has already been created? Because the code is an essential part of the meaning of the certificate as a record. The existence of the certificate means that that creation code was executed with the result stored in the certificate.

Can the contents of a certificate be changed? In the Simple Certificate System, no. In the more liberal Certificate System discussed later, yes, except that the certificate identifier and certificated code-pointers cannot be changed, again because they give meaning to the certificate as a record.

Why are certificate identifiers kept distinct from certificate creation code objects? Because there may be multiple certificate identifiers paired with the same certificate creation code. The reason there may be multiple certificate identifiers is that there may be multiple semantics provided for executing native code. For example, if one wants to improve the way native code is executed, or correct some defect, one would create a new certificate identifier (adding it to the system's table of certificate identifiers). It must be new because altering the original meaning of the old certificates would violate the basic archival trust that is the purpose of the system.

The system implementors say which objects are certificate identifiers, but who says what the creation code for certificates should be? Anyone can say what code is executed to create certificates; the creation code objects are ordinary texts that users can create. Let us call a certificate kind a pair consisting of a native code object and a certificate identifier object. Users can therefore design whatever kinds of certificate they like, limited by the available execution semantics bound by the system to certificate identifiers. One would expect the number of certificate identifiers to be small, with many certificate kinds designed for each certificate identifier, with many certificates of each kind created.

# certificate identifiers << # certificate kinds << # certificate objects

What goes into the result part of the certificate? Whatever the designer of the certificate kind chooses. The value of that choice, the value of certificates of that kind, is an matter external to the system. Useful certificates must be designed to record sufficient data, especially pointing to the objects they are about, but there is no formal requirement.

But what keeps users from undermining the knowledge supposedly stored in the repository? Other users must ascertain, with system help, what certificates are worth their consideration. This is the basis for managing an open-ended theoretically neutral repository. The internal computational significance of certificates is what users must agree upon and be guaranteed by the implementors. The external significance of computational and syntactic facts must, as always, be determined by the users. One would normally use library utilities and certificate kinds that filter data to be marshaled from the repository for whatever purposes.

How can you hope to design a native language, or a few, that support the great variety of programming methodologies used by diverse user groups? There is no such intent. The intent is that the system calls external systems for heavy duty and special purpose programming tasks such as verifying inferences. The native language would be oriented to communicating with external processes and using the repository for data provided to, or returned by, those external processes. Disputes about external significance of certificates will therefore often reduce to disputes about external system behavior and reliability of communication methods.

How are proofs represented in the system? There is no prescription for this and it is determined by users of the repository, but there is good reason to represent a proof as a dag of its inference steps, each step having a conclusion and zero or more premises, rather than the whole proog as a single text. The cost of creating and checking inference steps, at least those steps carried out at a level high enough to make proofs humanly comprehended, will often dominate the cost of organizing individual steps into a whole proof. Especially when proofs are developed incrementally, adding inferences, one would want to avoid the rechecking of all steps of a whole proof every time it is slightly enlarged.
Remark: Also, it often happens that making a change to a completed proof changes only some of its constituent inferences, thus making it unnecessary to recheck the whole proof.

How would one check dags of inference steps? This answer is more explicit than the one actually provided in seminar, which vaguely described building a shadow dag of certificates paralleling the inference steps. Here is one plausible design. Design one kind of certificate K1 for validating (and maybe creating) purported inference steps. Design another kind of certificate K2 which takes as argument an object describing a rooted dag of inference steps. Such a dag could be represented by a rooted dag of objects each containing a pointer to one purported inference step and a sequence of pointers to all the predecessors in the dag. The certificate creation code of K2 for assembling a proof could then be a procedure that finds or builds a K1 certificate validating the step, builds similar K2 certificates for each of the predecessor inference steps, checks to make sure the conclusions of the predecessors match the premises of the root inference. The result text of a K2 certificate would then point at the K1 certificate for the root step and to all the K2 certificates for the predecessors. The K2 certificate code points to the K1 certificate code. Of course, if any of these steps fails, the K2 certificate creation code would fail and K2 certificate for the root would never be created.

Observe that one could similarly have stipulated not just that K1 certificates were acceptable to K2 certificates, but could instead have indicated a much broader criterion for which inference step checkers were acceptable in assembling a proof.

sfa