IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Problems with Naming
Individuals and traditions can disagree over the proper use of names informally, as well as whether a particular formalization of an informal named concept is appropriate. On such occasions, it may be important to change names. With appropriate technology, it would not be necessary to resolve such disputes; the parties could select the names they prefer and operate independently with regard to naming. Similarly, a person may come to regret their own name choices and desire to change them. This is most acute when a name belongs to an informal concept that does not match a formal use of the name, probably as a result of a mistake. And yet the material may be formally correct and worth preserving and using further, just with a better nomenclature.
Another form of dispute over names might be thought of as a property dispute. When two persons have independently developed formal material using the same name for different formal concepts, they may well agree that both are correct, but cannot formally combine their work because of the unfortunate coincidence of naming. The parties must agree to renaming if they are to unite their work formally.
The name collision problem becomes particularly intense when programs operate on names as data and come to depend on them, and here it is not the human-mnemonic value of names but their role as identifiers that is our concern. While we may tend to think of renaming mathematical concepts or identifiers in programs as paradigmatic, when names are runtime data the problem becomes more difficult. If we attempt to combine programs by resolving name conflicts in their code, we may still be left with name collisions in their execution because they may generate names as runtime data that we cannot avoid by static renaming. See Abstract Ids & Closed Maps.
The above remarks treat the names as essentially interchangeable because they focus on the problems of maintaining formal correctness under change of names, and assume the desirability of methods for freely changing names. But there is also the problem of informal correctness. The names must be assumed often to matter to the human ability to understand and apply the formal material. This means that name changes must not be imposed on individuals without their control. Each user must be empowered to manage their own assignment of names, albeit with advice provided for naming objects and concepts they did not themselves create.
As suggested in Words vs Formality, by design we separate the nomenclature from formal content, making it changeable without effect on the formal content, and use objects in the FDL to specify for any given Session how to attach informal names to objects and concepts. This exposes naming (and renaming) to management by those that depend on it. Just as users may rely on stability of formal content, so they may rely on stability of nomenclature as they see it, and yet cannot impose on others their nomenclature for formal content. (Note that even informal nomenclature within informal documents may be made variable by picking an abstract name for use within the document, and binding it to a concrete name by user choice using the same mechanisms as for naming formal objects. This would be like using TEX macros in a document source, but applying systematic methods for managing nomenclature choices throughout the system.)
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html