Maude-help mailing list

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

Hi Lorenzo,

I suppose that the problem comes down to something like 

fmod FOO is
  pr SET{List{String}} . 
  pr SET{String} .
endfm

In this case, Maude advises about the importation of operators from different 
modules and warns about preregularity issues. The problem comes from terms 
like 
  "a", "b"
which can be both of sorts Set{List{String}} and Set{String}. But also about 
terms like 
  insert("a", "b")

We have in the same component  sorts Set{List{String}}, Set{String}, 
List{String}, String, ... and operators with no minimum declarations. There 
is no covariance, but you can add it. 

fmod FOO is
  pr SET{List{String}} .
  pr SET{String} .
  subsorts Set{String} < Set{List{String}} .
  subsorts NeSet{String} < NeSet{List{String}} .
endfm

This module still produces advisories about the double importation of 
operators, but Maude doesn't complain about pre-regularity. 

If you want to keep them unrelated, or even with the subsort relations added, 
you can use renamed copies as in

fmod FOO is
  pr SET{List{String}} .
  pr (SET * (op empty to empty2,
    op _,_ to _;_,
    op insert to insert2,
    op delete to delete2,
    op _in_ to _in2_,
    op |_| to |_|2,
    op $card to $card2,
    op union to union2, 
    op intersection to intersection2,
    op $intersect to $intersect2,
    op _\_ to _\2_,
    op $diff to $diff2,
    op _subset_ to _subset2_,
    op _psubset_ to _psubset2_)){String} .
endfm

Best regards,

Paco

> On 18 Nov 2023, at 00:03, Steven Eker <steveneker AT gmail.com> wrote:
> 
> Hi Lorenzo,
> 
> Can you send the actual example (or a simplification) that demonstrates the 
> lack of preregularity.
> 
> Steven Eker
> 
> 
> On Thu, Nov 16, 2023 at 6:43 AM Lorenzo Capra <capra AT di.unimi.it> wrote:
> Dear Maude users
> I have a simple question about preregularity of terms built using
> nested generic modules.
> For example, I am using the built-in LIST{X} together with my own
> BAG{X} module (which defines multisets):
> a Bag{String} term, e.g., is defined as a formal sum
> 1 . "a" + 2 . "b"
> I need to use also multisets of lists, i.e., terms of sort
> Bag{List{String}} like
> 1 . "a" "b" + 2 . "c"
> but I guess that in this case some terms fail to be preregular:
> 
> 1 . "a"
> seemingly doesn't have a least sort, because (due to the suborting
> String < List{String}) it may be considered both of sort
> Bag{String}
> and of sort
> Bag{List{String}}
> (covariance doesn'hold, I believe, but I'm not sure 100%).
> 
> Am I missing something?
> In the case I'm not, may you kindly suggest to me how to manage this?
> Using another LIST implementation where X$Elt is not a subsort of List{X}?
> 
> Thank you very much
> Lorenzo Capra