Rule rewriting behavior

Question

This is kind of meta-programming attempt. Below are two snippets:

Snippet 1:

Hold[Block[{}, doSomething]] /. 
 HoldPattern[Block[{vars___}, body_]] :> 
  Block[{vars, newVar}, body; newVar = 10]

Snippet 2:

Hold[Module[{}, doSomething]] /. 
 HoldPattern[Module[{vars___}, body_]] :> 
  Module[{vars, newVar}, body; newVar = 10]

The second snippet results in:

Hold[Module[{newVar$}, doSomething; newVar$ = 10]]

The first behaves as expected:

Hold[Block[{newVar}, doSomething; newVar = 10]]

Adding "$" to newVar seems to be related somehow to Module's behaviour. But how it's gets any chance to happen?

The argument of ReplaceAll is under Hold, pattern is under HoldPattern and substitution is on the right side RuleDelayed

Can anyone suggest what happens here?

Answer 1

Overview (tl;dr)

Ultimately, the difference here is due to Module being lexically scoped, while Block is dynamically scoped.

Lexically scoped constructs like With, RuleDelayed, and Function are handled differently, since they (by definition) deal with the literal syntax of the expression, not (just) the state of variables involved in it like Block does.

In general:

When replacing a pattern name inside the body of a lexically-scoped construct, Mathematica attempts to rename (alpha-convert) any bound variables of the construct by appending $ to the variable name everywhere in the construct.

But what's really happening?

How replacement works

Setup

Let's unpack that a bit, though. How do replacements in Mathematica work? There are three expressions involved:

1. the expression which we are matching against and replacing part of, which I'll call the subject of the replacement

2. the pattern being matched

3. and the substitute, which is substituted in for the pattern in the location the pattern was found. E.g.,

subject /. pattern -> substitute

There are two places that replacement actually occurs: in the subject, of course, but also in the substitute! Any named patterns in pattern, e.g. x_, which appear in substitute and which are matched in subject get written into substitute, then substitute gets inserted into the matching location in subject.

