finding constantness of a term Let $S$ be a multisorted algebraic signature with function symbols $f_0, f_1, \ldots$. For every $i$, I partially know “constantness” of $f_i$. (I have no precise definition of constantness yet.) Examples:


Let $\cdot$ denote multiplication of numbers. If $x_0=0$, then $x_0\cdot x_1$ is constant.
Conditional operation. If $x_0=0$ and $x_2$ is constant, then  $\operatorname{if}x_0\operatorname{then}x_1\operatorname{else}x_2$ is constant.


I need to find a strongest constantness judgement for any term over $S$ given constantness of its variables. Is there an established way of reasoning about constantness?

A purpose is that every term in $S$ defines a function from program states to a pixel on a screen. Variables of the term are components of a state, i.e. the set of states is a Cartesian product. For every pixel $p$, if its term is found to be non-constant then I need to redraw $p$.
You might want to take a look at the compiler literature for some ideas.  What you're describing is akin to a well-known compiler optimization (virtually any modern compiler worth its salt will do it) called constant folding.  Of course, constant folding goes further in not just identifying constant expressions, but replacing them by their value.

In particular, compilers use a dataflow analysis to identify such constant expressions.  Any good compiler textbook will discuss this.