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$.
finding constantness of a term
lo.logic;pl.programming languages