Abstract Id Allocation

We have decided to identify object indices and abstract identifiers. We shall discuss this below. But first let us consider some scenarios in which abstract identifiers are allocated for various purposes.

Suppose while developing a certain closed map (a function mapping object indices to object contents) one decides to add a new definition for some mathematical operator, say for GCD. If names were concrete, and users chose them, then allocation of a new name for this operator would comprise the user's coming up with a name not already used in the current closed map, and which one hopes will be acceptable in the future. (Complications involving errors and disputes could arise as mentioned in Naming Problems.)

But in our abstract identifier scenario, this name is selected by the system being employed to maintain the current closed map, and is not a subject of dispute. The user says "give me a new abstract id to work with", then proceeds to employ it, say by giving a definition intended to describe the GCD function, and proving some theorems about it. The user might also create a new object explaining the intended meaning of the new operator informally, as well as stipulating how to show instances of the new operator consonant with its intended meaning.

It is then feasible to later retain the definition and proofs involving this operator while rejecting or altering the informal explanations and advice that refer to it.

Names are needed for things besides mathematical operators, of course. Programming operators, macros, procedure names; command interface components; and, especially, objects in the FDL, where most of the content is expressed. Examples of FDL objects are: definitions of constants, operators and macros, proofs, source code for programs, specifications for how to concretely display abstractly structured expressions, data used as arguments to user-defined programs, informal documents, data stipulating external relations between formal objects, Readings.

We have chosen to identify abstract identifiers with object indices in "Closed Maps". In doing so we identify object allocation with identifier allocation. To add a new object to a closed map is to add a new object index and extend the closed map with a new object content assigned to that index. To get a new abstract identifier is to add a new object, which will be indexed by this new identifier. See Adequacy of Single Id Space for arguments that this collapse of all abstract identifier spaces to the space of object indices is without loss of generality. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html