Reconstructing the 4694 expressions from the ground up.

Stream: Equational

[Eric Taucher]

I do not have a degree in math but a BS in computer science. One of my goals with this project is to understand how the 4694 expression in https://github.com/teorth/equational_theories/blob/main/data/equations.txt
where created.

The info in the Blueprint page is quite helpful but leaves me guessing at how to exactly do some things. Also looked at the Python code, however it did not help in starting from the ground up. With ChatGPT , it is not so useful when one does not know how to verify what is given.

So to start this side task could someone list the 16 items for

The number of magma structures on a set  G of cardinality n is of course , n^(n^2)

so then I can attempt to do the same with some code when N is 3 .

Note: I did look at https://oeis.org/A002489 for some help as it sometimes will list such but in this case only fond list of the sequence.

[Terence Tao]

The 2^(2^2) magmas of order 2 can be given by the multiplication tables [[0,0], [0,0]], [[0,0], [0,1]] [[0,0], [1,0]] [[0,0], [1,1]] [[0,0], [0,1]] [[0,0], [0,0]] [[0,1], [0,1]] [[0,1], [1,0]], [[0,1], [1,1]], [[1,0], [0,0]], [[1,0], [0,1]] [[1,0], [1,0]] [[1,0], [1,1]] [[1,0], [0,1]] [[1,0], [1,0]] [[1,1], [0,1]] [[1,1], [1,0]], [[1,1], [1,1]], but this does not directly relate to the equations.

The 4694 equations are all the laws that can be generated using at most 4 uses of the ◇ symbol (using parentheses as necessary), with the following additional rules:

