Slicing based on lattice annotations

[explorable-viz]

Slicing based on lattice annotations

[rolyp]

Spent some time trying to prove a Galois connection for evaluation based on "explained values", which is covariant in the value component and contravariant in the trace component. This seemed to make some kind of sense, although it was complicated by the fact that the trace itself contains (interim) values and that the eval-after-uneval is decreasing with respect to these, as it is with other parts of the trace.

However, I don't think this idea makes sense: evaluation isn't monotone with respect to such a "mixed variance" partial order. (Eval with a bigger program produces a bigger trace.) The reason eval-after-uneval is decreasing with respect to the trace is because the trace isn't really part of the output, but rather represents something that happened in the past: thus when we erase part of the output and do eval-after-uneval, we preserve the relevant part of the output, but "decrease the past".

A more sensible strategy will probably be to define uneval purely in terms of some kind of proof tree for eval, prove the GC with values only as the codomain, and then separately show how one of our "explained values" can be obtained from any value equipped with the appropriate proof tree for eval.