Equation 2126

Stream: Equational

[Bhavik Mehta]

All 35 of the conjectured non-implications from 2126 are false, and can be proven so by completing the rewriting system and showing that both sides of the resultant equation are reduced. The completion is

• ((yy)x)(xz) = x
• (xx)(((xx)y)z) = (xx)y
• ((yy)((xx)z))z = (xx)z
• ((xx)y)((((xx)y)w)z) = ((xx)y)w

[Shreyas Srinivas]

was this from an ATP?

[Bhavik Mehta]

It was from using kbcv to complete the TRS, then just inspection of the conjectures from https://teorth.github.io/equational_theories/implications/?2126

[Bhavik Mehta]

(Plus the intuition that this equation is like the central groupoid law and so it was a reasonable bet that it had a nice completion, which is why I tried this one and not others)

[Shreyas Srinivas]

Your own implementation of kbc?

[Shreyas Srinivas]

That's really cool

[Bhavik Mehta]

No, kbcv: http://cl-informatik.uibk.ac.at/software/kbcv/

[Terence Tao]

Nice! With duality, that’s 70 implications off the table, a sizeable advance! I’ll open a task to formalize this now.

[Shreyas Srinivas]

Oh I missed the v in kbcv

[Shreyas Srinivas]

Nice work

[Bhavik Mehta]

My proof that terms in central groupoids have a normal form in Lean forces you to discover the completion, so I could have done it like that too. But that isn't what I did; it will probably be how I formalise this unless someone does it before me using Confluence.lean

[Terence Tao]

opened equational#515 for this. There are some details on how to manage Equations.lean because we are trying (manually) to keep Chapter 2 of the blueprint synchronized with this file.

[lyphyser]

I think this is true for all current conjectures, I added infrastructure in https://github.com/teorth/equational_theories/pull/510 to define a system of rewrite rules, and it should be possible to prove all remaining conjectures this way, using output from either Twee or Vampire (they seem better than kbcv)

[lyphyser]

I'll probably do it in the next days, my current plan is to generate the rewrite rule system and the skeleton of the proof automatically using rule_system like the current ones in Confluence.lean, then prove manually and if a pattern emerges possibly write a tactic that can prove all of them and then switch to fully automated generation

[lyphyser]

an alternative could be to generally show that all critical pairs are confluent rather than showing that the normal forms of the hypothesis sides are equal; it seems that might be much slower to compile and complicated though, but I haven't tried it and maybe there's a great way to do it

[lyphyser]

also the current method has only been used for systems with 2 rules so far, so might need some sort of extra work for larger systems, although it could also just work as is

[lyphyser]

e.g. the system presented here for 2126 is substantially more complicated then the ones in the proofs so far

[Terence Tao]

Just a notational question: does your system show that 2126 is a confluent law, or is it establishing something weaker than confluence?

[Bhavik Mehta]

2126 isn't confluent, but the system I gave above is a completion of it: they're equations derivable from 2126 but together the 4 of them give a confluent system

[lyphyser]

on the surface it seems it establishes something weaker (but still sufficient to prove non-implications) but maybe it's actually equivalent, not totally sure

[lyphyser]

for context this is the current proof for the ! 3588 -> implications submitted in https://github.com/teorth/equational_theories/pull/510

rule_system rules {x y z w}
| z ⋆ ((x ⋆ y) ⋆ z) => x ⋆ y
| ((z ⋆ w) ⋆ (x ⋆ y)) ⋆ (z ⋆ w) => x ⋆ y

theorem comp2 {α} [DecidableEq α] {x y z : FreeMagma α} (hxy: NF rules (x ⋆ y)):
rules (z ⋆ rules (x ⋆ y ⋆ z)) = x ⋆ y := by
generalize h: rules (x ⋆ y ⋆ z) = e
simp only [rules.elim] at h
separate
· apply rules.eq2
· apply rw_eq_self_of_NF rules hxy
· apply rules.eq1

theorem comp3 {α} [DecidableEq α] {x y z : FreeMagma α} (hx: NF rules x) (hy: NF rules y):
rules (z ⋆ rules (rules (x ⋆ y) ⋆ z)) = rules (x ⋆ y) := by
generalize h: rules (x ⋆ y) = e
simp only [rules.elim] at h
separate
all_goals apply comp2
· apply Everywhere.left hy
· apply Everywhere.right hx
· rw [NF, Everywhere]
refine ⟨hx, hy, ?_⟩
simp only [rules.elim]
right
constructorm* _ ∧ _
all_goals trivial