(I'm not sure whether this actually happens in sequence or all at once, but we can still think of it as happening in sequence for our purposes. Who knows—it's all internal, and you won't see it with TracePrint!)

It turns out that it's the first substitution that matters: where we substitute expressions into substitute via named patterns.

Walkthrough of the process

Let me give an example of the overall process. Consider (with a fresh kernel)

g[f[x]] /. f[y_] :> y + 2

g[f[x]] is the subject. /. looks in the subject for something which matches the pattern f[y_]; it finds f[x], and now our process begins.

Matching: Having matched the pattern f[y_] to the expression f[x] in the subject by matching y_ to x, Mathematica attaches the expression x to the pattern name y and remembers it for the duration of the replacement. (And, if it were relevant, for the duration of any subsequent matching, though in this case we are done matching.)

First ("inner") substitution, affecting substitute:

1. Mathematica looks for all the named patterns that occur in pattern, and keeps track of their names. Here, it finds the pattern name y in f[y_]. (Note that the pattern name itself is simply the symbol y here, not the pattern y_.)

2. Mathematica looks for all the instances of any pattern name which occur in substitute, which here is y + 2. It finds y.

3. It substitutes the expression it's attached to y, which is x, into the spot it found y. We now have the resultant substitute, x + 2.

Second ("outer") substitution, affecting subject: Substitute the resultant substitute, x + 2, into the spot it originally located pattern within subject. Here, Mathematica had found it as the first argument to g, so we get g[x + 2].

Introducing the $ signs

But something special happens during the inner substitution when the pattern name occurs in the second argument (or onwards) of a lexically-scoped pattern! There's actually a step "3 a" occurring immediately before step 3:

3. (a) Check if any of the collected pattern names in pattern from step (1) occur in the second argument or further of a lexically-scoped construct in substitute. If so, alpha-convert the bound variables of that construct by appending $ to the end of the symbol names of the bound variables.

So, let's see an example of this:

Hold[f[x]] /. f[y_] :> With[{z}, {y, z}]

(* Evaluates to: *)

Hold[With[{z$}, {x, z$}]]

Here the pattern name y caused z to be $-renamed.

Note that With[{z}, {y, z}] doesn't make any sense, and will give an error if evaluated. It seems Mathematica doesn't mind! Credit to the linked answer by @Kuba for figuring that out!

This is the process you're seeing—and note that it's actually because of body, which plays the role of y.

Aside: this is hackable! If you insert a variable with $ after it, Mathematica will still blindly append $ to the bound variable and therefore mistakenly bind the one you're inserting! You can avoid this by evaluating SetSystemOptions["StrictLexicalScoping" -> True], which seems to make it behave like Module. This option introduces some extra failsafes, too, which are a bit weird: for example, even just y_ :> y, evaluated by itself, becomes y$_ :> y$.

Scope of behavior

Relevant heads

As far as I can tell, the heads with lexical scoping behavior are

lexicalHeads = Alternatives[
  Function,
  With,
  Module,
  Rule,
  RuleDelayed,
  Set,
  SetDelayed
  TagSet,
  TagSetDelayed
  ]

(Stored in a pattern for later use.)

Somehow, no expressions need to be evaluated

As you noted, every expression that needs to be held is being held! How does Mathematica manage to even perform this action?

My guess is that this means that all replacements occur inside Mathematica's pattern-matcher (or somehow "adjacent" to it). It's very difficult to "get inside" Mathematica's pattern matcher, and I'm not sure how to force evaluation in it (besides via PatternTest, and that's pretty limited in scope). It would make sense to me that substitution, being dependent on the pattern-matcher's functionality, takes place inside of it. This idea is reinforced by the behavior in the following:

Pattern names need not be matched

Note that the pattern y_ doesn't need to actually be matched; it just needs to appear somewhere in pattern.

Hold[f[x]] /. (f[x] | h[y_]) :> With[{z}, y]

(* Evaluates to: *)

Hold[With[{z$}]]

What happened here was that y got replaced with something effectively like Sequence[], since it did not match anything.

But note that y didn't actually get replaced with Sequence[]—no evaluation took place. (By the way, this kind of behavior is a general phenomenon, and not related to lexical scoping.) We can determine that no Sequence[] got flattened out via the usual evaluation procedure by using heads which are are either SequenceHold or HoldAllComplete, and which would therefore prevent Sequence[] from flattening if it had been inserted:

f[x] /. (f[x] | f[y_]) :> HoldComplete[y]

(* Evaluates to: *)

HoldComplete[]

This is further evidence that the pattern matcher (or something related) is performing actions outside of standard evaluation.

Other lexically-scoped heads perform the same $-renaming

The conclusions of the question linked by @Kuba are mostly correct! However, the behavior is not limited to RuleDelayed: check it out here with Rule:

f[x] /. f[y_] -> Hold[With[{z}, z + y]]

(* Evaluates to: *)

Hold[With[{z$}, z$ + x]]

Note that definitions, as given by :=, =, and /: (and the like), are essentially replacement rules—I think they're implemented by :>, considering the output of Language`ExtendedDefinition. It's just not so obvious what the subject is, because once a definition is created, every expression with an appropriate head is considered a subject, and pattern-matching and substitution proceeds as above.

But just about every other lexically-scoped construct performs replacement as well. So, we can expect this behavior from the rest too; here it is with With and Function:

With[{x = 1}, y_ :> x + y]

(* Evaluates to: *)

y$_ :> 3 + y$

Function[{x}, y_ :> x + y][1]

(* Evaluates to: *)

y$_ :> 1 + y$

Some lexically-scoped heads bind their variables via pattern names

Note that Rule, RuleDelayed, Set, and SetDelayed are themselves lexically-scoped as well, and fall under rule 3a, but we compute their bound variables differently: instead of a list of symbols and/or initializations, their bound variables are the names of any named patterns in the first argument. Consider

f[h] /. f[x_] -> Hold@Rule[y_, x + y]

(* Evaluates to: *)

Hold[y$_ -> h + y$]

How to avoid $-renaming

A failed (but informative) attempt

We can change our substitute to avoid renaming, though! Perhaps the easiest way is to do so is to use Inactive and Activate:

Activate[
  f[x] /. f[y_] :> Hold[Inactive[With][{z = 3}, y + z]]
 ]

(* Evaluates to: *)

Hold[With[{z = 3}, h + z]]

To make it more precise and avoid inadvertently activating other inactivated heads, we can use our pattern from before:

Activate[
  f[x] /. f[y_] :> Hold[Inactive[With][{z = 3}, y + z]],
  lexicalHeads
 ]

But there's a problem with this: variables that are meant to be bound now evaluate independently! The whole body evaluates! Consider

h = 5;
Activate[x /. y_ :> Inactive[Module][{h = -1}, h]]

We get an error, because {h = -1} has evaluated by itself to {-1} before Module came into play.

A better attempt

There are lots of ways to do this: as we see from the above, the crucial thing we need to do is to hold all arguments until immediately after the replacement. Turns out, getting it to automatically do it at exactly the right time, in full generality, with access only to things inside RuleDelayed is a bit difficult. But if we can fudge on evaluation time a bit, here's an example of something that can work:

AvoidRenamingInner[x_ :> substitute_] := 
 RuleDelayed[x, #] & @@ (HoldComplete[substitute] /.
    (head : lexicalHeads)[args___] :> Hold["AvoidRenaming", head, args])

AvoidRenamingOuter[replacement_] := 
 replacement /.
  Hold["AvoidRenaming", head_, args___] :> head[args]

(* Example: *)

AvoidRenamingOuter[
 f[x] /. AvoidRenamingInner[y_ :> Function[{z}, z + y]]
]

This is pretty limited, because it only works for RuleDelayed. (I also suspect it's subject to breaking in certain nested cases.) It could likely be expanded in a cool way!

(Note: this requires lexicalHeads from earlier to be defined.)

Hope this helps; it was fun to write! :)