Metatheorem: complexity-preserving equations

Stream: Equational

[Hernan Ibarra]

Apologies if someone has thought of this before, I could not find anything in previous discussions. Say an equation is complexity-preserving (equicomplex?) if the number of times the binary operation is applied on the LHS equals the corresponding number on the RHS. Then a complexity-preserving equation cannot imply an equation that does not preserve complexity. (I think this is true, but would appreciate feedback). Maybe someone here knows how to calculate the number n of complexity preserving equations. Then the number of implications settled (on the negative) by this metatheorem is n*(4694 - n).

[Joachim Breitner]

Maybe I'm misunderstanding, but doesn't x = y imply all other equations? That looks complexity-preserving according to your definition?

[Hernan Ibarra]

Joachim Breitner said:

Maybe I'm misunderstanding, but doesn't x = y imply all other equations? That looks complexity-preserving according to your definition?

Ah you are right, silly me. I should add to the definition that the set of variables (counted with multiplicity) in the LHS and RHS are also equal. Does this work now?

[Daniel Weber]

You might be able to get numbers from the formulas in equational#80

[Edward van de Meent]

maybe it is the case that such an equation implies a non-preserving equation, but there is no proof?

[Edward van de Meent]

or does this fall under completeness of first-order logic?

[Hernan Ibarra]

Edward van de Meent said:

maybe it is the case that such an equation implies a non-preserving equation, but there is no proof?

No, this contradicts the Godel's completeness theorem (not to be confused with his incompleteness theorems, see here).

[Daniel Weber]

Edward van de Meent said:

or does this fall under completeness of first-order logic?

I believe it does

[Maja Kądziołka]

Indeed, once you add the assumption that all variables occur the same number of times on both sides, this works as a consequence of Birkhoff's theorem (by induction on proof tree)

[Hernan Ibarra]

Maja Kądziołka said:

Indeed, once you add the assumption that all variables occur the same number of times on both sides, this works as a consequence of Birkhoff's theorem (by induction on proof tree)

If I understand correctly, Birkhoff's theorem is 'completeness for equational logic' right? (I quickly glanced at the wikipedia page). In that case, I agree with you.

[Maja Kądziołka]

I think you can have a similar metatheorem: an equation where all variables occur on both sides cannot imply one where the occur set differs between the two sides of the equation

[Maja Kądziołka]

I suppose the next question to ask is for what other such metrics/invariants the proof works out

[Daniel Weber]

There are 164 equations where all variables occur on both sides, and in 32 of those the multisets are also equal

[Maja Kądziołka]

I suppose this is the sort of thing that might be well-known by universal algebraists

[Hernan Ibarra]

Maja Kądziołka said:

I think you can have a similar metatheorem: an equation where all variables occur on both sides cannot imply one where the occur set differs between the two sides of the equation

You don't need that all variables occur right? Only that the multisets are equal. So I think the general metatheorem is that equations whose LHS and RHS multisets are equal cannot imply equations whose multisets differ. (Again, correct me if I'm wrong).

[Daniel Weber]

A more general metatheorem is that for every function $f$ on multisets which satisfies $f(a) = f(b) \to f(a + c) = f(b + c)$ and $f(a) = f(b) \to f(a[X := Y]) = f(b[X := Y])$, if $f(lhs) = f(rhs)$ then the equation can only imply other equations which satisfy that, although I'm not certain these are the correct conditions on $f$.

[Cody Roux]

I could add formalizing proof rules and Birkhoff's theorem to https://github.com/teorth/equational_theories/issues/104, is that a good idea?

It's probably not _too_ much pain for equational logic.

[Hernan Ibarra]

I see this metatheorem has been added to the blueprint two hours ago as Theorem 3.8. The slick proof there is better and doesn't appeal to Birkhoff's theorem.

[Daniel Weber]

Maja Kądziołka said:

I think you can have a similar metatheorem: an equation where all variables occur on both sides cannot imply one where the occur set differs between the two sides of the equation

