SetDelayed not working as expected

Question

According to the manual, "A variable defined with SetDelayed is evaluated every time it is used". The code below suggests otherwise.

x : t[a_] /; ! TrueQ[c] := Block[{c = True}, w[x]];

w /: Times[a_w, b__] /; ! TrueQ[c] := 
  Block[{c = True}, 
   w[Times @@ Replace[Prepend[{b}, a], x_w :> x[[1]], {1}]]];

e := a t[1]

output = {a t[1], e, e, a t[1]}

The output is

{w[a t[1]], w[a t[1]], a t[1], w[a t[1]]}

The first element is the result of evaluating the same expression as the right hand side of the definition of e. That is a t[1] -> w[a t[1]] as expected.

The second element is the first evaluation of e. That is e -> w[a t[1]] as expected. The first and second elements are equal to each other because they both evaluate a t[1].

The third element is the second evaluation of e. However, this time e -> a t[1]. In my understanding of the manual, this entry should be w[a t[1]] not a t[1].

The fourth element is there to check if there is an issue with successive evaluations of a t[1]. It evaluates to w[a t[1]] as expected.

Question: What is part of the evaluation process that causes the unexpected result?

Answer 1

Consider the following simpler modification of the example that still has similar behavior

x : t[] /; ! TrueQ[c] := Block[{c = True}, w[x]]
e := t[];
{e, e, e}

{w[t[]], t[], t[]}

What is happening on the second and third attempt is that the evaluator thinks (in this case, incorrectly) that the expression is up to date and hence does not need to be reevaluated from scratch.

There is a relevant description near the end of the "Controlling Infinite Evaluation" tutorial

Some of the trickiest cases occur when you have rules that depend on complicated /; conditions (see "Putting Constraints on Patterns"). One particularly awkward case is when the condition involves a "global variable". The Wolfram Language may think that the evaluation is finished because the expression did not change. However, a side effect of some other operation could change the value of the global variable, and so should lead to a new result in the evaluation. The best way to avoid this kind of difficulty is not to use global variables in /; conditions. If all else fails, you can type Update[s] to tell the Wolfram Language to update all expressions involving s. Update[] tells the Wolfram Language to update absolutely all expressions.

The documentation for Update has another example with a /; condition along the lines of

Quit[]

t[] /; c := 0;
e := t[]
e

(* t[] *)

c = True;
e

(* t[] *)

where the value of e should have changed, but did not. One would need to run Update manually each time when c changes to obtain a freshly evaluated result.

Update[t];
e

(* 0 *)

This is essentially an internal performance optimization that saves a lot of work, at the cost of having to rely on Update in certain relatively rare circumstances to obtain the desired results.

Using Update will never give you incorrect results, although it will slow down the operation of the system.