Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
There is an example of applying a substitution to an expression, and I am having a problem with it. Let $\theta = \{ x/f(y), y/z \}$, and $E=p(x,y,g(z))$, then $E\theta = p( f(y),z,g(z) )$.
Why is $y/z$ not applied to $E$ after using $x/f(y)$, so that the answer would be $E\theta = p( f(z),z,g(z) )$?
Because that's not how substitution is defined.
Seriously, there isn't much more to it than that. In some situations (such as applying a single step of a collection of rewriting rules), having the ability to substitute "each variable once, all at once" like this is important for the correctness of the definition. So substitution is defined so that there is a way to write these definitions correctly.
In other situations (such as the output of a unification algorithm), authors require that substitutions be idempotent, i.e. applying the substitution a second time does not change the result. This prohibits substitutions such as the one in the question, thereby avoiding the issue.