@[equational_result]
theorem «Facts» :
∃ (G : Type) (_ : Magma G), Facts G [3588] [3862, 3878, 3917, 3955] := by
use ConfMagma (@rules Nat _), inferInstance
repeat' apply And.intro
· rintro ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩
simp only [Magma.op, bu, hx, hy, hz, buFixed_rw_op]
symm
congr! 1
apply comp3 ((NF_iff_buFixed rules).mpr hx) ((NF_iff_buFixed rules).mpr hy)
all_goals refute

[lyphyser]

so e.g. in this case the question is whether establishing that rules (z ⋆ rules (rules (x ⋆ y) ⋆ z)) = rules (x ⋆ y) is weaker than establishing that the "rules" rewrite rules system is confluent or whether they are equivalent

[lyphyser]

2126 -> proved in https://github.com/teorth/equational_theories/pull/510

[lyphyser]

I think I proved them all modulo duality in that pull request

[Daniel Weber]

Looking at equation 1659 $x = (x \diamond y) \diamond ((y \diamond y) \diamond z)$, the pair of rules x ◇ ((y ◇ y) ◇ z) = x ◇ y and (x ◇ y) ◇ y = x seems confluent to me (and both of them together are equivalent to 1659). Can someone better-versed in confluence check this?

[lyphyser]

no; Twee doesn't terminate and gives output that starts like this:
11. mul(X, mul(mul(mul(mul(Y, Y), Z), Y), W)) -> mul(X, Y)
12. mul(X, mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V)) -> mul(X, Y)
13. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U)) -> mul(X, Y)
14. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U), Y), T)) -> mul(X, Y)
15. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U), Y), T), Y), S)) -> mul(X, Y)
16. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U), Y), T), Y), S), Y), X2)) -> mul(X, Y)
17. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U), Y), T), Y), S), Y), X2), Y), Y2)) -> mul(X, Y)
18. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U), Y), T), Y), S), Y), X2), Y), Y2), Y), Z2)) -> mul(X, Y)
19. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U), Y), T), Y), S), Y), X2), Y), Y2), Y), Z2), Y), W2)) -> mul(X, Y)
20. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U), Y), T), Y), S), Y), X2), Y), Y2), Y), Z2), Y), W2), Y), V2)) -> mul(X, Y)
21. mul(X, mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(mul(Y, Y), Z), Y), W), Y), V), Y), U), Y), T), Y), S), Y), X2), Y), Y2), Y), Z2), Y), W2), Y), V2), Y), U2)) -> mul(X, Y)

[lyphyser]

maybe adding the infinite rule scheme X(YY(?Y)*?) -> XY would work?

[Daniel Weber]

I think it might, if you can test it that'd be great (does Twee support infinite rule schemes?)

[lyphyser]

perhaps there's a way to express it finitely by adding other symbols?

[Daniel Weber]

You can define good(Y, A) ↔ A = Y ∨ ∃ B C, good(Y, B) ∧ A = mul(mul(B, Y), C), I guess, and then add good(Y, A) -> mul(X, A) = mul(X, Y)

[Daniel Weber]

I tried encoding this to vampire as

fof(h1, axiom, ! [X, Y] : mul(mul(X, Y), Y) = X).
fof(good_def, axiom, ! [A, Y] : (good(Y, A) <=> (A = Y | (? [ B, C] : (good(Y, B) & (A = mul(mul(B, Y), C))))))).
fof(h2, axiom, ! [X, Y, A] : (good(Y, A) => (mul(X, A) = mul(X, Y)))).

[Daniel Weber]

It can't reach saturation from this, but from what I'm seeing all equations it produces are reduced by this

[Daniel Weber]

How does one prove confluence?

[Fan Zheng]

It looks confluent to me. The only non trivial critical pair arises from matching yy with xy=x((yy)z...), in which case except for the first y, the other y's can be replaced by a simple variable.

[Fan Zheng]

It seems that ChatGPT is able to find the pattern in this infinite sequence:
https://chatgpt.com/share/670ce7db-8a44-800d-a5dc-8462c12eca3b
So here is an opportunity for input from AI.

[Kevin Buzzard]

This is 404 for me(needs login)

[Bhavik Mehta]

As @lyphyser says, the two equations as given by Daniel aren't confluent: the term x((tt)z) with t = (yy)w has two reductions, and produces the equation x((ty)z) = xy, both sides of which are fully reduced under the two proposed rewrite rules. (I abbreviate t just for ease of transcription!)

[Fan Zheng]

@Bhavik Mehta After putting back t you get x((((yy)w)y)z)=xy, which is the next one in the infinite sequence.

[Bhavik Mehta]

Indeed, using a third equation not included in Daniel's two :)

[Terence Tao]

