Maude-help mailing list

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

Hi Raghu,

A few comments on your code:

- Maude doesn't initialize attribute values. You should write

rew < O : R | a : 0, b : 0, c : 0 > .

- The rewriting of this term will, however, not terminate. This doesn't 
necessarily execute as you may expect. 

Maude> rew [100] < O : R | a : 0, b : 0, c : 0 > .
rewrite [100] in LOCALS : < O : R | a : 0, b : 0, c : 0 > .
rewrites: 364 in 0ms cpu (0ms real) (692015 rewrites/second)
result Object: < O : R | a : 1, b : 7, c : 12 >

Any of the rules can be repeatedly applied. An option might be to use some 
kind of flag. For example, since b and c are the "calculated" variables, you 
could use flags indicating whether they have already been re-calculated or 
not. This will required to keep track of dependencies, which may be 
complciated. 

- I'd write the calculation of b and c to happen in equations, then making 
sure that they have their values calculated before they are required in 
rules. Since this mechanism is confluent and terminating, you can write them 
as eqs. 

omod LOCALS is
pr NAT .
class R | a : Nat, b : Nat, bf : Bool, c : Nat, cf : Bool .
var X Y Z U : Nat .
var O : Oid .

op f : Nat Nat Nat Nat -> Nat .
eq f(X,Y,Z,U) = X + Y + Z + U .
rl < O : R | a : X, b : Y, c : Z > => < O : R | a : s X, bf : false, cf : 
false > [print "a: " X ", b: " Y ", c: " Z] .
eq < O : R | a : X, bf : false > = < O : R | b : f(2,X,3,X), bf : true > .
eq < O : R | a : X, b : Y, bf : true, cf : false > = < O : R | c : 
f(Y,2,X,2), cf : true > .
endom

Note the increment of the a attribute in the rule, and the reset of the 
dependency flags. I've also added a print attribute to witness how things 
work. 

Maude> set print attribute on .
Maude> rew [10] < O : R | a : 0, b : 0, bf : false, c : 0, cf : false > .
rewrite [10] in LOCALS : < O : R | a : 0, b : 0, bf : false, c : 0, cf : 
false > .
a: 0, b: 5, c: 9
a: 1, b: 7, c: 12
a: 2, b: 9, c: 15
a: 3, b: 11, c: 18
a: 4, b: 13, c: 21
a: 5, b: 15, c: 24
a: 6, b: 17, c: 27
a: 7, b: 19, c: 30
a: 8, b: 21, c: 33
a: 9, b: 23, c: 36
rewrites: 120 in 0ms cpu (0ms real) (625000 rewrites/second)
result Object: < O : R | a : 10, b : 25, bf : true, c : 39, cf : true >

Best,

Francisco


> On 4 Dec 2023, at 07:51, Raghu Ranganathan <rraghu.11502 AT gmail.com> wrote:
> 
> I would like to be able to assign local variables (or something similar to 
> a local variable) to reuse intermediate values instead of creating 
> potentially 3-4 ops for a single purpose.
> 
> Taking a pseudocode example:
> 
> a=1
> b=F(2,a,3,a)
> c=F(b,2,a,2)
> F(x,y,z,u)=x+y+z+u
> 
> my attempt at translating this to an object module is:
> omod LOCALS is
>   pr NAT .
>   class R | a : Nat, b : Nat, c : Nat .
>   var X Y Z U : Nat .
>   var O : Oid .
>   var Atts : AttributeSet .
> 
>   op f : Nat Nat Nat Nat -> Nat .
>   eq f(X,Y,Z,U) = X + Y + Z + U .
>   
>   rl < O : R | Atts > => < O : R | a : 1 , Atts > .
>   rl < O : R | a : X , Atts > => < O : R | b : f(2,X,3,X), Atts > .
>   rl < O : R | a : X, b : Y, Atts > => < O : R | c : f(Y,2,X,2), Atts > .
> endom
> 
> This strategy doesn't seem to work when i try to rewrite it:
> 
> Maude> rew < O : R | > .
> rewrite in LOCALS : < O : R | none > .
> rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
> result Object: < O : R | none >
> 
> But even if it worked, this is equally as verbose if not more verbose than 
> simply creating new ops. I am wondering if there is a simpler way to store 
> values for later use, or a better way to reuse state in an operator.