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

Operations on Closed Maps

Here we describe some basic operations on closed maps. Recall that a closed map is a function of type DText(D) for some finite discrete type D. See Conservation and Destruction for connotations of + and - prefixes used below.

+ Uniform Renaming.

Let the function r*  Text(D)Text(X), for r  DX, replace each abstract id constituent i:abid (for i  D) by r(i):abid throughout the text. A renaming of a whole closed map f  DText(D) is a closed map r* o f o r  XText(X) for inverse functions r  DX and r  XD. Two closed maps f  DText(D) and g  XText(X) are "equivalent" when they are renamings of each other.

+ Contracting.

If X  D then "contracting" a closed map f  DText(D) around X is restricting f to X together with objects referred to by objects in X (ie, the smallest A  D such that X  A and f(i)  Text(A) for all i  A). Hence the contraction is the smallest submap including X. So, contracting a closed map around some of its objects (indices) X is discarding all objects except those among or referred to by the objects of X.

+ Focusing.

If X  D then "focusing" a closed map f  DText(D) on X is "contracting" f around X together with objects that refer to members of X. So focusing a closed map on some of its objects X is restricting it to the objects relevant to X.

+ Deleting.

If X  D then "deleting X" from a closed map f  DText(D) is finding the largest submap of f excluding X from its indices. That is, the deletion of some objects (indices) X from a closed map is gotten by removing X along with all objects whose contents refer to any of X.

- Reassigning.

A reassignment of a closed map is a closed map with the same indices but perhaps different contents for some or all the indices.

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

Glossary FDLnotes