Maude-help mailing list

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

Hi Marc,

What is supposed to be the sort of bc? When you reduce bc you expect it to be 
of sort B or C?

All terms are supposed to have a unique least sort. It is like being 
non-confluent, but in the more general case of  membership equational logic.

Your example is equivalent to the following.

fmod TEST-MB3 is 
  sorts A B C .
  subsorts B C < A .
  op b : -> B . 
  op b : -> C .
endfm 

which gives you a warning.

Francisco



El 13/04/2011, a las 16:01, Marc Boyer escribió:

> Dear maude users,
> 
> I have a term which is a member of two subsorts. But I can not manage to 
> tell Maude to see both membership without declaring a new subsort.
> 
> Here is a minimal example:
> 
> fmod TEST-MB2 is
>   sorts A B C  .
>   subsorts B < A .
>   subsorts C < A .
> 
>   op bc : -> A .
>   mb bc : B .
>   mb bc : C .
> endfm
> 
> red bc :: B .
> red bc :: C .
> 
> Of course, I could declare a new sort BC, subsort of B and C, but in
> my real problem, it does not match any "real" sort, and I would like to
> avoid it.
> 
> Regards,
>    Marc Boyer
> -- 
> Marc Boyer, Ingenieur de recherche                              ONERA
> Tel: (33)  5.62.25.26.36                                         DTIM
> Fax: (33)  5.62.25.26.52                          2, av Edouard Belin
> http://www.onera.fr/staff/marc-boyer/          31055 TOULOUSE Cedex 4
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help