Maude-help mailing list

[Jeff Thompson <jeff AT thefirst.org>]

A feature one expects from functions is that the output is predictable 
from the input. So, can a commutative operator in a functional module 
violate this?  Consider:
fmod TEST is
 protecting QID-SET .
 op pick : QidSet -> Qid .
 eq pick((E:Qid , S:QidSet)) = E:Qid .
endfm

Since _,_ from QidSet is commutative, it seems that
red pick(('a , 'b)) .
could return either 'a or 'b, making the output not determined by the 
input. And I can't claim I fully understand what "Church-Rosser" means, 
but it seems that with a commutative operator, different reduction paths 
could give different results.  I couldn't find it in the Maude book, but 
are there guidelines for when you lose determinism and Church-Rosser 
when you use commutative operators?

Thanks for any help,
- Jeff