Glossary FDLnotes

Certificate Bias

As was mentioned at the end of Certificates, we give preferred treatment to certifications of facts about Closed Maps that are abstract, monotonic, and "localized".
Elsewhere we shall address the questions of what kinds of certificates are likely to be preferred, and which disfavored, and why we give this preferential treatment. But, here we address:
What constitutes this preferential treatment?

When the user's current closed map is modified, the FDL interface system is responsible for deleting or altering certificates, and advising the user about problems, especially to avoid surprising de-certification which could be expensive to recover from by recertification.

Setting aside the issue of how to forestall undesired damage to a current closed map, what happens to certificates normally? We shall use program execution in some scenarios because the problems should be familiar, and because some methods of proof (eg, Tactics) involve execution of programs from a general purpose programming language.

Here are the features of certificates about closed maps mentioned above, and examples of disfavored kinds of certificates. Following each explanation of a feature is a description of undesired consequences of using certificates lacking the feature; the fact that such undesired consequences arise constitutes the system's bias towards violated features, ie, the system treats certificates having those features more favorably.


This means abstractness with respect to object identifiers (see Abstract Ids & Closed Maps and Abstract Identifiers (how)).
When a closed map is uniformly renamed or is retrieved from the FDL, which is only guaranteed modulo renaming, there is no rechecking of certificates; they are treated like any other objects.

Suppose, for example, that during a session, a person goes out or their way, and against advice, to store a program whose execution depends on the concrete values that happened to be used in that session for object ids, and has the system execute that program and certify a result. Then if that current closed map is saved and reloaded (modulo name change) in a later session, that certification object will cease to entail that the old connection between the program and result has been preserved.


Similarly, suppose one wrote a program whose execution involves a heuristic search of the whole current closed map, whatever it may be at execution time. Then executing the same program on a extension of the same closed map may well have different results, thus a certification of the result of executing in one closed map will not certify the result in an enlarged closed map.

But, again, the system will not modify a certification object when the current closed map is enlarged.


Locality of a claim based on a certificate is dependence of that claim only upon the certificate and objects referred to by the certificate. A localized claim will also be monotonic since extending the map doesn't change what a localized claim about a certificate depends on.

Suppose that one cuts down the current closed map to a submap by Contracting or Focusing (see Closed Map Operations). For example, suppose one picks a certification object and Focuses on it, deleting every object that is irrelevant to it (ie, no reference path between them). The certificate will not be modified or checked. The problems are the same as for monotonicity above.

See Conservation and Destruction for a list of some closed map operations that leave certificates intact. IF YOU CAN SEE THIS go to

Glossary FDLnotes