Variables in Pure Functions and Rules
Module and
With allow you to give a specific list of symbols whose names you want to treat as local. In some situations, however, you want to automatically treat certain symbol names as local.
For example, if you use a pure function such as
Function
, you want

to be treated as a "formal parameter", whose specific name is local. The same is true of the

that appears in a rule like

, or a definition like

.
Mathematica uses a uniform scheme to make sure that the names of formal parameters which appear in constructs like pure functions and rules are kept local, and are never confused with global names. The basic idea is to replace formal parameters when necessary by symbols with names of the form

. By convention,

is never used as a global name.
Here is a nested pure function.
| Out[1]= |  |
Mathematica renames the formal parameter

in the inner function to avoid conflict with the global object

.
| Out[2]= |  |
The resulting pure function behaves as it should.
| Out[3]= |  |
In general,
Mathematica renames the formal parameters in an object like
Function
whenever
body is modified in any way by the action of another pure function.
The formal parameter

is renamed because the body of the inner pure function was changed.
| Out[4]= |  |
Since the body of the inner function does not change, the formal parameter is not renamed.
| Out[5]= |  |
Mathematica renames formal parameters in pure functions more liberally than is strictly necessary. In principle, renaming could be avoided if the names of the formal parameters in a particular function do not actually conflict with parts of expressions substituted into the body of the pure function. For uniformity, however,
Mathematica still renames formal parameters even in such cases.
In this case, the formal parameter

in the inner function shields the body of the function, so no renaming is needed.
| Out[6]= |  |
Here are three nested functions.
| Out[7]= |  |
Both inner functions are renamed in this case.
| Out[8]= |  |
As mentioned in
"Pure Functions", pure functions in
Mathematica are like

expressions in formal logic. The renaming of formal parameters allows
Mathematica pure functions to reproduce all the semantics of standard

expressions faithfully.
| Function[{x,...},body] | local parameters |
| lhs->rhs and lhs:>rhs | local pattern names |
| lhs=rhs and lhs:=rhs | local pattern names |
| With[{x=x0,...},body] | local constants |
| Module[{x,...},body] | local variables |
Scoping constructs in Mathematica.
Mathematica has several "scoping constructs" in which certain names are treated as local. When you mix these constructs in any way,
Mathematica does appropriate renamings to avoid conflicts.
Mathematica renames the formal parameter of the pure function to avoid a conflict.
| Out[9]= |  |
Here the local constant in the inner
With is renamed to avoid a conflict.
| Out[10]= |  |
There is no conflict between names in this case, so no renaming is done.
| Out[11]= |  |
The local variable

in the module is renamed to avoid a conflict.
| Out[12]= |  |
If you execute the module, however, the local variable is renamed again to make its name unique.
| Out[13]= |  |
Mathematica treats transformation rules as scoping constructs, in which the names you give to patterns are local. You can set up named patterns either using

,

and so on, or using

.
The

in the

goes with the

, and is considered local to the rule.
| Out[14]= |  |
In a rule like

, the

which appears on the right-hand side goes with the name of the

pattern. As a result, this

is treated as a variable local to the rule, and cannot be modified by other scoping constructs.
The

, on the other hand, is not local to the rule, and
can be modified by other scoping constructs. When this happens,
Mathematica renames the patterns in the rule to prevent the possibility of a conflict.
Mathematica renames the

in the rule to prevent a conflict.
| Out[15]= |  |
When you use
With on a scoping construct,
Mathematica automatically performs appropriate renamings. In some cases, however, you may want to make substitutions inside scoping constructs, without any renaming. You can do this using the

operator.
When you substitute for

using
With, the

in the pure function is renamed to prevent a conflict.
| Out[16]= |  |
If you use

rather than
With, no such renaming is done.
| Out[17]= |  |
When you apply a rule such as

, or use a definition such as

,
Mathematica implicitly has to substitute for
x everywhere in the expression
rhs. It effectively does this using the

operator. As a result, such substitution does not respect scoping constructs. However, when the insides of a scoping construct are modified by the substitution, the other variables in the scoping construct are renamed.
This defines a function for creating pure functions.
The

and

are explicitly inserted into the pure function, effectively by using the

operator.
| Out[19]= |  |
This defines a function that creates a pair of nested pure functions.
The

in the outer pure function is renamed in this case.
| Out[21]= |  |