• Any equation of the form w = w, where w is not just a single variable, is deleted. For instance, we do not consider the law x ◇ y = x ◇ y.
• We name the variables, in order of first appearance reading from left to right, according to the (somewhat arbitrary) ordering xyzwuvrst (though for the initial 4692 laws we never need to go past v). For instance, we would spell the associative law as x ◇ (y ◇ z) = (x ◇ y) ◇ z as opposed to say y ◇ (x ◇ z) = (y ◇ x) ◇ z.
• Given an equation w = w' and its reverse w' = w, we keep the one that appears first in the ordering we chose (after renaming the variables if necessary). For instance, x = y ◇ x reverses to y ◇ x = x, or x ◇ y = y after using the above naming convention, but x = y ◇ x appears earlier in our ordering x ◇ y = y, so we keep that one.
• Our ordering is such that shorter laws (i.e., laws with fewer total appearances of ◇) appear earlier than later ones. For instance, equations 1-2 are the laws with no ◇ operations, equations 3-7 are the laws with one ◇ operation, equations 8-46 are the laws with two ◇ operations, and so forth.
• Among laws of the same length, laws with a shorter left-hand side appear first. For instance, among the equations 8-46 that have two two ◇ operations, equations 8-22 have no ◇ operations on the left-hand side, and equations 23-46 have one ◇ operation on the left-hand side. (We don't have any equations with two ◇ operations on the left hand side here, because their reversal would have come earlier in the sequence.)
• The ordering on laws with a fixed length on both the left-hand side and right-hand side is a bit hard to explain (recursive lexicographic). At this point it is easier just to point to the python code than to try to describe it properly here.

[Joachim Breitner]

A lean function implementing this order is in https://github.com/teorth/equational_theories/blob/ac7e97bcf877a590a022a597ce44ef70ceb5cefe/equational_theories/Equations/LawsComplete.lean#L53, for those who read code better then prose. It's worth noting that it first orders by the shape of the law (all variables erased), and then by the variables occurring.

[Michael Bucko]

Joachim Breitner schrieb:

A lean function implementing this order is in https://github.com/teorth/equational_theories/blob/ac7e97bcf877a590a022a597ce44ef70ceb5cefe/equational_theories/Equations/LawsComplete.lean#L53, for those who read code better then prose. It's worth noting that it first orders by the shape of the law (all variables erased), and then by the variables occurring.

Thank you. Checked it out and then generated this with O1.

Define FreeMagma(Nat):
  Leaf(i)         // Variable i
  Fork(left, right) // Binary operation of two FreeMagma expressions

Define NatMagmaLaw:
  lhs: FreeMagma(Nat)
  rhs: FreeMagma(Nat)

Define Ordering comp for FreeMagma:
  Compare number of forks
  If equal, compare structures recursively:
    Leaf vs. Fork
    Compare variable indices

Define Ordering comp for NatMagmaLaw:
  Compare total forks in lhs and rhs
  Compare canonical forms (variables mapped to zero)
  Break ties using original variables

Canonicalize FreeMagma m:
  Initialize empty variable mapping
  Renumber variables in order of first appearance

Check is_canonical for FreeMagma m:
  Ensure variables are numbered from 0 upward without gaps or repeats

Canonicalize NatMagmaLaw l:
  Canonicalize lhs and rhs with shared variable mapping

Prove canonicalize produces is_canonical FreeMagma:
  Use induction on m
  Show variables are renumbered correctly

Build laws array:
  Use elaborator to collect Law1, Law2, ..., LawN into laws array

Find MagmaLaw l in laws:
  Use binary search with comp ordering
  Return index i where laws[i] = l

Test all canonical NatMagmaLaws up to forks ≤ s:
  For s from 0 to max_forks:
    Generate all possible splits of s into s1 and s2
    For each s1, s2:
      Generate all canonical FreeMagmas l with forks = s1
      Generate all canonical FreeMagmas r with forks = s2
      For each pair (l, r):
        If l is canonical and l ≤ r:
          Create law l ≃ r
          If law is canonical:
            Test predicate P(law)

Main Theorem laws_complete:
  For all canonical NatMagmaLaw l with forks ≤ 4:
    There exists i such that laws[i] = l
  Proof:
    Use testLawsUpto(4, P) with P(l) = (laws[findMagmaLaw(l)] = l)

My fav part is testLawsUpto4_computation (even though I don't fully get the decision native_decide vs decide) and the combination of is_canonical / canonicalize_is_canonical (it's beautiful that we can define functions and prove that they work!)

Btw. that kind of functionality could be added to the existing mission-critical systems by converting regular sensitive code into lean, and then generating proofs using ml. I guess it'll take some time before systems we'll get there. I also think such methods could eventually be applied to hardware with much success.

The famous (or perhaps not so famous) example is using 3k+1 variants to control the execution flow. Being able to prove that such a modified algorithm will actually converge could make a diff.

[Eric Taucher]

For those that are creating source code for these concrete examples, considering adding to the respective OEIS entries. :smile:

[Mario Carneiro]

Is there an OEIS sequence whose fourth element is 4694 which generalizes the above?

[Terence Tao]

That would be the partial sums of https://oeis.org/A376640 (which we submitted to OEIS in the first week of the project).

[Mario Carneiro]

Is it possible to compute the Nth law faster than O(N)? I think all of the constraints seem possible to predict in advance except for the symmetry rule

[Mario Carneiro]

Oh, looks like there is a formula listed on https://oeis.org/A376640, based on the stirling, bell, and catalan numbers, I guess that would at least get you into the right ballpark, and then you would need to do binary search on a more precise version of this formula which can estimate how many rejects there are within a group and below N

[Terence Tao]

There is one component of the formula, https://oeis.org/A103293 , which isn't Stirling, Bell, or Catalan based, but still has a (slightly messy) recursive formula that allows for computation in O(N), and certain amount of literature on it. But yes, it is a lower order term and one can get ballpack asymptotics fairly easily, especially when dealing with an odd number of operations in which symmetry just means dividing by 2.

[Mario Carneiro]

O(N) is bad though, that's the complexity of just enumerating everything up to N

[Mario Carneiro]

O(log(N)) is the aim

[Mario Carneiro]

Oh sorry we might have switched meanings of N. In A103293, n is the index in the sequence, which is small, so O(n) is a good asymptotic, while in my question N is the index of a target law in the list, so N is bounded by an exponential in n

[Mario Carneiro]

Step 1 of such an algorithm would be "determine the least n such that N < A103293(n)"

[Mario Carneiro]

which can be done efficiently using Chai Wa Wu's algorithm

[Mario Carneiro]

But step 2 requires you to interact with the specifics of the ordering and rejection rules

[Daniel Weber]

I thought about that a bit, most of the components are easy enumeratively (the shape of the LHS and RHS is different), but when the shape is the same and the difference is in the variable names seems a bit hard to enumerate

[Amir Livne Bar-on]

You can iterate on tree structures, and on partitions once you found the right structure, which is O(Catalan(n) + Bell(n)). The bell numbers grow faster so it will be the dominant part.

[Mario Carneiro]

(I guess this would have been useful for the sporadic laws)

[Terence Tao]

Opened equational#724 for anyone who wants to try the challenge of implementing a reasonable time agorithm for converting an equation to a number of vice versa. For equations of length up to 6 we can simply brute force generate the list, but after that it becomes difficult with our current approach.

[Amir Livne Bar-on]

If we didn't reduce by symmetry of the law, we could easily jump ahead in the partitions. I'm not sure how close we can get to binary search using the standard recurrence for partitions (Bn+1 = SUM Binom(n,k) Bk) but we can probably reduce this to almost polynomial, making the tree structure more dominant. And this is also amenable to sub-divisions.

[Mario Carneiro]

One possibility is to just not reduce by symmetry and instead just leave gaps in the numbering... I imagine that would cause a lot of disruption though

[Eric Taucher]

Terence Tao said:

the challenge of implementing a reasonable time algorithm for converting an equation to a number of vice versa.

Should the numbers be allowed to be changed? In other words the current numbering is from the list https://github.com/teorth/equational_theories/blob/main/data/equations.txt, if it turns out there is a different order that leads to a simpler algorithm would that be allowed?

[Eric Taucher]

The creation of Minimal perfect hash functions come to mind for this problem.

[Terence Tao]

In principle this would work, although the refactor of the entire codebase to the new numbering system would be painful and may lead to subtle errors if not done properly. So I would prefer not to go down this route unless there was an extremely compelling reason to do so.

[Shreyas Srinivas]

Isn't the storage size necessary for perfect hash functions quadratic in the number of keys (I could be wrong, do correct me if so)

[Shreyas Srinivas]

Also the table reconstruction time is also quadratic

[Shreyas Srinivas]

Tbh, I think the idea around git might be good to emulate.

1. Hash each equation with a suitable modern hash function and store the equation with the corresponding file name.

[Shreyas Srinivas]

This makes the equation number content addressable. In other words : give me an equation and I can give you its number as well as all the info that its file contains.

[Shreyas Srinivas]

2. Maintain a tag file that stores tags for specific equations we want to call out by name

[Shreyas Srinivas]

The downside is of course that the numbers are ugly hexadecimals

[Amir Livne Bar-on]

The file names could be equations. With symlinks for equivalents

[Shreyas Srinivas]

You will run into weird file naming conventions

[Shreyas Srinivas]

on different operating systems

[Shreyas Srinivas]

To add the invariance properties, we convert any equation into a canonical form using nat binders

[Shreyas Srinivas]

The nat binder is determined by left-to-right order of universal quantifiers (which I am guessing we will be specifying along with the equation).

[Eric Taucher]

Shreyas Srinivas said:

Isn't the storage size necessary for perfect hash functions quadratic in the number of keys (I could be wrong, do correct me if so)

No ides.

Never created one but this seems like worth mentioning as somethin that I might try and making note of it in case others were not aware of such.

[Eric Taucher]

Terence Tao said:

the refactor of the entire codebase to the new numbering system would be painful

Thanks, yes.

If a different numbering worked better than the current numbering used in the documentation and from the file, I am simply thinking there would be a mapping table from the new numbering to the current numbering. Then both could be used with a note for when the transformation table is needed.

One could prefix each number in the new order, say with a letter, like a-200, so that a-200 is not confused with just 200 and that a-200 would have to be looked up to find the index for the current numbering from the file.

No real need to put more thought into this unless a different numbering system works better with a simpler generator algorithm.

[Eric Taucher]

To help me and possibly others understand OEIS A002489 when N=2 created the 16 operations in a few different representations viewable as an HTML page

• Matrix notation, e.g. [[01],[1,0]]
• Cayley table
• Binary operation
• Graph

image.png

https://github.com/EricGT/Equational-implication-graph-four-operations/blob/main/OEIS_A002489_N_%3D2_single_page_application.html

These are also helpful for understanding how to derive the ten isomorphism classes for OEIS A001329 when N=2.

[Eric Taucher]

There is no copyright or license on the file so feel free to use it to help others learn. Maybe others might find it of use in the blueprint. :thinking:

[Michael Bucko]

Eric Taucher schrieb:

To help me and possibly others understand OEIS A002489 when N=2 created the 16 operations in a few different representations viewable as an HTML page

• Matrix notation, e.g. [[01],[1,0]
• Cayley table
• Binary operation
• Graph

image.png

https://github.com/EricGT/Equational-implication-graph-four-operations/blob/main/OEIS_A002489_N_%3D2_single_page_application.html

These are also helpful for understanding how to derive the ten isomorphism classes for OEIS A001329 when N=2.

Very cool! It'd be good to visualize those graphs for arbitrary-length matrices. That way we could simply input the operation table and see the graph.

Bildschirmfoto 2024-10-26 um 17.32.32.png

[Michael Bucko]

Also, I think if you could visualize strategies, ie. what's refuted, what's refuted with duality, what's left, what's needs to be understood. If we get to that level of visualization, I think that'd be helpful. Really cool!

[Eric Taucher]

Michael Bucko said:

It'd be good to visualize those graphs for arbitrary-length matrices.

That is on the TODO list.

Part of the reason for doing such basics is that I think about my nephews starting high school and that if some of these dots were connected for them and others like them, they might actually have fun with this project in recreating what was learned. I know I don't know all of the gears in the clockwork but am making progress thanks to the help of those in this topic. Thanks!

Also, as noted the code on the HTML page has no copyright or license so if others that want to take it and run with it, please do so, I would be curious to see where others can make it. Also, expect for one minor problem, ChatGPT has been creating the code, (HTML, CSS, JavaScript, JSON, Cytypscape.js) without error so even if you don't know how the code works or how to create it, if one has access to an LLM such as ChatGPT then they can move the idea forward.

Thank you and the others for your support and kinds words.

I also really like what you are doing with Neo4j, didn't know it could support so many nodes in one graph.

[Eric Taucher]

When the graphs move to 2 operations, e.g. ((x ◇ y) ◇ x) the edges of the graph will most likely have to include a means to keep the paths (edges) traceable back to an expression such as

• using a label on each edge
• color coding a path of edges
• a user interface to select one or more paths of edges
• etc.

Currently creating examples of A002489 with N=3 to see if such a graph is intuitive.

[Eric Taucher]

In looking up some old code on graph generation remembered this was quite useful for me at least as a programmer. Others might also find it of value

"Pólya Counting Theory" by S. Gill Williamson

https://cseweb.ucsd.edu//~gill/AlgCombSite/Resources/_CreateSp4.pdf

[Eric Taucher]

In trying to understand Lemma 1.12 in the blueprint, generating the Catalan patterns was easy to comprehend and generate with Prolog code. However in trying to understand how Bell numbers related was and might still be a problem for me.

With the help of ChatGPT o1-preview was able to get this reply.

ChatGPT reply

Certainly! Let's provide a detailed explanation for \( N = 1 \), showing:

1. The 2 Catalan expressions (structures).
2. The 5 Bell partitions of variables.
3. How these combine to form the 10 distinct laws \( w \simeq w' \).

Step 1: Identify the 2 Catalan Expressions for \( N = 1 \)

For total order \( n = 1 \), the Catalan number is:

• \( C_{n+1} = C_2 = 2 \)

These represent the number of distinct binary tree structures (parenthesizations) for expressions involving one operation (\( \diamond \)).

Since we have only one operation at \( N = 1 \), the two distinct structures (up to isomorphism) are:

1. Structure A: An expression where the operation is on the right side.

   • Form: \( w = a \simeq b \diamond c \)

2. Structure B: An expression where the operation is on the left side.

   • Form: \( w = a \diamond b \simeq c \)

(Note: With only one operation, both structures may seem similar, but for completeness, we consider them as distinct for combinatorial purposes.)

Step 2: Determine the 5 Bell Partitions for Variables

The Bell number for \( N = 1 \) is:

• \( B_{n+2} = B_3 = 5 \)

This represents the number of ways to partition a set of 3 elements (variables). The variables involved are those in the expressions \( w \simeq w' \). Let's denote the variables as \( x \), \( y \), and \( z \).

The 5 partitions of the set \( \{ x, y, z \} \) are:

1. Partition 1: \( \{ \{ x, y, z \} \} \)

   • All variables are the same.

2. Partition 2: \( \{ \{ x \}, \{ y, z \} \} \)

   • Variable \( x \) is distinct; \( y \) and \( z \) are the same.

3. Partition 3: \( \{ \{ y \}, \{ x, z \} \} \)

   • Variable \( y \) is distinct; \( x \) and \( z \) are the same.

4. Partition 4: \( \{ \{ z \}, \{ x, y \} \} \)

   • Variable \( z \) is distinct; \( x \) and \( y \) are the same.

5. Partition 5: \( \{ \{ x \}, \{ y \}, \{ z \} \} \)

   • All variables are distinct.

Step 3: Combine Structures and Partitions to Form 10 Laws

We now apply each partition to both structures, resulting in \( 2 \times 5 = 10 \) laws.

Applying Partitions to Structure A: \( a \simeq b \diamond c \)

Variables in Structure A: \( a \), \( b \), \( c \)

Partition 1: \( \{ \{ a, b, c \} \} \)

• All variables are the same: \( a = b = c = x \)
• Law: \( x \simeq x \diamond x \)

Partition 2: \( \{ \{ a \}, \{ b, c \} \} \)

• \( a = x \), \( b = c = y \)
• Law: \( x \simeq y \diamond y \)

Partition 3: \( \{ \{ b \}, \{ a, c \} \} \)

• \( b = x \), \( a = c = y \)
• Law: \( y \simeq x \diamond y \)

Partition 4: \( \{ \{ c \}, \{ a, b \} \} \)

• \( c = x \), \( a = b = y \)
• Law: \( y \simeq y \diamond x \)

Partition 5: \( \{ \{ a \}, \{ b \}, \{ c \} \} \)

• All variables are distinct: \( a = x \), \( b = y \), \( c = z \)
• Law: \( x \simeq y \diamond z \)

Applying Partitions to Structure B: \( a \diamond b \simeq c \)

Variables in Structure B: \( a \), \( b \), \( c \)

Partition 1: \( \{ \{ a, b, c \} \} \)

• All variables are the same: \( a = b = c = x \)
• Law: \( x \diamond x \simeq x \)

Partition 2: \( \{ \{ a \}, \{ b, c \} \} \)

• \( a = x \), \( b = c = y \)
• Law: \( x \diamond y \simeq y \)

Partition 3: \( \{ \{ b \}, \{ a, c \} \} \)

• \( b = x \), \( a = c = y \)
• Law: \( y \diamond x \simeq y \)

Partition 4: \( \{ \{ c \}, \{ a, b \} \} \)

• \( c = x \), \( a = b = y \)
• Law: \( y \diamond y \simeq x \)

Partition 5: \( \{ \{ a \}, \{ b \}, \{ c \} \} \)

• All variables are distinct: \( a = x \), \( b = y \), \( c = z \)
• Law: \( x \diamond y \simeq z \)

Summary of the 10 Laws

1. \( x \simeq x \diamond x \)
2. \( x \simeq y \diamond y \)
3. \( y \simeq x \diamond y \)
4. \( y \simeq y \diamond x \)
5. \( x \simeq y \diamond z \)
6. \( x \diamond x \simeq x \)
7. \( x \diamond y \simeq y \)
8. \( y \diamond x \simeq y \)
9. \( y \diamond y \simeq x \)
10. \( x \diamond y \simeq z \)

Interpretation and Significance

• Each law represents a possible equation of total order \( n = 1 \), involving expressions with one \( \diamond \) operation.
• The Catalan structures provide the skeletons of the expressions, determining where the operation \( \diamond \) is placed.
• The Bell partitions dictate how variables are assigned to the positions in the structures, considering the equivalence up to relabeling.

Connection to Catalan and Bell Numbers

• The Catalan number \( C_{2} = 2 \) accounts for the two distinct structures (ways to parenthesize or arrange the operations) at this order.
• The Bell number \( B_{3} = 5 \) represents the number of ways to assign variables to the positions in each structure, up to equivalence under relabeling.
• Multiplying these together yields the total number of distinct laws: \( 2 \times 5 = 10 \).

Conclusion

By carefully combining the structures provided by the Catalan numbers with the variable assignments from the Bell numbers, we enumerate all possible laws of total order \( n = 1 \) up to relabeling. This method demonstrates how combinatorial mathematics underpins the enumeration of logical laws in abstract algebraic structures like magmas.

---

I hope this detailed explanation clarifies how the Catalan and Bell numbers contribute to generating the expressions and laws for \( N = 1 \). Let me know if you have any further questions!

The detail for me that made understanding how some of the partitions could be used was in this example

Partition 2: {{a},{b,c}}

• a=x, b=c=y
• Law: x≃y⋄y

Mapping more than one of the letters from the set {a,b,c} to one of the value in {x,y} did not seem correct, but seems to be correct.

Since this is a ChatGPT reply, it needs to be verified and thus this post.

[Eric Taucher]

x≃x⋄x
x≃y⋄y
y≃x⋄y
y≃y⋄x
x≃y⋄z
x⋄x≃x
x⋄y≃y
y⋄x≃y
y⋄y≃x
x⋄y≃z

Are those the correct 10 ways to create laws w≃w′ for lemma 1.12 when N = 1?

[Terence Tao]

Yes, these are the ten possible laws, up to relabeling. We have adopted a labeling convention where the first variable encountered (reading from left to right) will be called x, the second will be called y, and so forth (using the somewhat arbitrary ordering xyzwuvrst), so for instance we would label y≃x⋄y as x≃y⋄x, but it is of course the same law.

[Eric Taucher]

Side note for those also trying to understand how to reconstruct the 4694 expressions based on the blueprint.

"A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms" by Paul Tarau (PDF)

It notes

Example 5 Well-formed formulas of minimal logic (possibly types) of size 2.

?- maybe_type(s(s(0)),T,_).
T = (A->A->A) ;
T = (A->B->A) ;
T = (A->A->B) ;
T = (A->B->B) ;
T = (A->B->C) ;
T = ((A->A)->A) ;
T = ((A->B)->A) ;
T = ((A->A)->B) ;
T = ((A->B)->B) ;
T = ((A->B)->C) .