On this site I found, for example here, some very interesting questions and answers on the use of delayed rules with conditions. I would very much like to understand these answers, but so far I failed on a very basic level.
The documentation states that Condition
is an expression with two arguments: a pattern and a test. Such an expression is itself a pattern, which is matched only by expressions that match the first argument and moreover for which the evaluation of test gives True
.
Since the lefthand side of a rule is a pattern, the following works:
lhs /. (lhs/;True) :> rhs
(* rhs *)
My problem in understanding has to do with Condition
in the right hand side of a rule. The documentation states that lhs :> rhs /; test
represents a rule which applies only if the evaluation of test
yields True
. Such a rule is in fact a normal RuleDelayed
, with the Condition
expression as the second argument.
A Condition
expression evaluates to itself, even when the second argument is True
:
Condition[rhs,True]
(* rhs/;True *)
When I use a RuleDelayed
, my understanding is that the unevaluated right hand side is substituted for any subexpression that matches the pattern of the left hand side, and then a further evaluation of the expression takes place. Therefore, I expected the result of the following two commands to be respectively Condition[rhs, False]
and Condition[rhs, True]
.
lhs /. lhs:>(rhs /; False) (* lhs *)
lhs /. lhs:>(rhs /; True) (* rhs *)
In the first example the rule is not used at all, in agreement with the documentation for Condition
, but not in accordance with my understanding of RuleDelayed
. In the second example, the rule is used, but moreover at some point the right hand side is evaluated to its first argument.
So my impression is that when we have a RuleDelayed
with a Condition
in the right hand side, the evaluation rules seem to be different from those without the Condition
. That is something I cannot believe. So can someone point me to what I do not properly understand?
Condition
can be viewed as a pattern, or, pattern-buiding block, it does not surprise me that it behaves in the special way in the context of the pattern-matching. But I think that the source of this behavior is not inCondition
, but in the pattern-matcher, into whichCondition
must be wired pretty deeply. When the pattern-matcher sees a rule withCondition
, it evaluates and matches that rule in a special way. The fact thatCondition
does keep the test code unevaluated, does not mean that it is actually the function that eventually evaluates it - ... $\endgroup$ – Leonid Shifrin Jan 23 '16 at 21:03RuleCondition
and$ConditionHold
. The evaluations inCondition
are induced by the pattern-matcher, and are sub-evaluations from the point of view of the main evaluation process for the original expression.Condition
taken standalone may behave completely differently, and that does not violate the evaluation rules. $\endgroup$ – Leonid Shifrin Jan 23 '16 at 21:06