This can also be established in a similar fashion, by considering $\mathbb{Z}_{2^n}$ with bitwise or

[Hernan Ibarra]

It generalizes as well, doesn't it?

[Hernan Ibarra]

Oh you beat me to the punch

[Hernan Ibarra]

I'm not sure we are saying the same thing actually. We can have a metatheorem that says: if each variable occurs on the LHS and the RHS the same number of times modulo n then it can only imply equations of the same type.

[Hernan Ibarra]

And the same proof works right? Consider linear forms modulo n

[Daniel Weber]

Oh, that's not what I meant, I talked about each variable occuring on both sides

[Hernan Ibarra]

Ah okay I see. But does the new metatheorem make sense?

[Terence Tao]

Ah, I was just going to notify this thread that I had formalized the first metatheorem on the blueprint, but I see you noticed it already. Please feel free to add additional metatheorems of this type directly to the blueprint. I will also create a task to formalize the first metatheorem in Lean.

[Daniel Weber]

This can be generalized to any specific magma where checking laws is easy, right? Another example is that equations where the leftmost variable is equal in the LHS and RHS can't imply an equation where it isn't (by using any magma with $x \circ y = x$)

[Terence Tao]

Would you be willing to add that lemma (and its dual) to the blueprint also? Collecting all these easy metatheorems could be worthwhile (and good practice for formalization of metatheory).

[Anand Rao Tadipatri]

I may have a slightly different way to prove @Hernan Ibarra's metatheorem (adapting the proof from the blueprint) that may generalize to other invariants of expressions.

