Related question concerning interpretation of the substitutions:

Subtle order-of-evaluation issues when pattern-matching with attributes

Questions researched before posting this one:

Orderless pattern matching

Combinations of multiple matching patterns

About OneIdentity

What has changed in pattern matching functions with the Orderless attribute?

Transformation rule for arbitrary number of argument expressions

Pattern does not match with Orderless head

All work done with Mathematica on Ubuntu 18.04 (bionic)

In an attempt to understand pattern-matching better, I tried some exhaustive testing of a certain substitution rule under all seven combinations of attributes, leaving out the null case of no attributes:

In[1]:= allAtts =
   Union[Sort /@
     Permutations[{Flat, Orderless, OneIdentity}, {i}]], {i, 3}], 1]
Out[1]= {{Flat}, {OneIdentity}, {Orderless}, {Flat, OneIdentity}, {Flat,
  Orderless}, {OneIdentity, Orderless}, {Flat, OneIdentity,

The substitution rule attempts to match the pattern eqv[x_, y_] against the input eqv[p, q, r] to see what gets bound to x and y for each combination of attributes.

In the first test, I define the substitution before setting the attributes. After some manual prettification:

In[2]:= Table[Module[{e = (eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}})},
    SetAttributes[eqv, j];
    {j, First@e, Rest@e}],
  {j, allAtts}]
Out[2]= {{{Flat},                         p, eqv[q, r]},
         {{OneIdentity},                  eqv[p], {eqv[q, r]}},
         {{Orderless},                    p, eqv[q, r]},
         {{Flat, OneIdentity},            p, eqv[q, r]},
         {{Flat, Orderless},              p, {eqv[q, r]}},
         {{OneIdentity, Orderless},       q, {eqv[p, r]}},
         {{Flat, OneIdentity, Orderless}, p, eqv[q, r]}}

The results are reasonable, plausible, interpretable. I won't go into interpreting the results in this post other than to note that the results are subtly different when attributes are set before the substitution rule is parsed. The subject of this post is that unrolling the tests produce very different, not subtly different, results. Because I unroll below under both conditions --- substitution parsed before attributes set and attributes set before substitution parsed --- here are the results of the latter, subtly different:

In[3]:= Table[Module[{e},
    SetAttributes[eqv, j];
    e = (eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}});
    {j, First@e, Rest@e}],
  {j, allAtts}]
Out[3]= {{{Flat},                         eqv[p], {eqv[q, r]}}, (* difft *)
         {{OneIdentity},                  p, eqv[q, r]},        (* difft *)
         {{Orderless},                    p, eqv[q, r]},
         {{Flat, OneIdentity},            p, {eqv[q, r]}},      (* difft *)
         {{Flat, Orderless},              q, {eqv[p, r]}},      (* difft *)
         {{OneIdentity, Orderless},       p, eqv[q, r]},        (* difft *)
         {{Flat, OneIdentity, Orderless}, p, {eqv[q, r]}}}

In a separate post, I have questions about interpreting the results. I Continue here with the main question about unrolling.

I now attempt to unroll these tests, one test for each combination of attributes rather than one table with all combinations. I get many surprises that reveal I don't really understand what's going on. I highlight these surprises below and would be grateful for explanation and clarification.

First, here is my attempt at unrolling the tests:

In[3]:= test32substBeforeAttrs[attrs_] := Module[{eval},
  eval[] := eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}};
  ClearAll[eqv]; SetAttributes[eqv, attrs]; eval[]]

I try to prevent any early evaluation of the substitution by packaging it in a delayed rule named eval, but I do want the substitution denoted and parsed before attributes are set, which (I thought), were the same conditions as in the rolled-up test.

Surprise number one, the Flat results look similar to the test where attributes are set before the substitution rule is parsed, just without a list enclosing the second binding for y:

In[5]:= test32substBeforeAttrs[{Flat}]
Out[5]= {eqv[p], eqv[q, r]}

Surprise number two, we get no matches for OneIdentity alone and for Orderless alone:

In[6]:= test32substBeforeAttrs[{OneIdentity}]
Out[6]= eqv[p, q, r]
In[7]:= test32substBeforeAttrs[{Orderless}]
Out[7]= eqv[p, q, r]

No surprises for {Flat, OneIdentity}:

In[8]:= test32substBeforeAttrs[{Flat, OneIdentity}]
Out[8]= {p, eqv[q, r]}

but surprise number three for {Flat, Orderless}: p and q are reversed, just like the rolled-up case for {OneIdentity, Orderless}, except, again, no list enclosing the second binding, the binding for y:

In[9]:= test32substBeforeAttrs[{Flat, Orderless}]
Out[9]= {q, eqv[p, r]}

Surprise number four: no match for unrolled {OneIdentity, Orderless}:

In[10]:= test32substBeforeAttrs[{OneIdentity, Orderless}]
Out[10]= eqv[p, q, r]

No surprise for the case of all attributes.

