Counterexamples by Enumerating Words in Quotient Magma

Stream: Equational

[Andrés Goens]

If we have two laws $l_1 ≃ r_1$ and $l_2≃ r_2$ over FreeMagma (Fin n) (choosing n to be large enough that both words can be expressed), then we should be able to quotient over $l_1 ≃ r_1$ in a suitable way, right? Any counterexample that uses n elements should also be in the image of an epimorphism of this (by the universal property). (I'm basing this on the intuition for groups, so please correct me if I'm missing something!)

So, would it make sense to look for counterexamples by just picking random words and checking whether by plugging these into $l_2, r_2$ in the quotient magma, and checking if the words are equivalent (i.e. equal in the quotient)l? Or is the problem with this that the equality of words might be undecidable in some of these magmas (even with a single relation)?

[Daniel Weber]

The problem of checking equality in the quotient is exactly the problem of deciding implication (by completeness, as an equality in the quotient means equality using a sequence of rewrites with the equation)

[Daniel Weber]

This might be interesting for finite models, though

[Anand Rao Tadipatri]

@Andrés Goens This is the general idea behind @Hernan Ibarra's metatheorem (theorem 4.8 in the blueprint) about counting variables on both sides of the equation, which has been expanded upon in Chapter 8 of the blueprint. You're right that for an arbitrary magma, the problem might be undecidable; however, one can pick certain "nice" classes of magmas for which the problem of deciding equality of elements is computationally tractable.

[Andrés Goens]

right, I meant this just for counter-examples

[Andrés Goens]

shouldn't the deciding equality for the quotient of 1 law be always decidable and tractable, if we just do what simp does (rewrite lhs -> rhs as often as we can) that should give a normal form

[Andrés Goens]

but yeah, I can see why stuff like theorem 4.8 would make things more computationally tractable, I'll have to read up on chapter 8!

[Hernan Ibarra]

Andrés Goens said:

shouldn't the deciding equality for the quotient of 1 law be always decidable and tractable, if we just do what simp does (rewrite lhs -> rhs as often as we can) that should give a normal form

I don't think that just because you are quotiening out by one law you are guaranteed nicesness of the reduction. At any given point there might be many ways to apply the reduction but only some of them will make progress.

[Andrés Goens]

@Hernan Ibarra :thinking: can you give an example of that? I thought since we're in the free magma, there's no ambiguity in the elements (like assocativity or similar), and since the laws are expressed in tho generators of the free magma (and not universally quantified like in an "Equation"), there should be no ambiguity in the matching either. What am I missing here?

[Hernan Ibarra]

If the generators satisfy the law then the free magma also satisfies the universally quantified law right?

[Hernan Ibarra]

And then the hardness of the equation kicks in.

[Andrés Goens]

The free magma doesn't satisfy any law, but if we quotient it by a law it might be that we need to interpret it as universally quantified for the quotient, yeah. I'll admit I haven't thought through how the quotient construction should go exactly