Question on nested Unevaluated

Question

When trying to simulate the evaluation behavior of RuleDelayed I faced unexpected behavior of nested Unevaluated. Consider:

In[1]:= f[Verbatim[Unevaluated][expr_]] := f[expr]
f[Unevaluated[1 + 1]]
f[Unevaluated@Unevaluated[1 + 1]]
f[Unevaluated@Unevaluated@Unevaluated[1 + 1]]
f[Unevaluated@Unevaluated@Unevaluated@Unevaluated[1 + 1]]

Out[2]= f[Unevaluated[1 + 1]]

Out[3]= f[2]

Out[4]= f[Unevaluated[1 + 1]]

Out[5]= f[2]

One can see that only even number of nested Unevaluated wrappers are completely removed. Why?

Answer 1

The key is that, effectively, one layer of Unevaluated is removed before the expression is pattern-matched. From the docs:

f[Unevaluated[expr]] effectively works by temporarily setting attributes so that f holds its argument unevaluated, then evaluating f[expr].

Thus, in the first case, f[Unevaluated[1 + 1]] is evaluated as f[1 + 1], but remaining unevaluated during pattern matching even though f lacks Hold* attributes, and since nothing matches f[1 + 1], the original expression (pre-pattern-matching) is returned unevaluated.

In the second case, f[Unevaluated[Unevaluated[1 + 1]]] evaluates as f[Unevaluated[1 + 1]] in the pattern-matcher, which does match a pattern for f, and then f[1 + 1] is evaluated recursively, and thus you get f[2].

In the third case, f[Unevaluated[Unevaluated[Unevaluated[1 + 1]]]] evaluates as f[Unevaluated[Unevaluated[Unevaluated[1 + 1]]]], matches, and recursively evaluates as f[Unevaluated[1 + 1]], and we're back to the first case.

In the fourth case, f[Unevaluated[Unevaluated[Unevaluated[Unevaluated[1 + 1]]]]] matches on f[Unevaluated[Unevaluated[Unevaluated[1 + 1]]]], recursively evaluates f[Unevaluated[Unevaluated[1 + 1]]], and we're back to the second case.

HTH!

Answer 2

Use Trace to see why:

In[1]:= f[Verbatim[Unevaluated][expr_]]:=f[expr]

In[2]:= f[Unevaluated[1+1]]//Trace
Out[2]= {f[1+1],f[Unevaluated[1+1]]}

1. Due to the defining special property of the Unevaluated language construct, f[Unevaluated[1 + 1]] evaluates just like f[1 + 1] except the 1 + 1 is left unevaluated.
2. f[1 + 1] does not match the definition you gave for f.
3. Therefore f[Unevaluated[1 + 1]] remains unevaluated.

Whereas:

In[3]:= f[Unevaluated@Unevaluated[1 + 1]] // Trace
Out[3]= {f[Unevaluated[1+1]],f[1+1],{1+1,2},f[2]}

1. Due to the defining special property of the Unevaluated language construct, f[Unevaluated@Unevaluated[1 + 1]] evaluates just like f[Unevaluated[1 + 1]] except the Unevaluated[1 + 1] is left unevaluated.
2. f[Unevaluated[1 + 1]] matches the definition you gave for f, and evaluates to f[1 + 1].
3. Therefore f[Unevaluated@Unevaluated[1 + 1]] evaluates to f[2].