Dado que Mathematica es fundamentalmente un sistema de reescritura, podemos usar el concepto de una Forma Normal para abordar tu pregunta.
Podemos formalizar el comportamiento de Mathematica de esta manera para responder a tu pregunta. Considera dos conjuntos de reglas de reescritura, que almacenarán todas las reglas que ingreses en Mathematica. En el primer conjunto, que llamaremos Eager, todos los lados derechos de las reglas se reescriben inmediatamente a sus respectivas formas normales. Sin embargo, en el segundo conjunto, que llamaremos Lazy, no se lleva a cabo tal reescritura. La correspondencia con Mathematica es que Eager es el valor predeterminado, incluido el comando Set y el bucle de lectura-evaluación-impresión; SetDelayed corresponde con Lazy.
Siguiendo el ejemplo en la documentación de Mathematica, al ingresar y = 4 en el símbolo de dólar se coloca la regla de reescritura $y \rightarrow 4$ en el conjunto de Eager:
Eager = $\{y \rightarrow 4\}$, Lazy = $\{\}$
Al ingresar z := y^2 en el símbolo de dólar se coloca la regla $z \rightarrow y^2$ en el conjunto de Lazy:
Eager = $\{y \rightarrow 4\}$, Lazy = $\{z \rightarrow y^2\}$
Al ingresar z en el símbolo de dólar, hace que z se reescriba a su forma normal utilizando la unión de Eager y Lazy.
$z \Rightarrow 16$
Ahora, si ingresamos y = 3 en el símbolo de dólar, la regla que ya está allí se reemplaza:
Eager = $\{y \rightarrow 3\}$, Lazy = $\{z \rightarrow y^2\}$
Por lo tanto, al ingresar nuevamente z hace que se reescriba a su forma normal:
$z \Rightarrow 9$
La lógica subyacente en este ejemplo es ecuacional, es decir, lógica de primer orden con funciones e igualdad. En este contexto, las reglas de reescritura son simplemente ecuaciones con una dirección preferida.
En cuanto a variables como x_, no veo algo correspondiente en las reglas de reescritura a este tipo de notación. Mi suposición es que este formalismo está diseñado para inhibir el evaluador predeterminado de Mathematica, ya que si ya tenemos x = 3 y escribimos lo siguiente en Mathematica....
f[x] := x^2
... obtendríamos
f[3] := x^2
... lo cual claramente no es lo que queremos. Los sistemas de reescritura evitan este problema al no hacer que las asignaciones constantes como x = 4 sean reglas de reescritura. Esto es necesario ya que es importante poder reescribir los lados izquierdos de las reglas de reescritura en sus formas normales, no solo los lados derechos.
