Statistics of higher-order equations

Stream: Equational

[Bruno Le Floch]

Can we understand the statistics of laws with a large number of ⋄? For instance 30% of the 4694 laws are overdetermined (equivalent to Equation 2). How does that percentage change as we increase the order? More generally, for a given equation, what are the asymptotics of the number of equations of order n that are equivalent to that equation? Are there any equation equivalent to Equation 3? If typical equations are equivalent to equations of lower order then it is conceivable that we can define an asymptotic probability measure on the set of equations that would give a sense in which a particular equation is typical or not.

[Bruno Le Floch]

Relatedly, for a given strict implication A⇒B, is there always an intermediate equation C of higher order such that A⇒C⇒B are strict implications? For a trivial example, 2⇒1, but taking into account laws with one operation refines this implication into a consequence of two implications such as 2⇒3⇒1. A less trivial example is that 2⇒5 (namely x=y implies x=y⋄x) cannot be factorized into 2⇒eq⇒5 for any eq up to four operations; does that continue to arbitrary order?

[Alex Meiburg]

As for your second point, the answer is known to be negative. There are no laws that are strictly between 2 and 46.

Terence Tao said:

All non-trivial constant magmas satisfy exactly the same set of laws (those laws with at least one application of the operation on both sides, as well as the trivial law x=x), so the answer is "no".

A similar argument shows that 2->4 and 2->5 are similarly irreducible.

[Vlad Tsyrklevich]

Bruno Le Floch said:

How does that percentage change as we increase the order?

Incidentally, I am looking at some things at order 5 at the moment and the percentage is close: ~19392 / 57882 = 33.5% where as at order <= 4 it is 1496/4694.0 = 31.9%

At order 5 I only have stats for implications to Equation 2.

[Vlad Tsyrklevich]

The per-order break down of equations implying Equation 2 is:
Order 0: 1/2 = 50%
Order 1: 2/5 = 40%
Order 2: 12/49 = 24.5%
Order 3: 119/364 = 32.7%
Order 4: 1362/4284 = 31.7%
And then the approximate order 5 number of 31.9%.

There are no Austin laws of order <= 4 so those numbers are the same for the finite and 'general' (is there a better word?) graphs, order 5 numbers would vary slightly upwards.

[Vlad Tsyrklevich]

Did we ever nail down how to compute the number of equations of a given order? The known Equation 2 equivalence class has a pretty clear structure (e.g. LHS of 'x', no outer most 'x' term in the RHS), so I imagine it should not be too hard to compute that bound.

[Alex Meiburg]

Alex Meiburg said:

As for your second point, the answer is known to be negative. There are no laws that are strictly between 2 and 46.

A similar argument shows that 2->4 and 2->5 are similarly irreducible.

... and with some more work, one can show this holds for equation 168 as well. One can show that all nontrivial laws that imply 168 must take the form x = (_*x)*(x*_) . And then 168 implies that back.

[Bruno Le Floch]

Vlad Tsyrklevich said:

Did we ever nail down how to compute the number of equations of a given order? The known Equation 2 equivalence class has a pretty clear structure (e.g. LHS of 'x', no outer most 'x' term in the RHS), so I imagine it should not be too hard to compute that bound.

Yes, see https://oeis.org/A376640 and related sequences. What you say will give an upper bound on the fraction of equations that imply 2. If I understand correctly the asymptotics, the simple lower bound consisting of all equations of the form x=(expr in y,z,... without x) only reaches at most a fraction like 1/n of the full set of equations. So the bounds are not very tight yet.

[Notification Bot]

8 messages were moved here from #Equational > Future directions by Bruno Le Floch.

[Vlad Tsyrklevich]

I meant something else but actually I see now that it is wrong as it would capture the Austin law 28770.

[Bruno Le Floch]

