IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Continued from
Closed Map Operations (merge)
Using a method for zipping much like in the Zipping Merge, we define a way of "folding" a closed map into itself by identifying (with each other) certain objects within it.
Assume fAText(A) and Z is a 2-place relation on A.
See Merging for definition of "matching" texts and IdPairs(t,s).
Let Z' be the smallest symmetric-transitive extension of Z such that if x(Z')y then f(x) and f(y) match and each pair of IdPairs(f(x),g(y)) satisfies Z'.
A procedure for generating Z' from Z is to iteratively compare contents of already identified pairs of objects, failing when the texts don't match, or identifying the IdPairs(?,?) if they do match, then (at each step) taking the symmetric-transitive closure.
To fold f along Z, determine Z' as above, then choose a function rAA such that r(x) = r(y) if x(Z')y, and r(x) = x if x is related to nothing by Z'. (Thus, r picks a canonical representative for each partial-equivalence class.)
The folding of fAText(A) is r* o fXText(X), where XA is the range of r over inputs from A.
Observe that folding a closed map need not result in a submap (modulo equivalence).
Cloning a collection of objects is replicating them and replacing the references to originals within the clones by references to their clones. This is probably done for the purpose of subsequently modifying some of them. If A and B are originals with clones A' and B', and if B references A, then B' references A'.
Assume fAText(A) and XA. To clone X, first choose a class B disjoint with A, and a bijection rXB with inverse r BX; let r'AB agree with r on X and be identity outside X. Then extend f from A to r'*(f(r(b))) for bB.
Splitting a closed map is cloning some objects along with all objects that refer to them, causing the closed map to branch into two equivalent closed maps, probably for the purpose of subsequently modifying a branch into a variant.
Not only is the original closed map a submap of the split, but deleting the cloned objects (and leaving the clones) would leave a closed map equivalent to the original.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html