Condition and RuleDelayed

Question

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?

Answer 1

This was somewhat too long for a comment. Not sure it answers the question but it might give a way of thinking about the elusive handling of Condition that proves helpful.

The behavior in question is fairly well documented (I think people know this, I just wanted to state it for the record). The general idea to RuleDelayed is that it fires on a match and delivers its rhs. The devil in the details can be broken into two questions. (1) What comprises a match? (2) What is the evaluation of the rhs?

When Condition is present on the rhs we do get into some murky semantics issues. The gist is that it is part of what determines whether there is a match, which is to say that the lhs alone does not suffice (I believe this is the only exception to the general rule that the lhs determines a match). As for what is the evaluated rhs, if the Condition is True then the rhs is what preceded that condition. If it is not True then the issue is moot because the delayed rule is not going to fire. Which is the point of having this construct to begin with.

Answer 2

Actually, both

FullForm@Hold[lhs /. lhs :> (rhs /; test)]

and

FullForm@Hold[lhs /. lhs :> rhs /; test]

yield the same:

Hold[Replace[lhs,RuleDelayed[lhs, Condition[rhs,test]]]]

and this Replace evaluates as the documentation says it does. I think you misunderstand Condition as an If construct that evaluates to something on its own. But it seems to me that Condition is closely tied to ReplaceAll as you can make reference to pattern names appearing only in the left hand side of some (delayed) rule. Consider, for example,

lhs[1, 2, 3] /. x_ :> (rhs /; (x > 2))]

(lhs[1, 2, rhs]) and its FullForm.

On the other hand, you can "switch-off and on" the condition by typing

Condition@@(lhs/.lhs:>NoCondition[rhs,True])

Im not sure if that answers your question, though. (Are you asking out of curiosity or do you have some application in mind, where you would need the ReplaceAll to return expressions with head Condition?)