The Weak Map

A weak map has a mutable abstracted state consisting of a set of ordered pairs. There are just two orders on a Weak Map m:

m.add(x, y) which adds the pair (x, y) to the set, displacing any previous (x, z) that might have been in the set.
m.get(x) which returns false if there is no pair in the set whose first element is x, and y if (x, y) is in the set.

Note the absence of any order to enumerate the state elements. Such a function, WeakMap, is proposed for JavaScript.

The Weak Map is primitive and thus in a position to know that for a particular member of the set (x, y) that x is the only reference in the system and the pair may safely be deleted as m.get(x) can never be performed. Circular references within the weak map do not themselves constitute a reason to maintain the referenced objects in the real state; they remain in the abstract state.

Here is a Gutag definition assuming that wmg is the function that produces empty weak maps.

getV(wmgS(), x)= false
getV(addS(s, (x, y)), x) = y
getS(s, get(x)) = s

Keykos has the KID (Key indexed directory) which maps from keys to integers. It holds the rare capability to see the bits of a capability and can eliminate keys that have expired. The KID also abstracts the key-set and thus provides the inclusion test, and intersection and union operations.

Synergy

Here Mark Miller builds sealer-unsealer pairs from WeakMap. (See the inner JavaScript.)

Just now (2017 May) I see no objection to a weak map providing a method to spill its caps. One can argue that the holder of a cap to a weak map could have held onto all the caps he put into the map. If the creator of the map wants to pass the map to someone who should not have those caps he can easily produce a facet that omits retrieval. The map code could easily do this itself. This is an economic issue. The Keykos KID exploits the fact that the keys are not kept.