Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

Hi Jeff,

All functional modules are assumed to be Church-Rosser. In the context  
of membership equational logic, being Church-Rosser means being  
confluent, terminating and sort-decreasing. You can find definitions  
of these in the Maude book, but also in other places since they are  
common terminology.

You don't "lose determinism and Church-Rosser"... your spec is simply  
not confluent.

Best,

Paco


El 26/08/2009, a las 8:23, Jeff Thompson escribió:

> 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
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help