Maude-help mailing list

[Steven Eker <steveneker AT gmail.com>]

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