Just to confirm (for the purposes of reporting in my daily personal log), does this ChatGPT-inspired infinite sequence of rewriting rules establish that 1659 is confluent?

[Daniel Weber]

lyphyser said:

maybe adding the infinite rule scheme X(YY(?Y)*?) -> XY would work?

Isn't that what lyphyser suggested here?

[Fan Zheng]

The correct statement is: the rules x=xyy, xy=x(yyz), xy=x(yyzyw) (multiplication is from left to right), ... together form a confluent set. To be fair I wouldn't say it is GPT inspired, because the pattern is easily recognizable to the human eye. I am just trying to see if ChatGPT can figure out the pattern, and it can.

[Terence Tao]

Even if this particular example is also visible to the human eye, knowing about the ChatGPT option is valuable, because it could potentially scale up better than human inspection. (Though at this stage we are down to a few dozen unresolved equations, so for this project at least we might be able to do the remaining confluence analysis just by hand.)

[Fan Zheng]

Initially I misread Tao's question as whether ChatGPT can prove that the set is confluent. I tried it, and the response degraded to AI-style gibberish (it says that they are not confluent without giving any new critical pair.) That said, I'm not on any fancy plan, so do not have access to the strongest LLM.

[Fan Zheng]

Here is the text version:

Equation Pattern Prediction

Here is a sequence of equations: xy=x((yy)z) xy=x((((yy)z)y)w) xy=x((((((yy)z)y)w)y)u) Can you find the pattern? Can you predict the next ones in the series?

ChatGPT

Yes! Let's examine the sequence of equations to identify a pattern.

1. First equation:

   xy=x((yy)z)

   • On the right-hand side, we have a composition where (yy) is computed first, then multiplied by z, and finally everything is multiplied by x.

2. Second equation:

   xy=x((((yy)z)y)w)

   • Here, the nested part inside the parentheses grows. After computing ((yy)z), it is multiplied by y, and then by w.

3. Third equation:

   xy=x((((((yy)z)y)w)y)u)

   • The nested part gets even larger: after computing ((((yy)z)y)w), it is multiplied by y and then by u.

General pattern:

• The right-hand side of the equation contains a progressively deeper sequence of nested expressions.
• Each expression starts with (yy)z, then subsequent levels are multiplied by y, and at the end, a new variable is introduced at each step (first w, then u).

Predicting the next ones:

4. Fourth equation:
   The next equation would continue this pattern by adding another nested multiplication with y and introducing a new variable (say v).

   xy=x((((((((yy)z)y)w)y)u)y)v)

5. Fifth equation:
   The next one adds yet another layer and a new variable (say t).

   xy=x((((((((((yy)z)y)w)y)u)y)v)y)t)

Conclusion:

The general structure involves nesting an expression that multiplies (yy)z by y, with a new variable introduced in each step. Each subsequent equation deepens the level of nesting and multiplies by y one more time.

[Terence Tao]

Thanks! Without integration with a formal proof assistant, using an LLM to actually prove anything beyond an undergraduate or early graduate homework assignment is still too unreliable to use, but this use case (to detect possible patterns that one could then check externally) could be a more promising workflow.

[Michael Bucko]

Does it have to that reliable? How about agents that would break the tasks down (CoT), and then try them out (esp. O1, when available, with RL instead of RLHF) until there're no goals left (and Lean marks the result with qed)?

One would just be leaving an agent "running all night".

Also, I have one algorithm idea that could be used in agents. It's a bit like collaborative filtering. One would give the LLM a task together with all the proofs related to that task in the context, and ask it to create a result that follows not only the task, but the task + the context.

[Shreyas Srinivas]

I think Terence Is talking about the final proof

[Shreyas Srinivas]

Lean is basically the tutor in the feedback loop

[Eric Taucher]

Ran this prompt

Here is a sequence of equations:

xy=x((yy)z)
xy=x((((yy)z)y)w)
xy=x((((((yy)z)y)w)y)u)

Can these form a confluent and terminating set of equations? If not can it be done by adding some equations via Knuth-Bendix?

using ChatGPT o1-preview

https://chatgpt.com/share/671025cc-5c90-8013-b394-5e7738c50725

and o1-mini

https://chatgpt.com/share/671025e2-4784-8013-bc17-31af5aa1ca07

both noted a similar answer.

No; as given, these equations cannot form a confluent and terminating set, and even with additional equations from Knuth-Bendix completion, the system cannot be made both confluent and terminating.

[Joachim Breitner]

You should probably ask for the other direction, conventional way of writing rewrite rules is with the pattern left and the result right. Only we have it sometimes the other direction here because our equations tend to be written that way. Maybe then chatgpt would answer differently

[Joachim Breitner]

Also it's saying things that are not really true:

