Very far (tho I have some other, derivative-like, concepts, but much fuzzier)...
"Refinement" in this case is a CS term of art, sorry: to say that "f refines g" is to say that f's domain[0] includes g's domain, and each fibre of g^-1 includes the equivalent fibre of f^-1, so anywhere in a computation you had a g, it could safely (although not always lively![1]) be replaced with f. In particular, programs as deterministic implementations refine their indeterministic specifications.
(the best specification[2] is the closest to chaos that one can get that still does the right thing — which I guess loops back to leadership?)
The optimiser's (pedantry: we really should call it an "amelioriser") job is to reverse one of those arrows, so when the programmer writes f, the optimiser tries to discern the comm... sorry, programmer's intent to determine the spec h which coarsens f, and then substitute a g which also refines h: f <- h -> g.
[0] here JUNK simplifies by using an appropriate lattice: as Nuts (the undefined/unconstrained value) includes (~ = is included by) all defined values, we don't need to speak separately of domains: f \refines g <=> f`x ~ g`x
[1] there is a term of art from our army which refers to the art of making oneself scarce when tasks are being handed out; similarly, in CS there is a distinction between "safety" and "liveness": nothing is always a safe, albeit unproductive, thing to do.
[2] on the dual end of the lattice, in general there will be many programs in the neighbourhood of the maximally determinate that still makes progress. This is why, if we have a "science" at the spec end, when it comes to imps we instead have an "art" of hacking or a "discipline" of engineering.
yes, msn did; I hadn't found that yet when I wrote it, because I'd been expecting he'd be publishing in the same journals as, say, your fellow Ithacan Dexter Kozen.
How far is your idea of refinement from some def of “derivative”?