Maude-help mailing list

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

Hi Emmnuel,

The Church-Rosser property describes the conditions that an equational  
specification needs to satisfy to be executable, by using its  
equations as oriented simplification rules. In the unsorted and many- 
sorted cases only confluence (and termination) is required. But in the  
order-sorted (and membership) cases sort-decreasingness is also  
required. Basically, a rewrite step can never change the type of your  
term to a bigger sort.

Regards,

Francisco


El 17/08/2010, a las 10:59, Emmanuel Castro escribió:

> Thank you, your explanations have me the things clearer. I am still
> puzzled with the subtlde difference between confluence and
> Church-Rosser properties. In many texts, they are stated as
> equivalent.
>
> e.g.
> http://en.wikipedia.org/wiki/Confluence_(abstract_rewriting)
> Term Rewriting Systems by J. W. Klop
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help