Maude-help mailing list

[Elliott Goldstein <eg9699 AT bard.edu>]

My first question would be about the frozen attribute. Currently I am trying to implement an operator m() that returns the "measure" of some term. The measure is calculated by deriving the value (1 + m(left hand subterm) + m(right hand subterm)) for any term. I was able to implement all this, but currently my rewrite system is unable to handle cases in which my terms can act as redexes. For instance, one of my rewrite rules specifies idempotency, so, working in the domain of the binary operators {* and /}, X*X=X, and X/X=X, etc. However, if I attempt to apply my m() operator to a term that can act as a redex, it evaluates the rewritten form of the redex, not the original, non-rewritten form, even if I include the [frozen] attribute. I am also sure to do all this in a system module and not a functional module, but it still rewrites my given term before applying m() to it, although the frozen attribute is supposed to avoid this.

My current system module set-up:

mod PRUNE is 

 op f : Term -> Term [frozen] .
op m _ : Int -> Int [frozen] .
vars X Y Z : Int .
eq m(X:Int) = 0 .
eq m(X:Term) = (1 + mult3(m(lhs(X:Term)))) + (m(rhs(X:Term))) .
eq m(C:TermList) = (1 + mult3(m(lhs(C:TermList)))) + (m(rhs(C:TermList))) .

endm

(My fmod sets the the rewrite rules and axioms as equations):

 eq X * X = X  [variant] .
eq X / X = X  [variant] .
eq ( X * Y ) / Y = X  [variant] .
eq ( X / Y ) * Y = X  [variant] .
eq X / ( Y / Z ) = ( ( X * Z ) / Y ) / Z  [variant] .
eq X * ( Y / Z ) = ( ( X *  Z ) * Y ) / Z  [variant] .
eq X * ( Y * Z ) = ( ( X / Z ) * Y ) * Z  [variant] .
eq X / ( Y * Z ) = ( ( X / Z ) / Y ) * Z  [variant] .
eq X / ( Y / Z ) = ( ( X * Z ) / Y ) / Z  [variant] .

(It should be noted for clarity that Int is a subsort of Term, and Term a subsort of TermList). This is causing quite an issue in my code, and I wasn't sure what the issue was, as I am under the impression the frozen operator should not be rewriting any of the arguments to m, although it will evaluate m(X * X) to be m(X), which returns a value of 0, rather than 1, since m(X*X) returns 1 + 0 + 0.

Secondly, I was curious about Maude's variant generation strategies. Something odd I have noticed that I may have missed in the manual is that, originally, before implementing the sorts Int, Term, and TermList, nearly all of my get variant commands on a given term generated infinite variants. However, after adding the sorts and subsorts Int < Term <TermList (For instance, Int is simply a single variable, a Term is two variables separated by an operator, and a TermList is two terms separated by an operator) my variant generation become non-infinite. I assume this is because in Maude sorts cannot rewrite to higher sorts, I can include an example of the way the variant generation varied in a future email, but my intuition would tell me the change was caused by the inclusion of the subsorts. If this is the case, is there any way to override this feature of Maude to allow sorts to be rewritten to higher sorts? My senior project is focused on attempting to implement some kind of semi-decideable procedure for determining if my rewrite system has the finite variant property so variant generation within maude is something I'd really need to understand deeply before going further.

Again, thanks so much for the help, Elliott