Confluence: Without termination, achieving confluence is not feasible.

The rule xy -> yx is non-terminating, but confluent.

[Joachim Breitner]

Ah, and maybe worth clarifying to chatgpt whether you consider these rewrite rules as rules on words or on the free magma.

[Eric Taucher]

As I am not an expert with term rewriting and much of the project is beyond my understanding, if you create the prompt I will be happy to run it with the o1-mini model first and then possibly the o1-preview model. Use of these models is extremely limited.

https://community.openai.com/t/o1-models-limits-increased-for-plus-and-team-users/947488

o1-mini - 50 messages per day
o1-preview - 50 messages per week

[Joachim Breitner]

Your prompt wasn't bad, I'd maybe try

Here is a term rewriting system given by these rules::

x((yy)z) -> xy
x((((yy)z)y)w) -> xy
x((((((yy)z)y)w)y)u) -> xy

Is this rewriting system confluent? If not, can it be made confluent by adding more rules, maybe via Knuth-Bendix?

[Eric Taucher]

Thanks for the prompt.

Model: o1-mini

https://chatgpt.com/share/671032b1-db08-8013-bafe-c36e4c189e41

---

---

For those lacking access via the share link

---

Thought process

Thought for 7 seconds
Identifying the pattern

I’m looking at the rules of the term rewriting system (TRS). The left-hand sides involve x with nested (yy)z and other variables, possibly concatenation or a binary operation. I need to clarify the terms’ structure.
Piecing together string rules

I’m working through this idea of interpreting the system as a string rewriting system. It seems clear that concatenation applies and groupings are associative. Reactions to string operations highlight focusing on specific nested terms and critical pairs.
Analyzing rule patterns

I'm mapping out the left-hand sides of the rules, noticing they consistently involve an outer term x followed by a deeply nested application of y, z, w, and u. This leads me to consider the confluence of the term rewriting system (TRS).
Investigating overlapping rules

I’m noting that Confluence involves comparing left-hand sides of rules for intersections and common reductions. Examples show terms rewritten by different rules depend on nested parts.
Figuring out confluence

I'm mapping out the confluence of a rule system, considering associativity, termination, and unique normal forms. Distinct left-hand sides might prevent overlaps.

---

The given term rewriting system (TRS) consists of the following rules:

1. \( x((yy)z) \rightarrow xy \)
2. \( x((((yy)z)y)w) \rightarrow xy \)
3. \( x((((((yy)z)y)w)y)u) \rightarrow xy \)

Analyzing Confluence

Confluence in a TRS means that if a term can be rewritten in multiple ways, all those different rewriting paths eventually lead to a common term. To determine if the system is confluent, we need to examine potential overlaps and critical pairs where different rules might apply to the same term in different ways.

1. Non-overlapping Rules:

   • Each rule in the system handles a distinct pattern with increasing nesting. For instance, the first rule deals with \( x((yy)z) \), the second with \( x((((yy)z)y)w) \), and so on.
   • Since the left-hand sides of the rules do not overlap (i.e., no single term matches the left-hand side of more than one rule simultaneously), there are no critical pairs arising from overlapping rules.

2. Unique Normal Forms:

   • Each rule reduces a complex term to the simpler form \( xy \).
   • Given the specific patterns, any term that matches a left-hand side of a rule will uniquely reduce to \( xy \), ensuring that there is only one possible normal form for each reducible term.

3. Termination:

   • The rules are designed to simplify terms by reducing their complexity, suggesting that the system is terminating (no infinite rewriting sequences).

Given these observations, the TRS appears to be confluent because:

• There are no overlapping rules that could lead to divergent rewriting paths.
• Each reducible term has a unique normal form.
• The system is terminating, preventing infinite rewriting sequences.

Making the System Confluent (If Necessary)

If, however, there are additional terms or patterns not covered by the existing rules that could lead to ambiguities or multiple normal forms, the system might not be confluent as is. In such cases, applying the Knuth-Bendix completion procedure could help:

• Knuth-Bendix Completion: This algorithm attempts to extend the TRS by adding necessary rules to resolve any critical pairs, thereby ensuring confluence.
• Adding Rules: By systematically identifying and resolving overlaps or ambiguities, additional rules can be introduced to handle more complex or previously unhandled terms.

Conclusion

The given term rewriting system is confluent as it stands because its rules do not overlap and each reducible term has a unique normal form. However, if additional patterns or terms introduce ambiguities, the system can be made confluent by adding more rules using the Knuth-Bendix completion procedure.

Answer:
No, the system as given is not confluent. However, by introducing additional rules (for example, through the Knuth-Bendix completion process), it can be extended to become confluent.