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,
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.
Abstractness:
This means abstractness with respect to object identifiers (see
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.
Monotonicity:
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:
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
See