Let $w \simeq w'$ be a law such that every variable appears the same number of times in both $w$ and $w'$, and let $w'' \simeq w'''$ be a law implied by it. Further, assume that these expressions contain at most $n$ variables $x_1, x_2, \ldots, x_n$. The condition on the law $w \simeq w'$ is equivalent to the statement that evaluating both expressions $w$ and $w'$ in the magma $(\mathbb{Z}^n, +)$ under the substitution $x_i \mapsto b_i$, where $b_i$ is the $i$ th basis vector of the form $(0, 0, \ldots, 1, \ldots, 0)$, yields equal elements of $\mathbb{Z}^n$.

It turns out that $(\mathbb{Z}^n, +)$ is in fact a model of the law $w \simeq w'$. Consider $n$ arbitrary elements $v_1, v_2, \ldots, v_n$ of $\mathbb{Z}^n$. Performing the substitution $x_i \mapsto v_i$ in an expression is equivalent to first performing the substitution $x_i \mapsto b_i$ and then applying the unique endomorphism of $\mathbb{Z}^n$ sending each $b_i$ to $v_i$. By assumption, both expressions $w$ and $w'$ evaluate to the same element of $\mathbb{Z}^n$ after the substitution $x_i \mapsto b_i$, and therefore, they evaluate to the same element of $\mathbb{Z}^n$ after the substitution $x_i \mapsto v_i$. This holds for any set of elements $v_1, v_2, \ldots, v_n$ of $\mathbb{Z}^n$, and hence $(\mathbb{Z}^n, +)$ is a model for the law $w \simeq w'$.

This means that $(\mathbb{Z}^n, +)$ is also a model for the law $w'' \simeq w'''$, since this is assumed to be implied by $w \simeq w'$. In particular, this means that performing the substitution $x_i \mapsto b_i$ evaluates both $w''$ and $w'''$ to the same element of $\mathbb{Z}^n$. This is equivalent to saying that $w''$ and $w'''$ have the same multisets of variables appearing in them, and the result follows.

[Anand Rao Tadipatri]

I believe that one can use the magma $((\mathbb{Z}/m)^n, +)$ in this argument to cover the case of counting variable multiplicities modulo $m$.

[Daniel Weber]

Isn't that basically the same argument except over $\mathbb{Z}^n$ instead of $\mathbb{R}$?

[Anand Rao Tadipatri]

I think @Daniel Weber's argument follows by replacing $\mathbb{Z}^n$ with the free magma on $x_1, x_2, \ldots, x_n$ satisfying the multiplication law $x \circ y = x$.

[Anand Rao Tadipatri]

Yes, it is adapted from that, but I feel that this formulation may be easier to formalize and generalize.

[Hernan Ibarra]

I like this proof a bit better since it makes explicit the linear algebra. With the old argument you need the result that the coefficients of a linear form (over R say) are uniquely determined. I know this is equivalent but the linear algebra formalism will maybe make it easier to formalise, as Anand says.

[Anand Rao Tadipatri]

Anand Rao Tadipatri said:

Yes, it is adapted from that, but I feel that this formulation may be easier to formalize and generalize.

To elaborate further, I believe that this argument generalizes by replacing $(\mathbb{Z}^n, +)$ by any magma $M$ with a lifting property, i.e., if there is a set $X$ and map $\operatorname{basis} : X \to M$ such that any $f : X \to M$ extends to a magma homomorphism $F : M \to M$ satisfying $f = F \circ \operatorname{basis}$ .

In the proof above, $X := \operatorname{Fin}(n)$ and $M := \mathbb{Z^n}$ with $\operatorname{basis} := i \mapsto b_i$ .

[Anand Rao Tadipatri]

It's possible that I haven't understood the proof in the blueprint completely and that this generalization is also implied by it, in which case I apologize for the confusion and redundancy.

[Cody Roux]

I think I can prove this relatively easy using completeness, and the concrete proof syntax from https://github.com/teorth/equational_theories/pull/123, will do that today if there's still interest.

[Anand Rao Tadipatri]

Thanks, I was about to take a stab at formalizing this and the MagmaLaw definition was exactly what I needed. I may still try to have a go at it over the next couple of hours; I'll let you know if I make any progress.

[Terence Tao]

I like the new proof too. I am busy the whole day, but if anyone wants to go and and PR in the new proof to replace the old one on the blueprint, please go ahead (but make a note here that you are doing so there is no duplication of effort)!

[Hernan Ibarra]

I would like to add a new section on these metatheorems in chapter 3. I will try to work on the blueprint today.

[Cody Roux]

I've proven a simple meta-theorem along these lines, hope this was not unwarranted (I didn't create an issue, etc):

https://github.com/codyroux/equational_theories/blob/codyroux/derivation-preserves-size/equational_theories/SizeMetatheorem.lean

Is this related to what we want? Does it help?

[Edward van de Meent]

i might be reading this wrong, but isn't your definition of FreeMagma.size constantly 0?

[Edward van de Meent]

in the base case it's 0, and otherwise you take the sum of the parts? so it's still 0?

[Daniel Weber]

You can use order from https://github.com/teorth/equational_theories/blob/main/equational_theories/Counting.lean#L12

[Cody Roux]

hehe oops

[Cody Roux]

miraculously, adding +1 to the size of Fork does not change the validity of any proofs!

[Cody Roux]

(try doing that in a paper proof!)

[Cody Roux]

@Daniel Weber updated to use that definition. Should I PR?

[Anand Rao Tadipatri]

I've made an attempt at formalizing the meta-theorem in generality, but it needs more work: https://github.com/0art0/equational_theories/blob/e238b81b3ae2b195eab96ddc3243796257c5c116/equational_theories/LiftingMagma.lean. Some of the changes I've introduced break code in Compactness.lean, so this is not yet ready to be merged (on the bright side, the proof of soundness is now a single line of code that uses aesop).

[Anand Rao Tadipatri]

I'll be joining @Hernan Ibarra in working on the section of the blueprint for metatheorems. We would like to lay the result out in generality, so we anticipate that it may take a bit of time.

[Cody Roux]

I've created an issue, in addition to a PR (though I haven't marked the PR as resolving the issue quite yet):
https://github.com/teorth/equational_theories/issues/156
https://github.com/teorth/equational_theories/pull/152

I'm actually confused about what we're doing here; I'll open a new thread to discuss what the general structure of our metatheorems development should be.