In[11]:= test32substBeforeAttrs[{Flat, OneIdentity, Orderless}]
Out[11]= {p, eqv[q, r]}

Now, my attempt at an unrolled setting of attributes before denoting and parsing the substitution rule. Again, I attempt to prevent early evaluation by packaging my main substitution rule in an outer, delayed substitution rule named eval:

In[12]:= test32AttrsBeforeSubst[attrs_] := Module[{eval},
  ClearAll[eqv]; SetAttributes[eqv, attrs];
  eval[] := eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}};

In[13]:= test32AttrsBeforeSubst[{Flat}]
Out[13]= {eqv[p], eqv[q, r]}
In[14]:= test32AttrsBeforeSubst[{OneIdentity}]
Out[14]= eqv[p, q, r]
In[15]:= test32AttrsBeforeSubst[{Orderless}]
Out[15]= eqv[p, q, r]
In[16]:= test32AttrsBeforeSubst[{Flat, OneIdentity}]
Out[16]= {p, eqv[q, r]}
In[17]:= test32AttrsBeforeSubst[{Flat, Orderless}]
Out[17]= {q, eqv[p, r]}
In[18]:= test32AttrsBeforeSubst[{OneIdentity, Orderless}]
Out[18]= eqv[p, q, r]
In[19]:= test32AttrsBeforeSubst[{Flat, OneIdentity, Orderless}]
Out[19]= {p, eqv[q, r]}

The big surprise here is that the results are exactly the same as the unrolled test with substitution parsed before attributes set.

To summarize, in addition to the four little surprises when unrolling the tests, there is a big surprise that the relative order of denoting the rule matters when the tests are rolled up and not when the tests are unrolled.

I've managed to confuse myself mightily, here, and would be grateful for insights from those who understand both the big picture and the micro details better than I do. I apologize for the length and complexity of this question, but I made it as short and as simple as I know how to. The gist of this question is that I don't know nearly as much as I thought I did about pattern-matching and attributes. Perhaps after I learn more from you-all, a much simpler form of the essential question --- hiding in here somewhere I hope --- will emerge.

  • $\begingroup$ That's a lot of information. $\endgroup$ – user6014 Oct 7 '18 at 22:25
  • $\begingroup$ i’m writing a proof assistant in Mathematica. I need to understand every tiny detail of its pattern-matching. $\endgroup$ – Reb.Cabin Oct 7 '18 at 23:05

Carl Woll, in a comment in the related question Subtle order-of-evaluation issues when pattern-matching with attributes, provided the clue that cleared the air for me. My original tests were misleading because I failed to notice that there are no matches when there is no Flat. To see this, I should have returned e instead of First[e] and Rest[e], because only e reveals that there was no match; when there is no match, First[e] produces p and Rest[e] produces eqv[q,r] and I was mislead by assuming those were the results of a match when, in fact, they are simply the ordinary deconstruction of eqv[p,q,r] into its first part p and its "rest" part eqv[q,r].

There are no differences between the case when substitution is defined (in a delayed-rule pseudo-function) before attributes are set and then case when the attributes are set before the substitution is defined, as revealed by the remaining meaningful tests below.

It makes no sense to set attributes after a substitution rule is applied, as Carl points out, but there are cases where setting attributes before or after definitions makes a difference (see the "Questions researched," above). But the order does not make a difference in this case.

In[1]:= Module[{}, ClearAll[eqv]; SetAttributes[eqv, {Flat}]; 
 eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}}]

Out[1]= {eqv[p], eqv[q, r]}

In[2]:= Module[{}, ClearAll[eqv]; 
 SetAttributes[eqv, {Flat, OneIdentity}]; 
 eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}}]

Out[2]= {p, eqv[q, r]}

In[3]:= Module[{}, ClearAll[eqv]; 
 SetAttributes[eqv, {Flat, Orderless}]; 
 eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}}]

Out[3]= {q, eqv[p, r]}

In[4]:= Module[{}, ClearAll[eqv]; 
 SetAttributes[eqv, {Flat, OneIdentity, Orderless}]; 
 eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}}]

Out[4]= {p, eqv[q, r]}

In[5]:= Module[{e}, ClearAll[eqv];
 e[] := eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}};
 SetAttributes[eqv, {Flat}]; e[]]

Out[5]= {eqv[p], eqv[q, r]}

In[6]:= Module[{e}, ClearAll[eqv]; 
 e[] := eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}};
 SetAttributes[eqv, {Flat, OneIdentity}]; e[]]

Out[6]= {p, eqv[q, r]}

In[7]:= Module[{e}, ClearAll[eqv]; 
 e[] := eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}};
 SetAttributes[eqv, {Flat, Orderless}]; e[]]

Out[7]= {q, eqv[p, r]}

In[8]:= Module[{e}, ClearAll[eqv]; 
 e[] := eqv[p, q, r] /. {eqv[x_, y_] :> {x, y}};
 SetAttributes[eqv, {Flat, OneIdentity, Orderless}]; e[]]

Out[8]= {p, eqv[q, r]}

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.