I am trying to find out whether there is a standard notion of generalizing indexing such as $\sum_i$ to function applications as in $\sum_{f(x)}$. Intuitively, the latter means "iterating over all values of $f(x)$, while leaving the other points in $f$ unchanged."
This naturally extends to other quantifications such as in
$$\exists income(x) : income(x) = income(Mary) + income(John)$$
which means "is there a possible income for x which is equal to the sum of Mary's and John's incomes?" (there may be external constraints on the income for the various persons).
Note that $x$ is a free variable and might have value equal to $Mary$ or $John$ (for example, this may be in a context in which $x$ ranges over all people).
This is different from
$$\exists x : income(x) = income(Mary) + income(John)$$
which asks a very different question: whether there is someone with that income.
The problem however is that $\exists$ is defined for variable symbol indices, not function applications such as $income(x)$.
Here is what I mean more formally: in a mathematical expression such as
$$ \sum_{x_1} \sum_{x_2} (x_1 + x_2) $$
the usual interpretation is that $x_1$ and $x_2$ are two distinct variable symbols. These symbols are "atomic", in the sense that the fact that $x$ is used in both of them is irrelevant; either variable could be renamed to $y$ without a problem.
However, if one writes
$$ \sum_{i,j}^n \sum_{x_i} \sum_{x_j} (x_i + x_j) $$
$x_1,\dots,x_n$ can no longer be considered distinct variable symbols; when $i=j$, $x_i$ and $x_j$ must have the same value. Renaming variables here would alter the meaning.
Instead, in this second expression $x$ is a function, and $x_i$ could be written as $x(i)$. This however introduces the issue of what $\sum_{x(i)} \psi$ means.
It is not too hard to see that this generalization of summation over simple variables can be defined as follows:
$$ \sum_{f(i)} \psi \equiv \sum_{f' : k \neq i \Rightarrow f'(k) = f(k)} \psi[f/f'],$$ where $\psi[f/f']$ is the result of replacing $f$ by $f'$ in $\psi$.
($\sum_{f': k \neq i \Rightarrow f'(k) = f(k)}$ stands for "summation over function $f'$ such that $f'(k)=f(k)$ if $k \neq i$".)
In other words, $f$ "inside" $\psi$ is replaced by a $f'$ which is a copy of $f$ everywhere but in $i$, leaving it to range over its possible values. This effectively computes the summation with $f(i)$ ranging over all its possible values.
This expansion is however cumbersome. It would be convenient to have instead a generalized indexing notation. I could do it myself but I am wondering if this has already been done.
One might think this is an odd, esoteric notion, but it does come up. For example, in the Bayesian network inference literature one sees informal uses of this all the time when marginalizing over random variable assignments:
$$ P(X_i = x_i) = \sum_{x_1} \dots \sum_{x_{i-1}} \sum_{x_{i+1}} \dots \sum_{x_n} \prod_j P(X_j=x_j|Pa_j=pa_j) $$
where $Pa_j$ is the parents of random variable $X_j$ in the network.
So my question is whether there is a standard name for this concept. I would also like to know if Mathematica or other algebra systems have the ability to represent this.