We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, called
, are therefore an ideal basis for truly machine-independent optimizations as they hold on every machine. Besides a general
theorem, covering arbitrary call-by-value parameters and local and global variables, we also obtain two new
results: one by constraining the analysis problem to
, and one by allowing
only. Thus if we miss a constant/equality in these two scenarios, then there exists a separating interpretation of the operator symbols.