Equivalence of programs with structured variables

摘要

We consider a class of straight line programs admitting structured variables. It is easy to associate with each program a set of expressions which reflects the natural meaning of a structured variable such as an array. However, the question of whether two such expressions are equivalent depends on what is assumed about the possible initial values of the variables and what algebraic laws are assumed to apply. We give necessary and sufficient conditions for two such assumptions to yield the same equivalences among expressions. The assumption which gives the smallest set of equivalences is exhibited. This assumption plays the role of “strong equivalence,” since it implies equivalence under any possible interpretation of the model which preserves the interpretation of “structure”, as we define it.