(I moved messages to avoid cluttering the generic "Future directions" topic. Hopefully it's ok etiquette.)
The number of equations with n operations goes mostly like Catalan(n+1)Bell(n+2)/2, where Catalan counts the trees and Bell the rhyme schemes. There are asymptotically tiny corrections to this when n is even. The $n\to+\infty$ asymptotics is $\text{Catalan}(n) \simeq 4^n n^{-3/2} \pi^{-1/2}$ and $\text{Bell}(n)=\Bigl(\frac{n}{e\log n}(1+o(1))\Bigr)^n$.

The equations that imply 2 (hence are equivalent to it since 2 implies everything) must have LHS of x. There are at most Catalan(n)Bell(n+2) of them, which is a proportion Catalan(n)/(Catalan(n+1)/2) of the total that asymptotes to 1/2. So it is not surprising that the percentages @Vlad Tsyrklevich got are <50%. What is not so clear is why most laws of the form x=... end up being overdetermined.

@Alex Meiburg Thanks. So the infinite Hasse diagram of equations of all orders has several edges (2⇒4,2⇒5,2⇒46,2⇒168, I would guess 5⇒19 too) known to be irreducible, and at least one equivalence class that is fully described (the one of 168). That's pretty nice. There are also semi-infinite chains of implications: equation $y=(L_x)^{2^n}y$ for some n implies the equation for larger n, and all the implications are strict as exemplified by the groups $\mathbb{Z}/2^n\mathbb{Z}$. It's not immediately clear to me whether there can be infinite chains in the other direction.

[Alex Meiburg]

Oh, the equivalence class of 168 isn't known, it's not obvious which "blanks" can go in and are tight enough.

Like x = ((z*w)*x)*(x*y) has a free value on the left and right ends, since z*w can take any value, so it's equivalent. x = (x*x)*(x*y) is not as flexible and it's weaker.

It's not immediately obvious whether something like

x = (    (((z*w)*x)*z)   *x)*(x*      ((y*z)*(w*x))   )

has enough degrees of freedom in picking w/y/z to get all of 168.

That's definitely an interesting question though, maybe a tractable but non-obvious one

[Harald Husum]

Alex Meiburg said:

As for your second point, the answer is known to be negative. There are no laws that are strictly between 2 and 46.

Terence Tao said:

All non-trivial constant magmas satisfy exactly the same set of laws (those laws with at least one application of the operation on both sides, as well as the trivial law x=x), so the answer is "no".

A similar argument shows that 2->4 and 2->5 are similarly irreducible.

As I mention in that thread, determining which implications are irreducible seems like an interesting question. Great to see you guys exploring that question!

[Bruno Le Floch]

Alex Meiburg said:

Oh, the equivalence class of 168 isn't known, it's not obvious which "blanks" can go in and are tight enough.

You're right. So the best we get from that is an upper bound on the size of the equivalence class. We also have a rather weak lower bound: equations of the form x = (_*x)*(x*_) in which the two blanks have disjoint sets of variables.

Getting tighter bounds on that equivalence class, or on the one of equation 2, seems tough.

One doable thing is to count equations implied by equation 4 x = x*y. These are simply all equations whose first letter on the lhs and rhs are the same, regardless of the tree. Asymptotically it will be a fraction $\text{Bell}(n+1)/\text{Bell}(n+2) \simeq (e \log n)/ n$ of the whole set of equations.

[Alex Meiburg]

Along similar lines, it's easy to count how many are implied by the constant law: they're everything not of the form x=_.

[Bruno Le Floch]

So that's asymptotically 1/2 of the laws if I'm not mistaken.

[Bruno Le Floch]

In case someone wants to test out some tools on higher-order equations, here is a (uniform) pseudo-random selection of equations with 9 operands:

Equation 4082587915: x ◇ y = (x ◇ (z ◇ (w ◇ (y ◇ u)))) ◇ (u ◇ (u ◇ (v ◇ r)))
Equation 3293773466: x = ((((y ◇ (z ◇ (w ◇ z))) ◇ (y ◇ y)) ◇ u) ◇ (x ◇ v)) ◇ v
Equation 2234912675: x = ((y ◇ (y ◇ z)) ◇ (y ◇ ((w ◇ x) ◇ z))) ◇ ((y ◇ y) ◇ z)
Equation 4353755559: x ◇ y = (z ◇ (((w ◇ (u ◇ (x ◇ z))) ◇ (x ◇ y)) ◇ u)) ◇ u
Equation 2471839353: x = (((y ◇ z) ◇ y) ◇ (((x ◇ (x ◇ y)) ◇ w) ◇ z)) ◇ (y ◇ y)
Equation 2644325661: x = (y ◇ (z ◇ (w ◇ (((x ◇ y) ◇ (u ◇ z)) ◇ (u ◇ y))))) ◇ v
Equation 2671366418: x = (y ◇ (z ◇ (((y ◇ z) ◇ w) ◇ (((y ◇ u) ◇ z) ◇ x)))) ◇ z
Equation 2668226843: x = (y ◇ (z ◇ ((w ◇ (u ◇ u)) ◇ (((x ◇ z) ◇ w) ◇ w)))) ◇ z
Equation 4587721794: x ◇ (y ◇ z) = z ◇ (w ◇ ((z ◇ (x ◇ ((x ◇ u) ◇ y))) ◇ w))
Equation 1272981597: x = (y ◇ z) ◇ (w ◇ (y ◇ (u ◇ ((w ◇ v) ◇ ((r ◇ s) ◇ y)))))
Equation 3348275465: x = ((x ◇ (((y ◇ z) ◇ w) ◇ (x ◇ ((u ◇ u) ◇ y)))) ◇ x) ◇ y
Equation 602296194: x = y ◇ ((y ◇ z) ◇ (w ◇ ((y ◇ (u ◇ x)) ◇ (z ◇ (v ◇ y)))))
Equation 1273938569: x = (y ◇ x) ◇ (y ◇ (z ◇ (y ◇ (((z ◇ z) ◇ w) ◇ (x ◇ x)))))
Equation 2947915174: x = ((x ◇ y) ◇ ((z ◇ w) ◇ (x ◇ ((x ◇ y) ◇ (y ◇ w))))) ◇ y
Equation 4556743601: x ◇ x = (((((y ◇ (x ◇ y)) ◇ y) ◇ (z ◇ w)) ◇ u) ◇ w) ◇ v
Equation 2818140173: x = (y ◇ ((((z ◇ (w ◇ w)) ◇ u) ◇ (y ◇ z)) ◇ (z ◇ z))) ◇ x
Equation 810512212: x = y ◇ ((((x ◇ z) ◇ z) ◇ (w ◇ w)) ◇ (y ◇ (w ◇ (z ◇ w))))
Equation 4922552802: (x ◇ x) ◇ y = z ◇ ((z ◇ (w ◇ (((u ◇ z) ◇ u) ◇ v))) ◇ w)
Equation 1165413432: x = y ◇ (((((x ◇ z) ◇ w) ◇ ((y ◇ z) ◇ u)) ◇ (z ◇ v)) ◇ y)
Equation 1909109109: x = (y ◇ ((x ◇ z) ◇ (z ◇ x))) ◇ ((((y ◇ x) ◇ w) ◇ w) ◇ w)

and one with 19 operands

Equation 363793511899060201570137: x = ((y ◇ x) ◇ z) ◇ ((((z ◇ w) ◇ ((x ◇ u) ◇ v)) ◇ ((z ◇ (w ◇ (z ◇ ((r ◇ r) ◇ z)))) ◇ (((u ◇ y) ◇ z) ◇ w))) ◇ (w ◇ x))
Equation 1281089033296964870512410: (x ◇ y) ◇ (z ◇ w) = (y ◇ (((u ◇ v) ◇ (v ◇ (((((r ◇ (w ◇ x)) ◇ w) ◇ r) ◇ x) ◇ (((x ◇ x) ◇ y) ◇ v)))) ◇ r)) ◇ (r ◇ w)
Equation 1098679464628395735713922: x ◇ y = ((z ◇ (((x ◇ z) ◇ ((w ◇ (x ◇ (z ◇ u))) ◇ (v ◇ w))) ◇ (r ◇ (((v ◇ z) ◇ y) ◇ ((w ◇ w) ◇ (s ◇ v)))))) ◇ r) ◇ y
Equation 514169071047350318203529: x = ((y ◇ (z ◇ w)) ◇ (u ◇ ((v ◇ ((r ◇ (u ◇ (v ◇ y))) ◇ ((u ◇ r) ◇ r))) ◇ (x ◇ z)))) ◇ (w ◇ (r ◇ (r ◇ ((s ◇ w) ◇ x))))
Equation 984598712119499325661720: x ◇ y = (((y ◇ (z ◇ w)) ◇ u) ◇ v) ◇ (r ◇ ((((s ◇ v) ◇ ((w ◇ ((r ◇ u) ◇ r)) ◇ ((s ◇ y) ◇ (x ◇ w)))) ◇ (s ◇ s)) ◇ r))
Equation 1189116426716184743370991: (x ◇ y) ◇ z = y ◇ (((w ◇ (((u ◇ w) ◇ (v ◇ r)) ◇ (w ◇ z))) ◇ (r ◇ (s ◇ (((u ◇ (v ◇ r)) ◇ (t ◇ w)) ◇ (y ◇ a))))) ◇ x)
Equation 90342697770149997794808: x = y ◇ (z ◇ (((z ◇ ((x ◇ ((((y ◇ w) ◇ u) ◇ v) ◇ x)) ◇ (y ◇ ((y ◇ z) ◇ (w ◇ (v ◇ (x ◇ x))))))) ◇ (z ◇ x)) ◇ (x ◇ v)))
Equation 394968337506739099909707: x = (y ◇ ((z ◇ z) ◇ (w ◇ u))) ◇ (v ◇ ((((y ◇ w) ◇ ((v ◇ (r ◇ s)) ◇ (v ◇ y))) ◇ ((((t ◇ a) ◇ b) ◇ (v ◇ y)) ◇ c)) ◇ d))
Equation 415673619149372168134875: x = ((y ◇ x) ◇ ((z ◇ w) ◇ (u ◇ u))) ◇ ((u ◇ v) ◇ (((v ◇ ((((r ◇ (y ◇ (s ◇ ((u ◇ r) ◇ r)))) ◇ v) ◇ u) ◇ y)) ◇ y) ◇ t))
Equation 1532454742108685033082571: x ◇ (((y ◇ z) ◇ x) ◇ ((w ◇ (x ◇ u)) ◇ (u ◇ z))) = (v ◇ (r ◇ (u ◇ (s ◇ ((s ◇ z) ◇ z))))) ◇ ((w ◇ (y ◇ r)) ◇ (u ◇ z))
Equation 1258540976367805646481554: x ◇ ((y ◇ z) ◇ z) = (z ◇ x) ◇ ((z ◇ (((((w ◇ u) ◇ (((z ◇ w) ◇ (z ◇ z)) ◇ v)) ◇ (w ◇ r)) ◇ s) ◇ (w ◇ s))) ◇ (t ◇ s))
Equation 949832392607223970612915: x ◇ y = (z ◇ x) ◇ (x ◇ (((w ◇ (x ◇ u)) ◇ z) ◇ (v ◇ (x ◇ (z ◇ (x ◇ ((r ◇ ((r ◇ v) ◇ ((x ◇ (w ◇ s)) ◇ t))) ◇ z)))))))
Equation 104992724806068835245264: x = y ◇ (z ◇ (((w ◇ (((((u ◇ (v ◇ ((z ◇ v) ◇ ((r ◇ w) ◇ x)))) ◇ ((s ◇ r) ◇ t)) ◇ t) ◇ (w ◇ t)) ◇ (s ◇ a))) ◇ r) ◇ y))
Equation 765832307945052398045396: x = ((((((y ◇ z) ◇ x) ◇ y) ◇ (w ◇ w)) ◇ u) ◇ (((u ◇ ((x ◇ z) ◇ u)) ◇ (((u ◇ x) ◇ w) ◇ ((v ◇ z) ◇ w))) ◇ (u ◇ x))) ◇ v
Equation 502360515847596955679418: x = ((y ◇ (((z ◇ (y ◇ w)) ◇ (u ◇ v)) ◇ r)) ◇ ((w ◇ s) ◇ ((v ◇ (v ◇ w)) ◇ t))) ◇ (v ◇ (((a ◇ v) ◇ ((a ◇ w) ◇ b)) ◇ a))
Equation 698331066872627590170608: x = (x ◇ (((((y ◇ (x ◇ x)) ◇ z) ◇ w) ◇ ((u ◇ (z ◇ (v ◇ (w ◇ (((r ◇ y) ◇ (x ◇ s)) ◇ y))))) ◇ v)) ◇ (u ◇ (t ◇ a)))) ◇ z
Equation 837193017485887935695868: x = ((y ◇ ((z ◇ (w ◇ (((u ◇ ((v ◇ (y ◇ u)) ◇ (w ◇ (((v ◇ r) ◇ s) ◇ x)))) ◇ z) ◇ (((u ◇ x) ◇ y) ◇ r)))) ◇ y)) ◇ r) ◇ z
Equation 178172409984494926151526: x = y ◇ ((((z ◇ (((w ◇ w) ◇ ((z ◇ u) ◇ x)) ◇ u)) ◇ ((v ◇ w) ◇ (r ◇ x))) ◇ (s ◇ (z ◇ v))) ◇ ((x ◇ v) ◇ ((x ◇ y) ◇ u)))
Equation 1564696276247327988447311: (((x ◇ y) ◇ ((z ◇ ((z ◇ w) ◇ u)) ◇ v)) ◇ z) ◇ r = ((v ◇ ((s ◇ t) ◇ a)) ◇ t) ◇ (r ◇ (b ◇ ((c ◇ s) ◇ (a ◇ (s ◇ z)))))
Equation 573854630796579181896363: x = ((y ◇ z) ◇ (z ◇ ((w ◇ u) ◇ ((((z ◇ w) ◇ (u ◇ v)) ◇ (r ◇ (z ◇ (s ◇ (((s ◇ w) ◇ s) ◇ y))))) ◇ s)))) ◇ (w ◇ (v ◇ x))

I'm still working on making my code work fast for even numbers of operations, which is trickier due to the symmetries involved.

[Amir Livne Bar-on]

Nice! How did you make the numbering work fast enough?

About sampling even ones, if you reduce the probability of the duplicate elements by 50%, for example by flipping a coin if you stumble upon one. Or dropping the non-canonical version if you canonicalize the non-duplicates. It's easy to detect duplicate elements, these are the ones with the same parentheses pattern on the left and right sides.

[Amir Livne Bar-on]

(numbering them is more difficult)

[Bruno Le Floch]

Let me explain the odd case. For each of the catalan(n+1)/2 trees there are bell(n+2) possible rhyme schemes, so the problem boils down to a division by bell(n+2) with remainder, and to separately being able to generate the i-th tree and j-th rhyme scheme. For trees we just have to determine how many nodes are in the left and right subtrees (then recurse), which we can do by remembering where the $C_{n+1} = \sum_{k=0}^n C_k C_{n-k}$ formula comes from: each term corresponds to a given number of nodes on the left. So just compare the target number i to the partial sums. For partitions the idea is the same, at any stage we just need to know how many partitions have a given number next; the calculations are a bit more annoying.

For the even case it is of course more complicated, and I only dealt fully with the case of trees with fewer nodes on the left than on the right, not with the equality case. I see how to deal further with the case of different shapes on the left/right, but for the case of equal shapes I will need to understand the recursive formulas for oeis' A376640 a bit better.

If my initial goal had been just to produce random instances without numbering, I agree your approach makes sense. But I'd rather not implement that, since I will hopefully finish implementing the numbering next weekend once day job stuff has subsided.

[Bruno Le Floch]

Just for fun (and to stress-test that my implementation is polynomial in the number of operations): equation $10^{100}$ is as follows, with 91 variables and 445 operations.

x = (y ◇ (z ◇ (((w ◇ u) ◇ v) ◇ (((r ◇ s) ◇ t) ◇ a)))) ◇ (((b ◇ ((s ◇ c)
◇ (d ◇ (e ◇ f)))) ◇ g) ◇ (h ◇ (((((((i ◇ j) ◇ ((k ◇ (l ◇ m)) ◇ ((n ◇ (o
◇ p)) ◇ ((q ◇ X) ◇ (((m ◇ Y) ◇ ((z ◇ (((((Z ◇ W) ◇ (c ◇ ((U ◇ (((((V ◇
(R ◇ (S ◇ T))) ◇ ((j ◇ A) ◇ B)) ◇ C) ◇ t) ◇ (D ◇ (((((((((u ◇ E) ◇ F) ◇
(X ◇ ((G ◇ (((A ◇ ((((((H ◇ g) ◇ X) ◇ I) ◇ (g ◇ J)) ◇ r) ◇ (Y ◇ (K ◇
l)))) ◇ (((Z ◇ L) ◇ Y) ◇ (A ◇ M))) ◇ (((N ◇ ((O ◇ (X ◇ (P ◇ f))) ◇ Q)) ◇
(a ◇ (w ◇ (α ◇ A)))) ◇ (o ◇ V)))) ◇ β))) ◇ (s ◇ γ)) ◇ (p ◇ a)) ◇ y) ◇ (I
◇ ((P ◇ ((δ ◇ (c ◇ ε)) ◇ (G ◇ ((C ◇ ((((ζ ◇ β) ◇ t) ◇ (η ◇ ((δ ◇ (θ ◇
((((G ◇ (r ◇ (ι ◇ ((H ◇ h) ◇ κ)))) ◇ P) ◇ I) ◇ J))) ◇ ((((l ◇ ((((((Z ◇
(λ ◇ (μ ◇ δ))) ◇ (I ◇ (κ ◇ ((((((ν ◇ ξ) ◇ (Q ◇ (ο ◇ (((π ◇ s) ◇ Y) ◇
ρ)))) ◇ (h ◇ (I ◇ (ο ◇ (ς ◇ K))))) ◇ u) ◇ n) ◇ O)))) ◇ δ) ◇ p) ◇ (n ◇ (l
◇ λ))) ◇ (l ◇ (σ ◇ E)))) ◇ (((((τ ◇ (((L ◇ υ) ◇ ((φ ◇ (χ ◇ ((ς ◇ (S ◇
o)) ◇ ((U ◇ κ) ◇ (E ◇ D))))) ◇ (((((((υ ◇ μ) ◇ Y) ◇ θ) ◇ i) ◇ (ψ ◇ H)) ◇
(Y ◇ k)) ◇ (ς ◇ ((S ◇ (C ◇ F)) ◇ ((s ◇ c) ◇ (τ ◇ m))))))) ◇ (μ ◇ j))) ◇
s) ◇ ω) ◇ τ) ◇ S)) ◇ (v ◇ (((Y ◇ β) ◇ (((n ◇ (((((L ◇ 가) ◇ μ) ◇ (β ◇
J)) ◇ (t ◇ (z ◇ (ψ ◇ I)))) ◇ ((A ◇ e) ◇ (υ ◇ H)))) ◇ (υ ◇ (V ◇ (A ◇
α)))) ◇ ((각 ◇ (((((θ ◇ (I ◇ ((ψ ◇ (L ◇ B)) ◇ i))) ◇ ((((가 ◇ (U ◇ M)) ◇
갂) ◇ (T ◇ S)) ◇ F)) ◇ ζ) ◇ ((((C ◇ (ς ◇ p)) ◇ p) ◇ ((갃 ◇ r) ◇ ((((((X
◇ x) ◇ ((a ◇ (υ ◇ (((w ◇ ((O ◇ ζ) ◇ (((ο ◇ ((간 ◇ (((((G ◇ (W ◇ H)) ◇
갅) ◇ K) ◇ (((((z ◇ L) ◇ K) ◇ S) ◇ μ) ◇ Z)) ◇ ((ω ◇ υ) ◇ t))) ◇ (γ ◇
c))) ◇ y) ◇ (Z ◇ ο)))) ◇ 갆) ◇ (((각 ◇ (χ ◇ (Q ◇ (T ◇ ((((v ◇ υ) ◇ (λ ◇
((a ◇ α) ◇ ρ))) ◇ ((η ◇ σ) ◇ ((((c ◇ C) ◇ (m ◇ ((φ ◇ m) ◇ P))) ◇ y) ◇ (z
◇ B)))) ◇ ξ))))) ◇ ρ) ◇ α)))) ◇ ξ)) ◇ α) ◇ ((((B ◇ (((β ◇ ((K ◇ ((A ◇
(((η ◇ k) ◇ y) ◇ (((ξ ◇ (o ◇ ((((R ◇ f) ◇ K) ◇ o) ◇ D))) ◇ (ς ◇ (υ ◇ ((l
◇ (((갇 ◇ (v ◇ M)) ◇ 갅) ◇ p)) ◇ (((n ◇ (ξ ◇ δ)) ◇ Q) ◇ 갅))))) ◇ G))) ◇
m)) ◇ ι)) ◇ 갈) ◇ λ)) ◇ (c ◇ (z ◇ (ρ ◇ (m ◇ Q))))) ◇ X) ◇ x)) ◇ λ) ◇
A))) ◇ (κ ◇ (갉 ◇ ((κ ◇ ω) ◇ V))))) ◇ (ζ ◇ 갆))) ◇ c))) ◇ ((o ◇ υ) ◇
Q)))) ◇ F)))) ◇ (ε ◇ Z))) ◇ ((η ◇ (((Z ◇ (((δ ◇ w) ◇ (갂 ◇ (B ◇ (((δ ◇
((K ◇ τ) ◇ (갆 ◇ W))) ◇ P) ◇ ((β ◇ 갃) ◇ (d ◇ (((F ◇ (C ◇ ((갅 ◇ Z) ◇
(((ζ ◇ b) ◇ (갉 ◇ n)) ◇ ξ)))) ◇ (φ ◇ ((((((Q ◇ (갇 ◇ (((N ◇ 각) ◇ κ) ◇
σ))) ◇ Z) ◇ ((갉 ◇ (갊 ◇ ((각 ◇ (p ◇ ((((s ◇ σ) ◇ 갇) ◇ C) ◇ n))) ◇
(((갅 ◇ 갇) ◇ (F ◇ I)) ◇ λ)))) ◇ 갈)) ◇ ψ) ◇ I) ◇ ((S ◇ 각) ◇ Z)))) ◇ (C
◇ 갆)))))))) ◇ o)) ◇ (Q ◇ β)) ◇ ξ)) ◇ ν))))) ◇ t))) ◇ (m ◇ (((u ◇ ((갃 ◇
E) ◇ c)) ◇ δ) ◇ (갇 ◇ 간)))) ◇ E)))) ◇ (a ◇ 갋)))) ◇ ((갌 ◇ (w ◇ n)) ◇
(ψ ◇ (β ◇ (σ ◇ C))))) ◇ j) ◇ π)) ◇ τ)) ◇ n))))) ◇ D) ◇ (b ◇ 갃)) ◇ (η ◇
f)) ◇ (((σ ◇ ((L ◇ (갉 ◇ (H ◇ ((K ◇ (C ◇ (F ◇ k))) ◇ (t ◇ (((((b ◇ T) ◇
(i ◇ μ)) ◇ (가 ◇ α)) ◇ (n ◇ v)) ◇ 갍)))))) ◇ ((((((Y ◇ 갈) ◇ η) ◇ I) ◇
(ς ◇ ((갊 ◇ M) ◇ ((갅 ◇ X) ◇ ς)))) ◇ C) ◇ e))) ◇ (S ◇ (t ◇ φ))) ◇ 갍)) ◇
(t ◇ P))))

[Eric Taucher]

Bruno Le Floch said:

Equation 4082587915: x ◇ y = (x ◇ (z ◇ (w ◇ (y ◇ u)))) ◇ (u ◇ (u ◇ (v ◇ r)))

1. Can the id (4082587915) be used to create a unique equation ?
2. Can the equation be used to calculate a unique id?
3. If this is a generator, are all of the equation for this project created and in order by id?

Did you by chance post the code and I missed it?

[Bruno Le Floch]

@Eric Taucher Yes, the mapping is one-to-one from positive integers to equations counted by A376640. I didn't yet post the code sorry, I'll do it tonight in a pull request.

[Vlad Tsyrklevich]

One more simple rule I thought of for non-equivalence to equation 2: any RHS with an odd number of occurrences of x and even numbers of occurrences of the other variables. The idea being that for example XOR satisfies this model.

[Ibrahim Tencer]

Vlad Tsyrklevich said:

One more simple rule I thought of for non-equivalence to equation 2: any RHS with an odd number of occurrences of x and even numbers of occurrences of the other variables. The idea being that for example XOR satisfies this model.

Yes, and this is an example of a general pattern: if we define the degree of a variable v in the equation as (occurrences on right - occurrences of left) then when the gcd of the degrees is n, Z/nZ will be a model.

[Bruno Le Floch]

fast_find_equation_id.py
@Eric Taucher I don't quite have the energy to clean up the code all the way to being a reasonable pull request tonight, but here is is. Usage: python fast_find_equation_id.py 23498 10233493498 "x=t*(x*(z*u))"

[Eric Taucher]

Bruno Le Floch said:

here it is

Thanks. Found the interactive mode and gave it a few simple cases to check. Works as expected. Nice!

python fast_find_equation_id.py -i

C:\Users\Groot\Projects\Python Magma Equation generator>python fast_find_equation_id.py -i
Welcome to the interactive equation canonicalizer!
Type 'exit' or 'quit' to end the session.
Enter an equation: x = x
The equation 'x = x' is Equation 1: x = x
Enter an equation: x = y
The equation 'x = y' is Equation 2: x = y
Enter an equation: x = x * x
The equation 'x = x * x' is Equation 3: x = x ◇ x
Enter an equation: x = y * z
The equation 'x = y * z' is Equation 7: x = y ◇ z
Enter an equation: x = x * ( x * x)
The equation 'x = x * ( x * x)' is Equation 8: x = x ◇ (x ◇ x)
Enter an equation: x = x ◇ (x ◇ x)
The equation 'x = x ◇ (x ◇ x)' is Equation 8: x = x ◇ (x ◇ x)
Enter an equation: x = y ◇ (z ◇ w)
The equation 'x = y ◇ (z ◇ w)' is Equation 22: x = y ◇ (z ◇ w)
Enter an equation: x ◇ x = x ◇ y
The equation 'x ◇ x = x ◇ y' is Equation 38: x ◇ x = x ◇ y
Enter an equation: x = x ◇ (x ◇ (x ◇ x))
The equation 'x = x ◇ (x ◇ (x ◇ x))' is Equation 47: x = x ◇ (x ◇ (x ◇ x))
Enter an equation: x = ((y ◇ z) ◇ w) ◇ u
The equation 'x = ((y ◇ z) ◇ w) ◇ u' is Equation 306: x = ((y ◇ z) ◇ w) ◇ u
Enter an equation: x ◇ x = x ◇ (x ◇ x)
The equation 'x ◇ x = x ◇ (x ◇ x)' is Equation 307: x ◇ x = x ◇ (x ◇ x)
Enter an equation: x = x ◇ (x ◇ (x ◇ (x ◇ x)))
The equation 'x = x ◇ (x ◇ (x ◇ (x ◇ x)))' is Equation 411: x = x ◇ (x ◇ (x ◇ (x ◇ x)))
Enter an equation: 100
Equation 100: x = x ◇ ((x ◇ x) ◇ y)
Enter an equation: 1
Equation 1: x = x
Enter an equation: 2
Equation 2: x = y
Enter an equation: 3
Equation 3: x = x ◇ x
Enter an equation: 307
Equation 307: x ◇ x = x ◇ (x ◇ x)
Enter an equation: quit
Goodbye!

Selected laws

Selected laws by number

C:\Users\Groot\Projects\Python Magma Equation generator>python fast_find_equation_id.py -i
Welcome to the interactive equation canonicalizer!
Type 'exit' or 'quit' to end the session.
Enter an equation: 1
Equation 1: x = x
Enter an equation: 2
Equation 2: x = y
Enter an equation: 3
Equation 3: x = x ◇ x
Enter an equation: 4
Equation 4: x = x ◇ y
Enter an equation: 5
Equation 5: x = y ◇ x
Enter an equation: 6
Equation 6: x = y ◇ y
Enter an equation: 7
Equation 7: x = y ◇ z
Enter an equation: 8
Equation 8: x = x ◇ (x ◇ x)
Enter an equation: 14
Equation 14: x = y ◇ (x ◇ y)
Enter an equation: 16
Equation 16: x = y ◇ (y ◇ x)
Enter an equation: 23
Equation 23: x = (x ◇ x) ◇ x
Enter an equation: 29
Equation 29: x = (y ◇ x) ◇ y
Enter an equation: 38
Equation 38: x ◇ x = x ◇ y
Enter an equation: 39
Equation 39: x ◇ x = y ◇ x
Enter an equation: 40
Equation 40: x ◇ x = y ◇ y
Enter an equation: 41
Equation 41: x ◇ x = y ◇ z
Enter an equation: 42
Equation 42: x ◇ y = x ◇ z
Enter an equation: 43
Equation 43: x ◇ y = y ◇ x
Enter an equation: 45
Equation 45: x ◇ y = z ◇ y
Enter an equation: 46
Equation 46: x ◇ y = z ◇ w
Enter an equation: 63
Equation 63: x = y ◇ (x ◇ (x ◇ y))
Enter an equation: 65
Equation 65: x = y ◇ (x ◇ (y ◇ x))
Enter an equation: 168
Equation 168: x = (y ◇ x) ◇ (x ◇ z)
Enter an equation: 206
Equation 206: x = (x ◇ (x ◇ y)) ◇ y
Enter an equation: 381
Equation 381: x ◇ y = (x ◇ z) ◇ y
Enter an equation: 387
Equation 387: x ◇ y = (y ◇ y) ◇ x
Enter an equation: 477
Equation 477: x = y ◇ (x ◇ (y ◇ (y ◇ y)))
Enter an equation: 854
Equation 854: x = x ◇ ((y ◇ z) ◇ (x ◇ z))
Enter an equation: 953
Equation 953: x = y ◇ ((z ◇ x) ◇ (z ◇ z))
Enter an equation: 1485
Equation 1485: x = (y ◇ x) ◇ (x ◇ (z ◇ y))
Enter an equation: 1491
Equation 1491: x = (y ◇ x) ◇ (y ◇ (y ◇ x))
Enter an equation: 1571
Equation 1571: x = (y ◇ z) ◇ (y ◇ (x ◇ z))
Enter an equation: 1648
Equation 1648: x = (x ◇ y) ◇ ((x ◇ y) ◇ y)
Enter an equation: 1657
Equation 1657: x = (x ◇ y) ◇ ((y ◇ y) ◇ x)
Enter an equation: 1659
Equation 1659: x = (x ◇ y) ◇ ((y ◇ y) ◇ z)
Enter an equation: 1661
Equation 1661: x = (x ◇ y) ◇ ((y ◇ z) ◇ y)
Enter an equation: 1689
Equation 1689: x = (y ◇ x) ◇ ((x ◇ z) ◇ z)
Enter an equation: 1701
Equation 1701: x = (y ◇ x) ◇ ((z ◇ x) ◇ x)
Enter an equation: 2662
Equation 2662: x = ((x ◇ y) ◇ (x ◇ y)) ◇ x
Enter an equation: 3167
Equation 3167: x = (((y ◇ y) ◇ z) ◇ z) ◇ x
Enter an equation: 3588
Equation 3588: x ◇ y = z ◇ ((x ◇ y) ◇ z)
Enter an equation: 3722
Equation 3722: x ◇ y = (x ◇ y) ◇ (x ◇ y)
Enter an equation: 3744
Equation 3744: x ◇ y = (x ◇ z) ◇ (w ◇ y)
Enter an equation: 3994
Equation 3994: x ◇ y = (z ◇ (x ◇ y)) ◇ z
Enter an equation: 4315
Equation 4315: x ◇ (y ◇ x) = x ◇ (y ◇ z)
Enter an equation: 4512
Equation 4512: x ◇ (y ◇ z) = (x ◇ y) ◇ z
Enter an equation: 4513
Equation 4513: x ◇ (y ◇ z) = (x ◇ y) ◇ w
Enter an equation: 4522
Equation 4522: x ◇ (y ◇ z) = (x ◇ w) ◇ u
Enter an equation: 4564
Equation 4564: x ◇ (y ◇ z) = (w ◇ y) ◇ z
Enter an equation: 4579
Equation 4579: x ◇ (y ◇ z) = (w ◇ u) ◇ z
Enter an equation: 4582
Equation 4582: x ◇ (y ◇ z) = (w ◇ u) ◇ v
Enter an equation: 5093
Equation 5093: x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ y))))
Enter an equation: 26302
Equation 26302: x = (y ◇ ((z ◇ x) ◇ w)) ◇ (x ◇ w)
Enter an equation: 28770
Equation 28770: x = (((y ◇ y) ◇ y) ◇ x) ◇ (y ◇ z)
Enter an equation: 345169
Equation 345169: x = (y ◇ ((x ◇ y) ◇ y)) ◇ (x ◇ (z ◇ y))
Enter an equation: 374794
Equation 374794: x = (((y ◇ y) ◇ y) ◇ x) ◇ ((y ◇ y) ◇ z)
Enter an equation: quit
Goodbye!

