CMP.12:2 - Problem

How can expression meaning be turned into effective evaluation and translation rules, so that the resulting computation preserves the observations needed by its user?

A mathematical interpretation can assign a meaning without providing an algorithm for obtaining it. A text substitution can preserve printed names while changing what they refer to. A translation can return the right value on a simple test while evaluating an unwanted branch, capturing another binding or failing to terminate on a previously terminating input.