A formal definition of mutation independence

Louis Dionne poses the problem of move independence in the context of C++, that is, under which conditions a sequence of operations

f(std::move(x));
g(std::move(x));

is sound in the sense that the first does not interfere with the second. We give here a functional definition for this property that can be applied to the case Louis discusses.

Let X be some type and functions f: X → T×X and g: X → Q×X. The impurity of a non-functional construct in an imperative language such as C++ is captured in this functional setting by the fact that these functions return, besides the output value itself, a new, possibly changed, value of X. We denote by f_T and f_X the projection of f onto T and X, respectively, and similarly for g. We say that f does not affect g if

 g_Q(x) = g_Q(f_X(x)) ∀x∈X.

If we define the equivalence relationship ~_g in X as

x ~_g y iff g_Q(x) = g_Q(y),

then f does not affect g iff

f_X(x) ~_g x ∀x∈X

or

f_X([x]_g) ⊆ [x]_g ∀x∈X,

where [x]_g is the equivalence class of x under ~_g.

We say that f and g are mutation-independent if f does not affect g and g does not affect f, that is,

f_X([x]_g) ⊆ [x]_g and g_X([x]_f) ⊆ [x]_f ∀x∈X,

The following considers the case of f and g acting on separate components of a tuple: suppose that X = X₁×X₂ and f and g depend on and mutate X₁ and X₂ alone, respectively, or put more formally:

f_T(x₁,x₂) = f_T(x₁,x'₂),
f_X2(x₁,x₂) = x₂,
g_Q(x₁,x₂) = g_Q(x'₁,x₂),
g_X1(x₁,x₂) = x₁

for all x₁, x'₁ ∈ X₁, x₂, x'₂ ∈ X₂. Then  f and g are mutation-independent (proof trivial). Getting back to C++, given a tuple x, two operations of the form:

f(std::get<i>(std::move(x)));
g(std::get<j>(std::move(x)));

are mutation-independent if i!=j; this can be extended to the case where f and g read from (but not write to) any component of x except the j-th and i-th, respectively.