[Eric Taucher]

Bruno Le Floch said:

I don't quite have the energy to clean up the code all the way to being a reasonable pull request tonight

What you provided is more than adequate. Mostly curious if you extended generate_eqs_list.py by Terry (which is yes) or created something different. Impressed with the calculation of l to help determine the left-hand side shape of a balanced equation..

calculation of l for left

l = ((2*m - 1) * bell(n + 2) + 2 * bell_same_shape(n)
         - isqrt(((2 * m - 1) * bell(n + 2) + 2 * bell_same_shape(n)) ** 2
                 - 8 * bell(n + 2) * eq_num - 1)
         - 1) // (2*bell(n + 2))

[Bruno Le Floch]

Mostly curious if you extended generate_eqs_list.py by Terry (which is yes) or created something different.

I extended find_equation_id.py, which was maybe already an extension of Terry's code.

Impressed with the calculation of l to help determine the left-hand side shape of a balanced equation..

Thanks, it was a bit messy to get. Basically the question is: in a triangle of the form

ebbbbb
 ebbbb
  ebbb
   ebb
    eb
     e

where e stands for the number of partitions that are valid when lhs and rhs have equal shapes and b the number when lhs and rhs have different shapes, given p, find the maximum position (i,j) in the triangle such that the sum of numbers e, b "before" the position (i,j) (from top to bottom, left to right) is less or equal to p. Inevitably this sum of e,b is quadratic in i (and linear in j-i) so we need an integer square root somewhere.

