+ Zipping Merge.

This is a way of merging two closed maps with a stipulation that certain objects be identified. Zipping can fail.

Assume f  AText(A), g  BText(B), that A and B are disjoint, and Z is a collection of pairs in AB, and that Z is one-to-one.
If t  Text(A) and s  Text(B) then let us say they "match" just when they have identical structure except for abstract id occurrences within them; wherever an abstract id occurs in one, then a possibly different id must occur in the other.
If t  Text(A) and s  Text(B) match then let IdPairs(t,s) be the collection of pairs <x,y>  AB such that x occurs in t where y occurs in s.

Given a collection Z of pairs in AB let Z' be the smallest one-to-one extension of Z such that if <x,y> is in Z' then f(x) and g(y) match and IdPairs(f(x),g(y)) is a subcollection of Z'. A procedure for generating Z' from Z is to iteratively compare contents of corresponding indices, adding the IdPairs(?,?) of the texts if they do match, or failing when either the texts don't match or adding them ruins the one-to-oneness.

To zip g into f along Z, determine Z' as above, then rename g to g' by replacing each y  B by x  A when <x,y> is in Z', then take the union of closed maps f and g' (recall that A and B are disjoint). We call the Z the zipper-start.
Then f is a submap of the zipping, and g is a renaming of a submap of the zipping. The bias towards f may be useful when f is the current closed map of a Session involving some state beyond the current closed map that mentions objects in f that would impractical to rename in that state. Then zipping is a way of merging a new closed map into f. Of course, the merge of f into g (along the inverse of Z) is simply a renaming of the merge of g into f.

A variation on zipping merge would allow A and B to overlap as long as f and g agree on the intersection of A and B, which would have the same result as renaming g by some function r to avoid A, then adding pairs <a,r(a)> to the zipper-start. This corresponds to merging a partial variant into ones current closed map.

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