Maude-help mailing list

[Francisco Durán <narudocap AT gmail.com>]

Hi Neil,

I don't have an answer for your problem, but I'll try to bring some light. 

First, I don't really see why you believe Maude can help you in your problem. 
It is possible that you didn't tell us the entire story, and that once you 
have your term sets you plan to do something Maude can do better than other 
tools. If you are looking for a language that can outperform Python you are 
possibly in the wrong place. If you are looking for something where you can 
express your problem at a higher level of abstraction, and possibly do some 
analysis on it, then Maude might be a good choice. 

Having a set of terms like the one you are creating looks like a simple idea, 
but possibly it is what you need. Depending on what you want to do with these 
sets it might be a good or a bad choice. Manipulating big terms is expensive, 
and rewriting modulo may be a bottleneck. Given too much freedom may make 
matching more expensive, even if the code looks simpler. Conditions are also 
typically expensive, if you can avoid them you'll notice the results, but it 
isnot always easy, or possible. 

The code you show in your email is related to the selection of terms. Given a 
set of terms you want to select some of them, turning a term into a validterm 
or an invalidterm depending on whether they satisfy a given condition. I 
don't think rules are the right way to do that. Actually what you do looks 
more like membership axioms to me. 

Given subterms ValidTerm InvalidTerm < Term, you could, for example, write 
your rule W-rule-1 like 
mb term (Oop (a, b), Hop (c, d), Wop (bd, ac)) : ValidTerm 
        if (bd == (b + d)) and (ac == (a + c)) .
which basically brings a term of type Term down into a subtype ValidTerm if 
it satisfy some condition. This is not necessarily more efficient, I couldn't 
tell at least, but it better represents what you intend to do. 

Either using rules or memberships, it seems that what you do is to generate a 
bunch of terms and then discard the invalid ones. Wouldn't it make more sense 
just not to generate invalid ones? I suppose it is not possible. 

I'm sure this doesn't help much, I hope that it at least allows you to help 
us to understand your problem. 

Best,

Francisco Durán


> On 7 Mar 2022, at 21:53, Neil George Raymond 
> <neil.raymond AT uwaterloo.ca>
>  wrote:
> 
> Hello all,
>  
> I haven’t used mailing lists before so please forgive any faux pas.
> I’m a researcher in computational chemistry looking to use Maude to help 
> with generating and reducing a large number of summation terms.
> So far my coworker and I have been able to read through and digest the 
> Manual up to the end of chapter 6.
> I have 10+ years of coding but I’m finding that some of my  traditional 
> tools/design mindset are not easily transferable to Maude so I would 
> greatly appreciate any help! 😊
>  
> Background of the problem (feel free to skip)
> I have derivatives which are calculated as a sum over terms.
> dy/dx = a + b + c + d … etc
> Many of these terms have zero contribution to the sum due to 
> off-diagonality in specific dimensions and/or other mathematical 
> constraints.
> Manually deriving all of these terms by hand is impossible for anything but 
> trivial systems.
> So they need to be generated algorithmically; which I have accomplished 
> with a package developed in Python for the series truncated to at most 
> 6thorder (and for a specific ansatz).
> However it would be very useful to have a more general approach using Maude.
> Ideally it would allow one to change the first principles ansatz and still 
> correctly derive all of the non zero summation terms.
> To change the ansatz (in python) requires rewriting large components of the 
> package, making it an impractical approach.
>  
> My questions
> 1 – How best to generate/represent truncated infinite series?
> 2 – What are some possible ways to represent my terms (better and/or 
> different)?
> 3 – How to validate / apply rules to each term (possibly in an efficient 
> manner)?
>  
> I have three infinite series (but we’ll ignore one of them for simplicity 
> for now)
> H = h_0^0 + h_1^0 + h_0^1 + h_1^1 + h_2^0 + ….
>                 Z = z_0^0 + z_1^0 + z_0^1 + z_1^1 + z_2^0 + ….
>  
> All terms are formed as the product of these infinite series, such as:
> h_0^0 * z_1^0
> or 
> h_0^1 * z_1^0
> or
>                 h_1^8 * z_3^4
>  
> However only certain ones have non zero contribution.
> I have a set of rules that a term must obey, otherwise it has zero 
> contribution.
> It seems like a problem that fits very well with what Maude can achieve.
>  
> Examples of some exploration/testing I have tried
>  
> I was exploring sets and the `owise` attribute as a means of collating and 
> keeping track of the terms.
> Below I provide a short excerpt, where the entire file is attached as 
> `exploring_sets.txt`
> ____________________________________
> *** define the set of valid terms
> sort ValidSet .
> subsort ValidTerm < ValidSet .
> op empty : -> ValidSet [ctor].
> op _;_ : ValidSet ValidSet -> ValidSet [ctor assoc comm id: empty] .
>  
> *** define membership in the set of valid terms
> op _in_ : Term ValidSet -> Bool .
> var SetOfValidTerms : ValidSet .
>  
> eq T in T ; SetOfValidTerms = true .
> eq T in SetOfValidTerms = false [owise] .
> ____________________________________
>  
> For representation I’m trying to adapt my currently working python code.
> A simplistic explanation is that it uses lists of tuples representing the 
> operators, for example
> h_0^1 * z_1^0
> would be [(0, 1), (1, 0)] 
> and you could see how rules (such as, the subscripts can never be larger 
> than 3) can applied to all terms for any numbers [(#, #), (#, #)]
>  
>  
> I also explored conditional rules (although I don’t think this approach is 
> great)
> ____________________________________
> crl [W-rule-1] :
>     term (Oop (a, b), Hop (c, d), Wop (bd, ac))
>         => validterm (Oop (a, b), Hop (c, d), Wop (b + d, a + c))
>         if (bd == (b + d)) and (ac == (a + c)) .
> ____________________________________
>  
> ____________________________________
> crl [W-rule-2] :
>     term (Oop (a, b), Hop (c, d), Wop (bd, ac))
>         => invalidterm (Oop (a, b), Hop (c, d), empty)
>         if (bd =/= (b + d)) or (ac =/= (a + c)) .
> ____________________________________
>  
>  
> In terms of generating series terms I tried at first to make conditional 
> rules that would ‘pull-off’ a super or sub script.
> I don’t really see this working, but it is unclear to me what direction to 
> go from here. Maybe there are other components of Maude that would better 
> fit this objective?
>  
> The idea is to take o^3_1 and produce o^2_1 * o^1_0.
> In this way I could start with maximal terms and generate smaller terms and 
> then only keep the unique ones.
> ____________________________________
> crl [a_+minus-_1]:
>     Wop(a, b)
>         => Wop(a - 1, b) Wop(1, 0)
>         if a > 1 or (a > 0 and b > 0) .
> ____________________________________
>  
>  
> ____________________________________
> crl [b_minus_1]:
>     Wop(a, b)
>         => Wop(a, b - 1) Wop(0, 1)
>         if b > 1 or (a > 0 and b > 0).
> ____________________________________
>  
>  
>  
>  
> The ultimate goal would be to only provide integers as input, each one 
> indicating the order of truncation for the infinite series and to output 
> all valid terms (terms that satisfy some number of conditions).
>  
>  
>  
> Considerations
> I imagine in the same way that vectorizing loops improves performance in 
> certain languages, the way I design my Maude script/modules will have 
> performance impacts.
> I just don’t have the experience with Maude to reason about pros/cons of 
> different possible approaches.
> Are there any rules of thumb about the scaling of conditional rules, 
> equations, maximal number of variables or such things?
>  
>  
>  
> Regards,
>  
> Neil
>  
> <exploring_sets.txt>