[Michael Bucko]

Bruno Le Floch schrieb:

23498 10233493498 "x=t*(x*(z*u))

It's awesome. Added the --solve and the --simplify options to the script, in case if anyone's interested.

python3 ./fast_find2.py 23498 10233493498 "x=t*(x*(z*u))"

Equation 23498: x = ((y ◇ y) ◇ x) ◇ (z ◇ (w ◇ x))

Equation 10233493498: x = y ◇ (z ◇ ((y ◇ (x ◇ (x ◇ (w ◇ (((w ◇ y) ◇ u) ◇ v))))) ◇ x))

The equation 'x=t*(x*(z*u))' is Equation 71: x = y ◇ (x ◇ (z ◇ w))

(myenc) riccitensor@perelman equational_theories % python3 ./fast_find2.py 23498 10233493498 "x=t*(x*(z*u))" --simplify

Equation 23498: x = ((y ◇ y) ◇ x) ◇ (z ◇ (w ◇ x))

Simplified Equation 23498: x = ((y ◇ y) ◇ x) ◇ (z ◇ (w ◇ x))

Equation 10233493498: x = y ◇ (z ◇ ((y ◇ (x ◇ (x ◇ (w ◇ (((w ◇ y) ◇ u) ◇ v))))) ◇ x))

Simplified Equation 10233493498: x = y ◇ (z ◇ ((y ◇ (x ◇ (x ◇ (w ◇ (((w ◇ y) ◇ u) ◇ v))))) ◇ x))

