Glossary FDLnotes
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Abstract Identifiers and Closed Maps

The abstract use of identifiers for FDL object "names" and as components of expressions within the text collection is basic to our methods for managing the collection, especially as regards correctness. The intention is that the user should treat names or identifiers abstractly, simply taking them to be discrete and atomic. They fill formal roles normally filled by simple names (identifiers), but have no informal value, in particular no mnemonic value or value as conventional nomenclature. See Abstract Identifiers (how). This is our technique for avoiding disputes or errors concerning names in the formal content, and how we facilitate essentially arbitrary combination of objects, avoiding name collision; abstractness of names entails their uniform replaceability.

We will discuss a variety of issues concerning abstract identifiers, but here we give an overview of relevant facts about our intended system without elaborate motivation.

By a "closed map" we mean a function of type DText(D) where D is a finite discrete type of values. The type Text(D) is the class of expressions where the values of D are of kind "abid". Here we must digress. Abstractly, for many purposes of reference and accounting, Text(D) could be any kind of data for which it is understood what counts as "occurrences" of D-values within the text. However, the Text structure we adopt is a simple recursive type of iterated operators on subtexts because the subexpression relation is dominant in typical computations on expressions in precise notations. In addition to its subtexts, a text contains a sequence of labeled values presupposed by the construction of texts, which we call here "pro-textual" values. When we define the class of texts, the kind of pro-textual values that can occur with a given label is determined by the label, and is stipulated when that class of pro-textual values is introduced. Text(D) is the type of texts in which the possible pro-textual value constituents of form "x:abid" are those such that x  D. We identify objects in a closed map with indices. See Pro-textual Constituents.

In practice the class D of object indices will be varied continually. For example, extending a closed map requires selecting a larger index class. Deleting members of a closed map requires a smaller index class.
If the restriction of a closed map f  AText(A) to a subclass X  A is in XText(X), and so is itself a closed map, then we call the restriction a "submap" of f.

Two closed maps f  AText(A) and g  BText(B) are "equivalent" when they are simply "renamings" of each other, i.e., when there is a one-one correspondence between A and B such that for corresponding a  A and b  B, f(a) and g(b) are identically structured modulo matching abid occurrences that correspond. See Closed Map Operations.
The abstract treatment of object indices entails that whatever criteria of correctness hold of one closed map hold also of equivalent closed maps.

Dependency management between objects in a closed map f  DText(D) is based upon an explicit criterion of object reference: an expression t  Text(D) refers "directly" to object (index) x  D just when x:abid is a pro-textual constituent of the text t (this includes any subtexts of t).
An expression refers, perhaps indirectly, (wrt f) to x  D just when either it refers directly to x or else it refers to some object y  D where f(y) refers to x.

Continued at Closed Maps IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes