First stab at formalism (benny)

[ngraymon]

1. Practice writing out the terms for the $\Omega^0_0$ case (given the 4 numbers) and make sure the rules are clear
2. start to compile some sources
3. play around with representations

[ngraymon]

In GitLab by @bjb2chen on Jun 28, 2021, 12:45

1. I have written tried writing out the terms for $\Omega^0_0$ case. Though, I do not fully understand Rule 2 currently. Looking at the examples for 1.1 Linear Equations, is $\hat{i}$ just always supposed to contain superscript z whereas $\hat{i}^\dagger$ always have subscript z?

2. Some sources I found interesting:

https://en.wikipedia.org/wiki/Boolean_algebra (helps beginners to logic systems like me understand the symbols used in formal languages)

https://www.youtube.com/watch?v=sa-TUpSx1JA&ab_channel=CoreySchafer (this was a good tutorial demonstrating how to make matching systems for regular expressions)

https://en.wikipedia.org/wiki/Nondeterministic_finite_automaton (cool article on a concept I think we might be interested in investigating)

3. No progress on this yet.

[ngraymon]

[ngraymon]

I'm pretty sure we need a TRS https://www.youtube.com/watch?v=WkPngxPUVL8

[ngraymon]

This looks really good (and dense sorry, lol) https://www.youtube.com/watch?v=b2Px7cu2a68

[ngraymon]

Good source of videos https://www.youtube.com/results?search_query=Abstract+rewriting+system

[ngraymon]

Experiment with $\Omega^0_0$,$\Omega^0_1$,$\Omega^1_0$ and try to come up with simple English rules for how to "rewrite" a term

Example: if we start with $\hat{\Omega}\hat{H}\hat{W}$ we use the rules:

1. $\hat{\Omega} \rightarrow\Omega^0_0$
2. $\hat{\Omega} \rightarrow\Omega^1_0$
3. $\hat{\Omega} \rightarrow\Omega^0_1$

to give us

1. $\Omega^0_0\hat{H}\hat{W}$
2. $\Omega^1_0\hat{H}\hat{W}$
3. $\Omega^0_1\hat{H}\hat{W}$

then how do we write a rule for $\hat{H}$ so that we only rewrite our 'generic' term into 'valid' terms and not 'invalid' terms

maybe the rule has to include W?

1. $\Omega^1_0\hat{H}\hat{W} \rightarrow\Omega^1_0 h^0_0 t^0_1$

or maybe its only the h, and the W has the weird parts?

1. $\hat{H} \rightarrow h^0_0$

2. $\hat{H} \rightarrow h^1_0$

3. $\hat{H} \rightarrow h^0_1$

4. $\Omega^1_0\hat{H}\hat{W} \rightarrow \Omega^1_0 h^0_0 \hat{W}$

5. $\Omega^1_0\hat{H}\hat{W} \rightarrow \Omega^1_0 h^1_0 \hat{W}$

6. $\Omega^1_0\hat{H}\hat{W} \rightarrow \Omega^1_0 h^0_1 \hat{W}$

Then write rules for W? does W know about the other guys? maybe W has rules for disseminating itself?

• $\Omega^m_n h^l_p \hat{W} \rightarrow \Omega^m_n h^l_p W^{n+p}_{m+l}$

(maybe omega removal rule? but we might need it to properly assign labels?....although that information would be encoded in the variables $m,n$....so we might be fine?)

• $\Omega^m_n h^l_p \hat{W} \rightarrow h^l_p W^{n+p}_{m+l}$

disseminate?

• $W^{a}_{b} \rightarrow W^{a-x}_{b}t^{x}$
• $W^{a}_{b} \rightarrow W^{a}_{b-y}t_{y}$
• $W^{a}_{b} \rightarrow W^{a-x}_{b-y}t^{x}_{y}$
• $W^{0}_{0} \rightarrow \epsilon$

[ngraymon]

In GitLab by @bjb2chen on Jul 5, 2021, 11:48

Make a Word document on simple interpretations of concepts found in videos.

[ngraymon]

Maybe the way to restrict W and what values H can take is by modifying this rewrite rule?