The equation 'x=t*(x*(z*u))' is Equation 71: x = y ◇ (x ◇ (z ◇ w))

Simplified Equation 71: x = y ◇ (x ◇ (z ◇ w))

(myenc) riccitensor@perelman equational_theories % python3 ./fast_find2.py
 23498 10233493498 "x=t*(x*(z*u))" --solve

Equation 23498: x = ((y ◇ y) ◇ x) ◇ (z ◇ (w ◇ x))

Error while solving: No algorithms are implemented to solve equation x - Diamond(Diamond(Diamond(y, y), x), Diamond(z, Diamond(w, x)))

No solutions found or the equation does not contain variables to solve for.

Equation 10233493498: x = y ◇ (z ◇ ((y ◇ (x ◇ (x ◇ (w ◇ (((w ◇ y) ◇ u) ◇ v))))) ◇ x))

Error while solving: No algorithms are implemented to solve equation x - Diamond(y, Diamond(z, Diamond(Diamond(y, Diamond(x, Diamond(x, Diamond(w, Diamond(Diamond(Diamond(w, y), u), v))))), x)))

No solutions found or the equation does not contain variables to solve for.

The equation 'x=t*(x*(z*u))' is Equation 71: x = y ◇ (x ◇ (z ◇ w))

Error while solving: No algorithms are implemented to solve equation x - Diamond(y, Diamond(x, Diamond(z, w)))

