Annotation-based forward slicing

[explorable-viz]

Annotation-based forward slicing

[rolyp]

It seems there's an inconsistency between the idea that values can be "shared" (e.g. bound to a variable which is used non-linearly) and the idea that availability annotations are combined conjunctively. If I bind a particular instance of the number 5 to x, and then use x in two places with distinct availabilities, I cannot reflect those distinct availabilities at the uses, because they have to be intersected. There is a similar situation with all the non-terminal forms (application, let, etc), since they share values with a subcomputation.

It's worth noting that it is sharing within a computation which is problematic for slicing, whereas for "differential" execution we are actually only interested in sharing across computations. Perhaps we can somehow have the latter in a useful way while precluding the former?

Related thought: I haven't yet considered how this notion of (where?) provenance is related to the scheme for identifying nodes in the computation. If we identify nodes in such a way that (otherwise shared) nodes are always discriminated by their "usage" context (e.g. so that for example the identity of the value of an application depends on the identity of the application expression), then perhaps these notions start to become related: my identity is the set of nodes that need to be available for me to be available, and my availability is the conjunction of the availability of those nodes.