Processes as Owners, Process Certificates, and Engine Stables

Process Certificates and Process Identity Certificates

Certificates generally are owned by an FDL, i.e., by the process maintaining the FDL repository. This means that the creation and alteration of certificates is done exclusively by that process. The FDL (process) promises to create and alter certificates according to specific procedures associated with certificate kinds. One policy that could be adopted by an FDL for some kinds of certificates is to assign exclusive modification rights to a subprocess in perpetuity. Let us call such certificates "process certificates". Once a process terminates, the contents of process certificates assigned to it are frozen, and they become faithful records of past subprocesses.

To track and remember process identity, when the FDL builds a subprocess it could create a "process identity" certificate containing information about its construction, and assign it as a process certificate to the subprocess; the subprocess might further create its own process certificates. In any records that one cared to develop referring to the subprocess, this reference could be effected by object reference to its process identity certificate.

A major kind of subprocess of an FDL is the establishment of a "Session" for developing a current closed map. Another major kind of subprocess involved in the development of a logical library is an "inference engine" for certifying inferences according to some specific criterion. Managing this process becomes interesting in light of the practical fact that establishing a process capable of performing such inferences can be expensive and we shall typically want to establish an inference engine then use it repeatedly for many inferences. If one were simply to build in a single inference engine into the FDL as a permanent vehicle, then there would be no particular complexity in using it and accounting for its use - certifying an inference would simply be calling the built-in inference procedure (which is not to say that accounting for its correctness is simple). But that simple scenario has little relation to the intended deployment of the FDL. In fact, we expect to manage multiple inference engines, each with complex state, as a matter of course, and indeed we expect this to involve building external processes as needed, and communicating with them repeatedly while they endure.

Stables of Engines

We imagine the FDL process maintaining a "stable" of these workhorses. Let us suppose that the FDL creates a process identity certificate for each of these engines indicating how it was established (the external significance typically being that an engine built in a certain way recognizes an understood class of inferences). Then when a request for verification of an inference arises, the desired sort of engine is determined and either an appropriate member of the stable is put to work, or the stable is further developed by building a new engine of the required sort. It should be expected that an engine would normally be built by constructing an external process, and then communicated with by appropriate protocols; the internal FDL subprocess would remember how the external process was established and how to communicate with it in order to effect inferences which the internal subprocess, as a subprocess of the FDL, then certifies. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html