No solutions found or the equation does not contain variables to solve for.

fast_find2.py

[Terence Tao]

Just for the record, generate_eqs_list.py is almost entirely @Amir Livne Bar-on 's code. I may have been the last to edit it to change a configuration parameter.

[Bruno Le Floch]

Michael Bucko said:

It's awesome. Added the --solve and the --simplify options to the script, in case if anyone's interested.

Sorry, I don't understand what these do. Sympy does not seem to simplify the equations in any case, nor can it solve the equation in a meaningful sense. Can you explain a bit?

[Amir Livne Bar-on]

For completeness I'll add that @Nicholas Carlini wrote find_equation_id.py

[Michael Bucko]

Bruno Le Floch schrieb:

Michael Bucko said:

It's awesome. Added the --solve and the --simplify options to the script, in case if anyone's interested.

Sorry, I don't understand what these do. Sympy does not seem to simplify the equations in any case, nor can it solve the equation in a meaningful sense. Can you explain a bit?

Simplify - it simply uses Sympy's simplify. Did it for myself to see what I can get out of Sympy.
Solve - uses Sympy's solve. I am not expecting it'll solve the equation. My goal here was to evaluate Sympy's current capabilities.

You can use --simplify or --solve to experiment. I'm doing this, so I shared the script (since it's based on your work).

[Terence Tao]

Experimenting with new code features on your own is fine, but for code that is not extremely time-sensitive (e.g., a patch for an ongoing bug), I would recommend that such code be subject to more testing before sharing it with the other participants here, in particular ensuring that the output doesn't simply look "neat" but actually solves some useful problem.

[Bruno Le Floch]

Now the script/module find_equation.py is available and merged. It is efficient (polynomial in the number of operations) as long as the equation (or equation id) under consideration does not have the same shape on the left and right hand sides. In that case it becomes linear in the number of partitions, which means (very slightly sub)linear in the equation id.