Maude-help mailing list

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

Hi Lorenzo,

I don't think there is a direct way to get all the matches, but you can 
either (1) traverse the search graph a find all matches with metaMatch, or 
1-step applications of metaSrewrite or metaSearch, or (2) build the search 
graph yourself, also at the metalevel. 

Cheers,

Francisco Durán

> On 28 Feb 2024, at 12:03, Lorenzo Capra <capra AT di.unimi.it> wrote:
> 
> Dears
> thank you, your answer perfectly matches my question
> 
> (unfortunately, for a glitch in our mail server, it  was marked as spam)
> 
> I have another one.
> Let me anticipate it, if you think it could be of interest to others I
> will post it also on the mailing list.
> 
> In the labelled transition system associated to a term t (that printed
> by the command
> Maude> show search graph . )
> state-transitions are inscribed by the rewrite rule(s) causing them,
> according to the fact (i suppose) that they represent equivalence
> classes of rewrite proofs
> 
> Is it possible to see (print) all the matches (variable substitutions)
> corresponding to a rewrite?
> 
> I was only able to get it for a single rewrite step using the print
> attribute for rules.
> 
> (We are trying to derive a lumped Markov Chain from the transition systems.)
> 
> Thank you in advance
> 
> Best regards
> 
> Lorenzo
> 
> 
> On Sat, Nov 18, 2023 at 10:52 AM Francisco Durán <fdm AT uma.es> wrote:
>> 
>> 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
>>