Maude-help mailing list

[Marc Boyer <Marc.Boyer AT onera.fr>]

Francisco Durán a écrit :
> Dear Marc and Min,
>
> But you have to worry about warnings, because sooner or later you may  
> get undesired results. And what is worst, you cannot trust what you  
> get. Maude assumes preregularity, and the user is responsible to get it.
>
> In this case what is happening is just that you are getting to  
> different instantiations of lists that are in the same connected  
> component. You can solve the problem by renaming the conflicting  
> operators. You can find below the compete specification where the  
> LIST{FUNCTION-ARG}{F} modulo gets all the sorts and operators coming  
> from LIST renamed (I'm sure you can find a more appropriate  
> renaming ;)).

  Your solution is Maude-compatible but does not address the problem
I am facing.
  In your solution, you can no more map any List{Nat}.

  My problem is the following: I have List{Nat}, and I want to map
several functions in different parts of the code. For example,
to use INC and in another equation LARGE, on the same List.

  Moreover, I do not understand why Maude complains about
pre-regularity.
  Let us just consider the sorts, Nat, List{Nat} and List{Arg}
and operator _ _ (my Maude 2.4 complains about this)

> Warning: sort declarations for operator __ failed preregularity 
> check on 21 out of 64 sort tuples. First such tuple is 
> (List{Nat}, Nat).

  I am considering definition of pre-regularity in the Maude book
(p 50) or in the Maude Manual (p30). it says that, for all signatures
   _ _ : S'1 S'2 -> S'3 .
it must exist some least Sorts S1, S2 and S3 such that
   Si < S'i

  And with declarations
List{Nat} < List{Arg}
NeList{Nat} < NeList{Arg}
  I was expecting to have the condition satisfied...

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