• $\Omega^m_n h^l_p \hat{W} \rightarrow h^l_p W^{n+p}_{m+l} \quad|\quad (n+p \leq \#) AND (m+l \leq \#)$
• $\Omega^m_n h^l_p \hat{W} \rightarrow \epsilon \quad|\quad (n+p > \#) OR (m+l > \#)$

or maybe we need a specific symbol for an invalid term??? .... this is unclear?

• $\Omega^m_n h^l_p \hat{W} \rightarrow \emptyset \quad|\quad (n+p > \#) OR (m+l > \#)$

or maybe if we are making A + B + C + D + E + F.... like

$\Omega^0_0 h^l_p \hat{W} + \Omega^1_0 h^l_p \hat{W} + \Omega^0_1 h^l_p \hat{W}$ then when we do $\Omega^m_n h^l_p \hat{W} \rightarrow \epsilon$

for example $\Omega^0_0 h^4_0 \hat{W} \rightarrow \epsilon$ when $W$ is rank 2

we end up with $\epsilon +$ or $+ \epsilon +$ or $+ \epsilon$ so we could add the rules

• $\epsilon + \rightarrow +$
• $+ \epsilon \rightarrow +$
• $+ \quad + \rightarrow +$

so we also probably need rules for the empty set (which removes extraneous 'plusses' on the left and right side of the sums of the terms, if all terms are epsilons then the sum will just be a super long string of plusses, which will become 1 singluar plus, which will plus two empty sets and then simply be the empty set?

• $\emptyset + \rightarrow \emptyset$
• $+ \emptyset \rightarrow \emptyset$
• $\emptyset + \emptyset \rightarrow \emptyset$
• $\emptyset \emptyset \rightarrow \emptyset$

[ngraymon]

Here on the wolfram website there is a source Term Rewriting and All That which there is a single copy of in the library but also we can search for similar subject matter

heres one from 2012:

which says its available at the davis center!

[ngraymon]

Okay so i found some conferences on the issue, this could be useful: Rewriting Techniques and Applications (RTA) WRLA

[ngraymon]

In GitLab by @bjb2chen on Jul 21, 2021, 12:17

Some experimenting with $\Omega^0_0$ case:

experimenting_rewriting.docx

[ngraymon]

@bjb2chen try implementing the first three omega rules in maude https://en.wikipedia.org/wiki/Maude_system copying the syntax in example 3

[ngraymon]

We learned some stuff today, playing around with maude. maude_omega_rules

[ngraymon]

run_maude.sh

[ngraymon]

1. try to make a basic implementation of going from a triplet of numbers to any permutation of Ooop, Hop, Wop that is valid. kind of like this
2. play around with the rl's and the crl's

[ngraymon]

In GitLab by @bjb2chen on Aug 10, 2021, 08:24

The Maude manual was noted to be a good reference source: http://maude.cs.illinois.edu/w/images/6/62/Maude-3.1-manual.pdf

[ngraymon]

I did a bit more playing around today; Section 4.4 (pg 53) seems very useful to understand. For example:

• pg 54 they talk about sequences/lists
• pg 55 they talk about Constructors; turns out if you don't have the [ctor] then you can have operators that don't 'appear'..... I think... ?
• pg 56 they talk about associativity and other operator decorators which we definitely will need pg 58/59 talks about polymorphic operators and gives an example of a list of multiple types!!

[ngraymon]

Okay .... its kind of facepalm how simple it is to do lists....X_X.

sort WList .
subsort Empty < W < WList .
op __ : WList WList -> WList [assoc] .

and thats it... then change rules to

crl [a_+minus-_1]:
    Wop(a, b)
        => Wop(a - 1, b) Wop(1, 0)
        if a > 0 .

and it just works:

Maude> load maude_omega_rules.maude
Maude> rew [1] Wop(4,0) .
rewrite [1] in RESIDUALS : Wop(4, 0) .
rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
result WList: Wop(3, 0) Wop(1, 0)

Maude> rew [2] Wop(4,0) .
rewrite [2] in RESIDUALS : Wop(4, 0) .
rewrites: 8 in 0ms cpu (0ms real) (~ rewrites/second)
result WList: Wop(2, 0) Wop(1, 0) Wop(1, 0)

Maude> rew [3] Wop(4,0) .
rewrite [3] in RESIDUALS : Wop(4, 0) .
rewrites: 13 in 0ms cpu (0ms real) (~ rewrites/second)
result WList: Wop(1, 0) Wop(1, 0) Wop(1, 0) Wop(1, 0)

[ngraymon]

In GitLab by @bjb2chen on Sep 11, 2021, 16:46

Fascinating stuff, pretty cool and elegant to build lists like this!

[ngraymon]

this might be interesting https://www.sciencedirect.com/science/article/abs/pii/S2352220818301688?via%3Dihub

[ngraymon]

BMgrt_2003.pdf

Maude-jlamp.pdf

found two recent preprints from 2020 http://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_Logic