Parts of Module body evaluated in external scope?

Question

I have an expression that suggests that some expressions in a module body are dragging in definitions from outside the scope in a surprising way. First, consider a symbolic constant, y:

ClearAll[y]

Now, define a couple of expressions that should evaluate to this constant, one immediate and one delayed:

z = y; w := y;

Let's also define a "function" v (actually a rewrite rule in the DownValuess of v), that will return its argument:

v[y_] = y;

Now, the surprise is that if I define a local variable y in a Module, various symbolic expressions involving the symbol y, specifically w and z, seem to be evaluated in the environment outside the Module, where y evaluates to itself, and other expressions involving the symbol y, namely y, v[y], and D[y^2/2, y] seem to be evaluated in terms of the local variable. To wit:

Module[{y}, {w, v[y], y, z, D[y^2/2, y]}]  

produces

{y, y$668, y$668, y, y$668}

Naturally, if I give the local variable y a value from outside, then I don't see the secret fresh variable:

ClearAll[x];
Module[{y = x}, {w, v[y], y, z, D[y^2/2, y]}]  

produces

{y, x, x, y, x}

I surmise that what's happening is that in a pre-evaluation step, any overt occurrences of y are rewritten to the (value of the) fresh variable and then the body is evaluated. Thus, w and z don't get evaluated until after an equivalent to

ReplaceAll[Hold[{w, v[y], y, z, D[y^2/2, y]}], y -> y$668]

or

ReplaceAll[Hold[{w, v[y], y, z, D[y^2/2, y]}], y -> x]

is done.

Is my surmising correct?

Answer 1

Module does lexical scoping. This means that whatever is explicitly passed as a parameter is applied a replacement rule with the new temporary variable, just like you suggested with your ReplaceAll snippet.

If you are looking for dynamic scoping, try Block. This means that while the evaluation of the Block is taking place, all calls to the localized symbol will not find the "external" values, but only those defined while running the Block.

Block localizes the execution, Module what`s explicitly written.

I'm sure there are a couple of good in-depth answers in the forum about Block vs Module if you do a search.

Here is a small code snippet illustrating this point:

ClearAll[z, y, w]
z = y; w := y;
v[y_] = y;

Module[{y = x}, {w, v[y], y, z, D[y^2/2, y]}]    
(* ==> {y, x, x, y, x} *)

Block[{y = x}, {w, v[y], y, z, D[y^2/2, y]}]
(* ==> {x, x, x, x, x} *)

{w, v[y], y, z, D[y^2/2, y]}
(* ==> {y, y, y, y, y} *)