Maude-help mailing list

[Neil George Raymond <neil.raymond AT uwaterloo.ca>]

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 6^th order (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

 

mod RESIDUALS is

*** including BOOLEAN .  because we want to use the `or` operator
protecting BOOL .
protecting NAT .
protecting INT .

*** define the types of terms
sorts ValidTerm InvalidTerm Term .
subsorts ValidTerm InvalidTerm < Term .

*** a variable for any term
var T : Term .
var VT : ValidTerm .
var IVT : InvalidTerm .

*** 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] .


*** define the set of invalid terms
sort InvalidSet .
subsort InvalidTerm < InvalidSet .
op empty : -> InvalidSet [ctor].
op _;_ : InvalidSet InvalidSet -> InvalidSet [ctor assoc comm id: empty] .

*** define membership in the set of Invalid terms
op _in_ : Term InvalidSet -> Bool .
var SetOfInvalidTerms : InvalidSet .

eq T in T ; SetOfInvalidTerms = true .
eq T in SetOfInvalidTerms = false [owise] .
 xmatch term(O^0_0, H^0_0, W^0_0) <=? ValidSet

*** now we try to define the set of valid terms?
sort operator .
sorts O H W Empty .
subsorts Empty < O H W < operator .
*** spacer
vars O^0_0 O^1_0 O^0_1 O^1_1 O^2_0 O^0_2 : O .
vars H^0_0 H^1_0 H^0_1 H^1_1 H^2_0 H^0_2 : H .
vars W^0_0 W^1_0 W^0_1 W^1_1 W^2_0 W^0_2 : W .
*** spacer
op term : O H W -> [Term] [ctor] .
*** op validterm : O H W -> ValidTerm [ctor] .
*** op invalidterm : O H W -> InvalidTerm [ctor] .

*** var VT : ValidTerm .
mb term(O^0_0, H^0_0, W^0_0) : ValidTerm .

*** eq VT in SetOfValidTerms = true .
*** rl [zerozerozero] : term(O^0_0, H^0_0, W^0_0) => ValidTerm .



*** define W operator lists
sort WList .
subsort Empty < W < WList .
op __ : WList WList -> WList [assoc] .

*** op empty : -> Empty .




***(
    explore both red and rew
    sort rank .
    op truncate : Nat Nat Nat -> rank [ctor] .
)



*** op Oop : Nat Nat -> O [ctor] .  *** ctor just means constructor
*** op Hop : Nat Nat -> H [ctor] .  *** I do not know if the underscores in 
the name causes issues or not, see the _+_ infix operator in Example 2
*** op Wop : Nat Nat -> W [ctor] .



vars a b c d : Nat .
vars bd ac : Nat .

--- eq term (Oop (a, b), Hop (c, d), Wop (bd, ac)) = term (O, H, W) .
*** rl [abc] : truncate (a, b, c) =>

*** rl [Oop-rule-1] : Oop (0, 0) => Oop (0, 0) .
*** rl [Oop-rule-2] : Oop (a, b) => Oop (1, 0) .
*** rl [Oop-rule-3] : Oop (a, b) => Oop (0, 1) .
*** rl [h-rule-1]   : Hop (c, d) => Hop (0, 0) .
*** rl [h-rule-2]   : Hop (c, d) => Hop (1, 0) .
*** rl [h-rule-3]   : Hop (c, d) => Hop (0, 1) .


*** rl [compact_list1] : Wops(Wops(anyW1, anyW2), anyW3) => Wops(anyW1, 
anyW2, anyW3).
*** rl [compact_list2] : Wops(anyW1, Wops(anyW2, anyW3)) => Wops(anyW1, 
anyW2, anyW3).
*** rl [compact_list3] : Wops(Wops(anyW1, anyW2), anyW3, anyW4) => 
Wops(anyW1, anyW2, anyW3, anyW4).
*** rl [compact_list4] : Wops(anyW1, Wops(anyW2, anyW3), anyW4) => 
Wops(anyW1, anyW2, anyW3, anyW4).
*** rl [compact_list5] : Wops(anyW1, anyW2, Wops(anyW3, anyW4)) => 
Wops(anyW1, anyW2, anyW3, anyW4).

***(

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).


crl [empty]:
    Wop(a, b)
        => empty
        if a == 0 or b == 0 .


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)) .
)

***(
    idk how to do 'or' Boolean function,
    from a cursory look at the references
    http://maude.cs.illinois.edu/w/images/6/62/Maude-3.1-manual.pdf
    and
    http://maude.cs.uiuc.edu/papers/pdf/maudeSlides.pdf
    I think _or_ operator needs to be implemented?? don't think just doing \/ 
is correct
)

endm