Generating metatheorems from invariants

Stream: Equational

[Hernan Ibarra]

@Anand Rao Tadipatri and myself have written a new blueprint chapter on a certain kind of metatheorems, generalizing the discussion in #Equational > Metatheorem: complexity-preserving equations. We welcome feedback, questions, etc. It is the PR 'Invariant based metatheorem blueprint'. You can find it in the blueprint, chapter 7.

The chapter describes a technique to produce metatheorems of the form "An equation w=w' is good if Invariant(u) = Invariant(v). Then good equations cannot imply non-good equations". Here Invariant(u) is some sort of data type associated with u. Below I list metatheorems I know of that follow this pattern; there are probably many more (help us find some!)

• Suppose w and w' have the same leftmost variable, while w'' and w''' do not. Then w=w' does not imply w'' = w'''.
• Suppose w and w' have the same rightmost variable, while w'' and w''' do not. Then w=w' does not imply w'' = w'''.
• Suppose w and w' have the same set of variables, while w'' and w''' do not. Then w=w' does not imply w'' = w'''.
• Suppose w and w' have the same multiset of variables, while w'' and w''' do not. Then w=w' does not imply w'' = w'''.
• Suppose w and w' have the same multiset of variables, where multiplicities are computed modulo n, while w'' and w''' do not. Then w=w' does not imply w'' = w'''.
• Suppose w and w' has a substring of the form v ∘ v, while w'' and w''' do not. Then w = w' does not imply w''= w'''.

[Hernan Ibarra]

Oh, and there are some tasks/open questions at the end of chapter that may help guide the discussion.

[Cody Roux]

The link looks broken?

[Cody Roux]

Also: I kind of wonder if each invariant happens to be a cleverly chosen functor G \alpha and a clever FreeMagma \alpha -> G \alpha. Maybe this is a triviality but deserves to be pointed out?

[Cody Roux]

E.g the first one, G \alpha = \alpha and op x y = x etc.

[Hernan Ibarra]

Cody Roux said:

The link looks broken?

Oops. The PR was merged, so you can now find it in the main blueprint.

[Hernan Ibarra]

The key to doing good category theory is to respect trivialities.

[Hernan Ibarra]

What you said seems right to me, I need to think about it more. You may want to read the 'Note for category theorists' in the chapter (if you haven't already).

[Anand Rao Tadipatri]

Here's the link to the file in the main repository: https://github.com/teorth/equational_theories/blob/main/blueprint/src/chapter/metatheorems_from_invariants.tex.